###
Journal of Software:2015.26(2):332-347

同步数据流语言高阶运算消去的可信翻译
刘洋,甘元科,王生原,董渊,杨斐,石刚,闫鑫
(清华大学 计算机科学与技术系, 北京 100084;清华大学 计算机科学与技术系, 北京 100084 ;新疆大学 信息科学与工程学院, 新疆 乌鲁木齐 830046;清华大学 计算机科学与技术系, 北京 100084 ;太原理工大学 计算机学院, 山西 太原 030021)
Trustworthy Translation for Eliminating High-Order Operation of a Synchronous Dataflow Language
LIU Yang,GAN Yuan-Ke,WANG Sheng-Yuan,DONG Yuan,YANG Fei,SHI Gang,YAN Xin
(Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China ;School of Information Science and Engineering, Xinjiang University, Urumqi 830046, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China ;School of Computer Science, Taiyuan University of Technology, Taiyuan 030021, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3516   Download 2677
Received:July 05, 2014    Revised:October 31, 2014
> 中文摘要: Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.
Abstract:Lustre is a synchronous dataflow language widely used in safety critical industrial control system. Formal verification is efficient to improve the reliability of the compiler which translates Lustre to C. Based on this approach, this paper conducts a research on the trustworthy compiler for translating Lustre*(a Lustre-like language) to Clight (a subset language of C). The entire compiling process is divided into different stages to tackle the large difference between Lustre* and Clight. Each stage performs a specific translation task. This paper describes a translation algorithm which eliminates high-order operations. The implementation of translation process is assisted by theorem proving tool Coq, and a strict proof of correctness of the process is also provided.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61272086); 国家科技支撑计划(2013BAB05B05) 国家自然科学基金(61272086); 国家科技支撑计划(2013BAB05B05)
Foundation items:
Reference text:

刘洋,甘元科,王生原,董渊,杨斐,石刚,闫鑫.同步数据流语言高阶运算消去的可信翻译.软件学报,2015,26(2):332-347

LIU Yang,GAN Yuan-Ke,WANG Sheng-Yuan,DONG Yuan,YANG Fei,SHI Gang,YAN Xin.Trustworthy Translation for Eliminating High-Order Operation of a Synchronous Dataflow Language.Journal of Software,2015,26(2):332-347