| 引用本文: | 刘洋,甘元科,王生原,董渊,杨斐,石刚,闫鑫.同步数据流语言高阶运算消去的可信翻译.软件学报,2015,26(2):332-347 |
| |
|
| 本文已被：浏览 6616次 下载 8896次 |
码上扫一扫！ |
|
|
| 同步数据流语言高阶运算消去的可信翻译 |
|
刘洋1, 甘元科1, 王生原1, 董渊1, 杨斐1, 石刚1,2, 闫鑫1,3
|
|
1.清华大学 计算机科学与技术系, 北京 100084;2.新疆大学 信息科学与工程学院, 新疆 乌鲁木齐 830046;3.太原理工大学 计算机学院, 山西 太原 030021
|
|
| 摘要: |
| Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明. |
| 关键词: 同步数据流语言 形式化验证 高阶运算 定理证明 |
| DOI：10.13328/j.cnki.jos.004785 |
| 分类号: |
| 基金项目:国家自然科学基金(61272086); 国家科技支撑计划(2013BAB05B05) |
|
| Trustworthy Translation for Eliminating High-Order Operation of a Synchronous Dataflow Language |
|
LIU Yang1, GAN Yuan-Ke1, WANG Sheng-Yuan1, DONG Yuan1, YANG Fei1, SHI Gang1,2, YAN Xin1,3
|
|
1.Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;2.School of Information Science and Engineering, Xinjiang University, Urumqi 830046, China;3.School of Computer Science, Taiyuan University of Technology, Taiyuan 030021, China
|
| 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. |
| Key words: synchronous dataflow language formal verification high-order operation theorem proving |
