同步数据流程序的可信排序

CREDIBLE SORTING FOR SYNCHRONOUS DATA-FLOW PROGRAMS

Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的,需要对其进行因果分析和串行化。利用Coq工具,形式化定义拓扑排序的性质和相应层次的Lustre的语义;对Lustre程序进行因果分析和排序;证明排序后的程序满足拓扑排序的性质;证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。

Lustre is a synchronous data-flow language which is widely applied in nuclear power and aviation,all are in the areas with high credibility. The safety of the compiler will be significantly improved by applying the formal verification approach to implementing the translation from Lustre to C and proving its procedure. Because the Lustre program executes concurrently,the causality analysis and sequentialisation on it is necessary. In the paper,we implement a credible sorting procedure for Lustre program,which is completed by in the first formally defining the property of topological sorting and the Lustre semantics in associate layers with Coq tool,doing the causality analysis and sorting on Lustre program,then proving that a sorted Lustre program fulfils the property of topological sorting,and finally proving that any two Lustre programs both of which satisfying the property of topological sorting are semantically equivalent in execution.