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

• 作者: 张智慧 张玲波 王沿海 王生原 甘元科 石刚 董渊
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 同步数据流 排序 形式化验证 Coq
• 年，卷（期）: 2014,（5）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 1-5,56
• 页数: 6页
• 分类号: TP314
• 字数: 8954字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2014.05.001

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
2	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
3	石刚	清华大学计算机科学与技术系	11	38	4.0	5.0
4	张智慧		5	8	2.0	2.0
5	甘元科	清华大学计算机科学与技术系	5	24	4.0	4.0
6	张玲波	清华大学计算机科学与技术系	2	8	2.0	2.0
7	王沿海		2	8	2.0	2.0