同步数据流语言高阶运算消去的可信翻译

来源：软件学报杂志2015年第2期北京时间：

作者：刘洋,甘元科,王生原,董渊,杨斐,石刚,闫鑫

单位：刘洋，清华大学 计算机科学与技术系, 北京 10008411,甘元科，清华大学 计算机科学与技术系, 北京 10008402,王生原，清华大学 计算机科学与技术系, 北京 10008403,董渊，清华大学 计算机科学与技术系, 北京 10008404,杨斐，清华大学 计算机科学与技术系, 北京 10008405,石刚，清华大学 计算机科学与技术系, 北京 100084 ;新疆大学 信息科学与工程学院, 新疆 乌鲁木齐 83004606,闫鑫，清华大学 计算机科学与技术系, 北京 100084 ;太原理工大学 计算机学院, 山西 太原 03002107

摘要：Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.

关键词：同步数据流语言;形式化验证;高阶运算;定理证明

基金资助：国家自然科学基金(61272086); 国家科技支撑计划(2013BAB05B05)