可信编译器L2C的核心翻译步骤及其设计与实现

发布时间：2018-05-04 17:06

  本文选题：经过验证的编译器 + 同步数据流语言　； 参考：《软件学报》2017年05期

【摘要】：同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.
[Abstract]:Synchronous data flow languages, such as Lustrea, have been widely used in recent years in aviation, high-speed rail, nuclear power and other safety concerns. These areas have quite high requirements for the security of the related development tools themselves. In order to solve the problem of "false compilation", the construction and verification of conventional imperative language compilers have been realized with the aid of reliable-by-construction auxiliary theorem prover recently, and great success has been achieved. For example, Comp Cert C compiler. L2C is a trusted compiler based on this method. It takes the extended Lustre language as the source language and the C language subset in Clight(Comp Cert as the target language. L2C is a synchronous data flow language compiler for practical industrial applications. This paper mainly introduces the core translation steps of L2C compiler, the main problems and relevant experiences in the design and implementation of L2C compiler.
【作者单位】： 清华大学计算机科学与技术系;
【基金】：国家自然科学基金(90818019,61462086) 国家科技重大专项(MJ-2015-D-066) Sino-European Laboratory of Informatics,Automation and Applied Mathematics资助项目~~
【分类号】：TP314

【参考文献】

相关期刊论文 前2条

1 杨志斌;赵永望;黄志球;胡凯;马殿富;Jean-Paul BODEVEIX;Mamoun FILALI;;同步语言的时间可预测多线程代码生成方法[J];软件学报;2016年03期

2 石刚;王生原;董渊;嵇智源;甘元科;张玲波;张煜承;王蕾;杨斐;;同步数据流语言可信编译器的构造[J];软件学报;2014年02期

【共引文献】

相关期刊论文 前7条

1 谷伟卿;张智慧;白涛;齐敏;;可信编译器中地址不相交的保持性证明[J];自动化博览;2017年04期

2 尚书;甘元科;石刚;王生原;董渊;;可信编译器L2C的核心翻译步骤及其设计与实现[J];软件学报;2017年05期

3 方伟;周彰毅;;SCADE在航空发动机FADEC软件开发中的应用[J];航空发动机;2016年05期

4 彭彦彬;田野;彭新光;;一种端到端的医疗无线体域网轻量认证协议[J];计算机工程;2017年06期

5 杨志斌;黄志球;;面向安全关键嵌入式软件工程的“编译原理”课程教学探索[J];工业和信息化教育;2016年03期

6 杨志斌;赵永望;黄志球;胡凯;马殿富;Jean-Paul BODEVEIX;Mamoun FILALI;;同步语言的时间可预测多线程代码生成方法[J];软件学报;2016年03期

7 刘洋;甘元科;王生原;董渊;杨斐;石刚;闫鑫;;同步数据流语言高阶运算消去的可信翻译[J];软件学报;2015年02期

【二级参考文献】

相关期刊论文 前2条

1 石刚;王生原;董渊;嵇智源;甘元科;张玲波;张煜承;王蕾;杨斐;;同步数据流语言可信编译器的构造[J];软件学报;2014年02期

2 杨志斌;皮磊;胡凯;顾宗华;马殿富;;复杂嵌入式实时系统体系结构设计与分析语言:AADL[J];软件学报;2010年05期

【相似文献】

相关期刊论文 前1条

1 ;可跟踪L2C信号的RTKGPS接收机[J];全球定位系统;2004年06期

相关硕士学位论文 前1条

1 高娟娟;GPS L2C捕获算法研究与实现[D];南京邮电大学;2014年

，

本文编号：1843857