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

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

【部分圖文】：

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

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

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

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

圖3Velus架構(gòu)圖

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

本文編號(hào)：3951250