| 同步数据流语言可信编译器的构造 |
| |
| 引用本文： | 石刚,王生原,董渊,嵇智源,甘元科,张玲波,张煜承,王蕾,杨斐.同步数据流语言可信编译器的构造[J].软件学报,2014,25(2):341-356. |
| |
| 作者姓名： | 石刚 王生原 董渊 嵇智源 甘元科 张玲波 张煜承 王蕾 杨斐 |
| |
| 作者单位： | 清华大学 计算机科学与技术系,北京 100084;新疆大学 信息科学与工程学院,新疆 乌鲁木齐 830046;清华大学 计算机科学与技术系,北京 100084;清华大学 计算机科学与技术系,北京 100084;科技部 高技术研究发展中心,北京 100044;清华大学 计算机科学与技术系,北京 100084;清华大学 计算机科学与技术系,北京 100084;清华大学 计算机科学与技术系,北京 100084;清华大学 计算机科学与技术系,北京 100084;清华大学 计算机科学与技术系,北京 100084 |
| |
| 基金项目： | 国家自然科学基金（61170051, 61272086, 90818019） |
| |
| 摘 要： | 同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而，此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的，有望最大限度地解决误编译问题.基于这种方法，开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异，源语言具有时钟同步、数据流、并发及流数据对象等特征，而目标语言则具有顺序控制流特征.同类研究中，目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程，相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.
|
| 关 键 词： | 同步数据流语言 经过验证的编译器 形式化验证 形式语义 定理证明 |
| 收稿时间： | 5/4/2013 12:00:00 AM |
| 修稿时间： | 2013/12/17 0:00:00 |
Construction for the Trustworthy Compiler of a Synchronous Data-Flow Language |
| |
| SHI Gang,WANG Sheng-Yuan,DONG Yuan,JI Zhi-Yuan,GAN Yuan-Ke,ZHANG Ling-Bo,ZHANG Yu-Cheng,WANG Lei and YANG Fei.Construction for the Trustworthy Compiler of a Synchronous Data-Flow Language[J].Journal of Software,2014,25(2):341-356. |
| |
| Authors: | SHI Gang WANG Sheng-Yuan DONG Yuan JI Zhi-Yuan GAN Yuan-Ke ZHANG Ling-Bo ZHANG Yu-Cheng WANG Lei and YANG Fei |
| |
| Affiliation: | 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;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;High Technology Research and Development Center, Ministry of Science and Technology, Beijing 100044, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China |
| |
| Abstract: | |
| |
| Keywords: | synchronous data-flow language verified compiler formal verification formal semantics theorem proving |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
