|
|||||
|
|
| 同步数据流程序的可信排序 | |
| 引用本文： | 甘元科 张玲波 石 刚等. 同步数据流程序的可信排序[J]. 计算机应用与软件, 2014, 0(5): 1-5,56 |
| 作者姓名： | 甘元科 张玲波 石 刚等 |
| 作者单位： | ;1.清华大学计算机科学与技术系;2.北京广利核系统工程有限公司 |
| 摘 要： | Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的,需要对其进行因果分析和串行化。利用Coq工具,形式化定义拓扑排序的性质和相应层次的Lustre的语义;对Lustre程序进行因果分析和排序;证明排序后的程序满足拓扑排序的性质;证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。 |
| 关 键 词： | 同步数据流 排序 形式化验证 Coq |
CREDIBLE SORTING FOR SYNCHRONOUS DATA-FLOW PROGRAMS |
|
| Abstract: | |
| Keywords: | |
| 本文献已被 CNKI 等数据库收录！ | |