隨著計算機控制系統在人們生活中的普及,軟件自身的可靠性也越來越受到重視.在航空、高鐵、核電及軍事等高安全要求領域的軟件系統——安全關鍵系統(safety-critical system,簡稱SCS)更是受到高度的重視.而隨著軟件系統的復雜度越來越高,軟件系統的安全性保證也變得越來越困難.這些系統的開發,僅僅依靠過程規范、代碼審核和系統測試來保證軟件安全還遠遠不夠,通常需要采用形式化驗證方法來保證軟件可靠性.全數字實時仿真平臺SkyEye的同步數據流語言可信編譯器的構造在某些安全性嚴格要求的領域,不但對目標系統的開發需要形式化方法來保證,而且開發過程所需工具,如編譯器等,也必須經過形式化驗證.

同步模型與同步數據流語言

工業生產中的很多實時系統(如控制系統)都是響應系統,它是以環境決定的速率對環境做出連續響應的系統.此環境可以隨時提供新的輸入,系統通過運算產生新的輸出,使得程序不斷地與環境進行交互,且以并發的方式體現.

同步模型是為了適應響應系統而開發的程序運行模型.它把響應系統分成連續的原子時間片(響應周期),每個時間片又分成事件采集、邏輯運算和事件發射這3個階段,從而有效地滿足響應系統的要求.在同步模型中,事件的采集、邏輯運算和事件的發射必須在同一個響應周期內完成,這稱為同步模型的同步假設.時間片的大小是由響應系統的環境決定的.同步假設的有效性檢查,就是評估系統對環境的最大響應時間能否滿足環境要求.圖 1為同步模型示意圖.

編譯器的可信

對于編譯器來說,可信的具體指標就是其正確性,要保證從源程序到目標程序的翻譯過程正確,即,保證源語言的特征被正確、完整地實現,能夠實現語義保持性,杜絕誤編譯.

為了保障編譯器實現的正確性,傳統的方法是通過大量的測試.例如,GCC(4.7版)的torture測試集包含2 853個C源程序用例,商用的Plum Hall Standard Validation Suite for C有29 424個用例,Lustre V6的開源軟件包中含有140個左右的源程序用例,等等.還有一些Bug-hunting工具(如Csmith)可能產生更多或更獨特的源程序用例.

然而和其他軟件一樣,通過測試只能發現錯誤,并不能保證編譯器是正確的.Scade工具的代碼生成器KCG或許是獲得民用航空軟件生產許可的第一個商用編譯器,其設計開發過程(很嚴格的V&V過程)符合民航電子系統的國際標準DO-178B,并成功應用于空客(airbus)A340和A380的設計中.盡管如此,這并不足以說明Scade的編譯器不存在“誤編譯”.事實上,業界已經發現Scade KCG的某些翻譯漏洞.

為增加編譯器的安全和可信程度,僅通過測試和嚴格的過程管理都是不夠的,人們很自然地會想到形式化驗證的途徑.在CC(common criteria)安全評估標準中,將可信性分為7個級別(EAL1~EAL7),級別越高,形式化規范和驗證的程度越高.航空無線電委員會(RTCA)近期也已推出民航電子系統的國際標準DO-178C,與DO-178B相比,增加的內容包括了對形式化規范和驗證的要求.

人們在幾十年前就開展了編譯器形式化驗證的工作:McCarthy等人在1967年手工證明了一個簡單編譯器(從算術表達式翻譯到棧式機目標代碼)的正確性;隨后,Milner等人在1972年給出了相應的機械化證明;Dave于2003年的綜述列舉了從1967年~2003年的大部分相關工作,包含從針對簡單語言的單遍編譯器到較成熟的代碼優化遍等形形色色的工作.近年來,隨著技術的不斷進步,已經可以驗證較為復雜的編譯器.例如,Leroy等人開發的驗證過的C編譯器CompCert,Chlipala給出一個從非純函數式的語言到匯編語言的一個經過驗證的編譯器,Klein等人驗證了一個從Java核心子集到Java虛擬機的編譯器.

CompCert編譯器是經過驗證的可信編譯器的杰出代表.該編譯器將C的一個重要子集Clight翻譯為PowerPC匯編代碼(目前也支持IA32后端),使其可以直接用于范圍廣泛的嵌入式應用開發.該編譯器包含了許多分析與優化,所生成的代碼可與gcc-0產生的代碼匹敵.該編譯器將編譯過程劃分為多個階段,每個階段的翻譯正確性(語義保持性)都借助輔助定理證明器Coq進行了證明,且這些證明可由獨立的證明檢查器檢查,這使得CompCert的中間層轉換過程達到了我們所能期望的最高可信程度.最近,Yang等人在關于Csmith的研究工作中對主流的C編譯器進行測試,共報告了325個bugs,其中包括Intel CC,GCC和LLVM等.在所比較的11種開源或商用的C編譯器中,CompCert表現較為突出,在6個CPU年中,其中間轉換過程沒有發現bugs.

編譯器驗證的另外一種可選方案是翻譯確認(translation validation).翻譯確認(translation validation)是 Pnueli等人首先提出來的.他們采用翻譯確認的方法來驗證同步數據流語言的翻譯(或編譯)過程,所給示范例子的源語言是Signal特征的多時鐘同步數據流語言,目標語言是C.翻譯確認的方法不是直接驗證翻譯程序,而是用統一的語義框架為某一翻譯過程的源和目標代碼建模,兩個模型之間定義一種求精(refining)等價關系,設計一種可自動證明二者等價性的分析程序(成功時可給出證明腳本,不成功時給出反例),再給出一種獨立的證明檢查器(proof checker),可最后確認翻譯的正確性.

在L2C項目中,我們選擇了對編譯器本身進行驗證.當源語言和目標語言的語義定義達到認可的程度時,原理上可以保證源程序的一般性質都可以保持到目標程序.與上述翻譯確認的做法相比,這是一種徹底的做法;而基于翻譯確認的方法往往只是關注部分性質的保持性(當然,也可以逐步逼近一般性質).然而,這項工作相當艱巨,正如前述Pouzet等人的項目,是一項長期的工作.然而,我們的考慮是:1) 實際中有值得這樣做的需求; 2) 如果在面向驗證的編譯器結構上下功夫,加強證明過程的局部化和模塊化研究,可減輕需要擴展和維護時的負擔;3) 在某些擴展和維護工作量過大的翻譯階段,還可以采用翻譯確認的方法作為補充,比如CompCert項目,也有個別階段采用了翻譯確認方案;4) CompCert項目的成功,告訴我們這一選擇的重要價值和可行性.

---

標題：全數字實時仿真平臺SkyEye的同步數據流語言可信編譯器的構造

鏈接：http://www.digiproto.com

總結

以上是生活随笔為你收集整理的全数字实时仿真平台SkyEye的同步数据流语言可信编译器的构造的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。