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

作者：甘元科; 张玲波; 石刚; 王生原; 董渊; 张智慧; 王沿海

来源：计算机应用与软件, 2014, 31(05): 1-56.

• 同步数据流
• 排序
• 形式化验证
• Coq

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

• 单位
  清华大学; 北京广利核系统工程有限公司