安全攸關(guān)的嵌入式領(lǐng)域廣泛使用基于Lustre語言描述的圖形化邏輯。工程師通過圖形化邏輯建模工具編寫控制邏輯,再通過代碼生成器把控制邏輯轉(zhuǎn)換成可執(zhí)行代碼下裝到嵌入式設(shè)備中運(yùn)行。因此,如何保證代碼生成器生成代碼的正確性成為關(guān)注的焦點(diǎn)。通過測試等傳統(tǒng)方法來確保代碼生成器的正確性,其覆蓋率有限,無法完全解決誤編譯的問題;而把形式化方法用于開發(fā)代碼生成器,通過邏輯推理的方式證明代碼生成的正確性,將最大限度地解決誤編譯的問題,使其成為一個(gè)可信代碼生成器。本文首先分析了同步數(shù)據(jù)流語言Lustre的語法特征,然后介紹了Lustre語言可信代碼生成器的研究進(jìn)展和形式化開發(fā)方法,為開發(fā)應(yīng)用于嵌入式安全攸關(guān)領(lǐng)域的Lustre可信代碼生成器提供借鑒。

【文章頁數(shù)】：5 頁

【部分圖文】：

圖1帶有翻譯驗(yàn)證的代碼生成過程

在可信代碼生成器形式化驗(yàn)證領(lǐng)域，JohnMccarthy等人已經(jīng)做了大量工作[7-10]，但仍然無法自動(dòng)證明給定的優(yōu)化編譯器的目標(biāo)語言和源語言語義的一致性。如果不能證明代碼生成器本身的正確性，也許可以檢查每個(gè)編譯過程的正確性。這啟發(fā)了翻譯驗(yàn)證技術(shù)，翻譯驗(yàn)證的概念最早由Pnuel....

圖2對(duì)代碼生成器本身進(jìn)行證明的開發(fā)流程圖

另一種形式化開發(fā)可信代碼生成器的方法是對(duì)代碼生成器本身進(jìn)行證明。這是一種將源語言的語法、語義模型及其滿足規(guī)范的性質(zhì)抽象為邏輯公式，然后使用邏輯推理技術(shù)來證明其語義一致性的技術(shù)，是最嚴(yán)格的開發(fā)方式。這種方法和數(shù)理邏輯相聯(lián)系，常使用高階邏輯系統(tǒng)進(jìn)行形式化描述，可通過Coq[18]、I....

圖3Velus架構(gòu)圖

學(xué)術(shù)界做了許多關(guān)于Lustre語言特性的形式化研究，JakubiecL[24]等人在Coq中使用歸納類型定義了Lustre語言的一個(gè)子集；G.Hamon[25]等人研究了同步數(shù)據(jù)流語言Lucid的高階特性，并完成了Lucid時(shí)鐘演算；E.Gimenez等人在開發(fā)Scade3代碼....

本文編號(hào)：3951250