| 引用本文: | 石刚,王生原,董渊,嵇智源,甘元科,张玲波,张煜承,王蕾,杨斐.同步数据流语言可信编译器的构造.软件学报,2014,25(2):341-356 |
| |
|
| 本文已被：浏览 7532次 下载 10736次 |
码上扫一扫！ |
|
|
| 同步数据流语言可信编译器的构造 |
|
石刚1,2, 王生原1, 董渊1, 嵇智源3, 甘元科1, 张玲波1, 张煜承1, 王蕾1, 杨斐1
|
|
1.清华大学 计算机科学与技术系,北京 100084;2.新疆大学 信息科学与工程学院,新疆 乌鲁木齐 830046;3.科技部 高技术研究发展中心,北京 100044
|
|
| 摘要: |
| 同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而，此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的，有望最大限度地解决误编译问题.基于这种方法，开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异，源语言具有时钟同步、数据流、并发及流数据对象等特征，而目标语言则具有顺序控制流特征.同类研究中，目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程，相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作. |
| 关键词: 同步数据流语言 经过验证的编译器 形式化验证 形式语义 定理证明 |
| DOI：10.13328/j.cnki.jos.004542 |
| 分类号: |
| 基金项目:国家自然科学基金（61170051, 61272086, 90818019） |
|
| Construction for the Trustworthy Compiler of a Synchronous Data-Flow Language |
|
SHI Gang1,2, WANG Sheng-Yuan1, DONG Yuan1, JI Zhi-Yuan3, GAN Yuan-Ke1, ZHANG Ling-Bo1, ZHANG Yu-Cheng1, WANG Lei1, YANG Fei1
|
|
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.High Technology Research and Development Center, Ministry of Science and Technology, Beijing 100044, China
|
| Abstract: |
| Synchronous data-flow languages have been widely used in safety-critical industrial areas such as airplanes, high-speed railways, nuclear power plants, and so on. However，the safety of development tools themselves for this kind of languages has become one of the potential safety problems which have been highly focused on. It has proved to be successful to implement the construction and verification of a conventional language compiler using an assistant theorem prover, and it is expected to have the opportunity in solving the miscompilation problem to the utmost extent. Based on such an approach, the key technologies for a trustworthy compiler from a synchronous data-flow language (Lustre as the prototype) to a sequential imperative language (C as the prototype) have been studied. The challenge lies in the great difference between the source and target languages, where the source language has the features of clock synchrony, data-flow, concurrency, stream data object, etc., while the target language is instead with the sequential and control-flow features. Among the similar researches, there is no reported result so far for the key translation stages. Recently, this research completed a formal verification for the whole compilation stages in the case of single clock. The related technologies will be taken into the development of a safety-level compiler in the country’s nuclear power system. The paper presents a survey on the trustworthy compiler with the research background, the architecture, the key technologies, the current status, and the future work. |
| Key words: synchronous data-flow language verified compiler formal verification formal semantics theorem proving |
