首页 | 本学科首页   官方微博 | 高级检索  
     

同步数据流程序的可信排序
引用本文:甘元科 张玲波 石 刚等. 同步数据流程序的可信排序[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 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号