QQ客服 官方微博 反馈留言

	同步数据流程序的可信排序
	甘元科 ; 张玲波 ; 石刚 ; 王生原 ; 董渊 ; 张智慧 ; 王沿海 ; Gan Yuanke ; Zhang Lingbo ; Shi Gang ; Wang Shengyuan ; Dong Yuan ; Zhang Zhihui ; Wang Yanhai
	2016-03-30 ; 2016-03-30
关键词	同步数据流 排序 形式化验证 Coq Synchronous data-flow Sorting Formal verification Coq TP314
其他题名	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.
语种	中文 ; 中文
内容类型	期刊论文
源URL	[http://ir.lib.tsinghua.edu.cn/ir/item.do?handle=123456789/146874]
专题	清华大学
推荐引用方式 GB/T 7714	甘元科,张玲波,石刚,等. 同步数据流程序的可信排序[J],2016, 2016.
APA	甘元科.,张玲波.,石刚.,王生原.,董渊.,...&Wang Yanhai.(2016).同步数据流程序的可信排序..
MLA	甘元科,et al."同步数据流程序的可信排序".(2016).

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。