本文選題：經(jīng)過驗證的編譯器 + 同步數(shù)據(jù)流語言　； 參考：《軟件學報》2017年05期

【摘要】：同步數(shù)據(jù)流語言(如Lustre)近年來在航空、高鐵、核電等安全攸關(guān)領(lǐng)域得到廣泛應(yīng)用.這些領(lǐng)域?qū)ο嚓P(guān)開發(fā)工具本身的安全性有著相當高的要求.為盡力解決好"誤編譯"問題,近期人們借助reliable-by-construction輔助定理證明器實現(xiàn)常規(guī)命令式語言編譯器的構(gòu)造和驗證,取得了很大的成功,如Comp Cert C編譯器.L2C是基于這種方法開發(fā)的可信編譯器.它以擴展的Lustre語言為源語言,以Clight(Comp Cert中的C語言子集)為目標語言.L2C是面向?qū)嶋H工業(yè)應(yīng)用的同步數(shù)據(jù)流語言編譯器.重點介紹L2C編譯器的核心翻譯步驟及其設(shè)計與實現(xiàn)過程中考慮的主要問題和相關(guān)經(jīng)驗.
[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.
【作者單位】： 清華大學計算機科學與技術(shù)系;
【基金】：國家自然科學基金(90818019,61462086) 國家科技重大專項(MJ-2015-D-066) Sino-European Laboratory of Informatics,Automation and Applied Mathematics資助項目~~
【分類號】：TP314

【參考文獻】

相關(guān)期刊論文 前2條

1 楊志斌;趙永望;黃志球;胡凱;馬殿富;Jean-Paul BODEVEIX;Mamoun FILALI;;同步語言的時間可預測多線程代碼生成方法[J];軟件學報;2016年03期

2 石剛;王生原;董淵;嵇智源;甘元科;張玲波;張煜承;王蕾;楊斐;;同步數(shù)據(jù)流語言可信編譯器的構(gòu)造[J];軟件學報;2014年02期

【共引文獻】

相關(guān)期刊論文 前7條

1 谷偉卿;張智慧;白濤;齊敏;;可信編譯器中地址不相交的保持性證明[J];自動化博覽;2017年04期

2 尚書;甘元科;石剛;王生原;董淵;;可信編譯器L2C的核心翻譯步驟及其設(shè)計與實現(xiàn)[J];軟件學報;2017年05期

3 方偉;周彰毅;;SCADE在航空發(fā)動機FADEC軟件開發(fā)中的應(yīng)用[J];航空發(fā)動機;2016年05期

4 彭彥彬;田野;彭新光;;一種端到端的醫(yī)療無線體域網(wǎng)輕量認證協(xié)議[J];計算機工程;2017年06期

5 楊志斌;黃志球;;面向安全關(guān)鍵嵌入式軟件工程的“編譯原理”課程教學探索[J];工業(yè)和信息化教育;2016年03期

6 楊志斌;趙永望;黃志球;胡凱;馬殿富;Jean-Paul BODEVEIX;Mamoun FILALI;;同步語言的時間可預測多線程代碼生成方法[J];軟件學報;2016年03期

7 劉洋;甘元科;王生原;董淵;楊斐;石剛;閆鑫;;同步數(shù)據(jù)流語言高階運算消去的可信翻譯[J];軟件學報;2015年02期

【二級參考文獻】

相關(guān)期刊論文 前2條

1 石剛;王生原;董淵;嵇智源;甘元科;張玲波;張煜承;王蕾;楊斐;;同步數(shù)據(jù)流語言可信編譯器的構(gòu)造[J];軟件學報;2014年02期

2 楊志斌;皮磊;胡凱;顧宗華;馬殿富;;復雜嵌入式實時系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言:AADL[J];軟件學報;2010年05期

【相似文獻】

相關(guān)期刊論文 前1條

1 ;可跟蹤L2C信號的RTKGPS接收機[J];全球定位系統(tǒng);2004年06期

相關(guān)碩士學位論文 前1條

1 高娟娟;GPS L2C捕獲算法研究與實現(xiàn)[D];南京郵電大學;2014年

，

本文編號：1843857