為了滿足國內(nèi)某安全攸關領域的需求, L2C編譯器的開發(fā)始于2010年9月, 其目標是設計實現(xiàn)一個經(jīng)過形式化驗證的可信編譯器, 其源語言是面向領域的同步數(shù)據(jù)流語言Lustre*(Lustre語言的一個變種, 參考下一節(jié)), 目標語言是C, 最終可用作相關領域數(shù)字化儀控系統(tǒng)的安全級代碼生成器.國產(chǎn)主可控的嵌入式仿真測試軟件SkyEye與可信編譯器L2C的核心翻譯步驟及其設計與實現(xiàn)。國產(chǎn)主可控的嵌入式仿真測試軟件SkyEye與可信編譯器L2C的核心翻譯介紹

1、L2C編譯器簡介

L2C編譯器的發(fā)展進程可歸為3個里程碑.一個是面向Lustre的一個核心子集, 設計實現(xiàn)了L2C編譯器的一個原型系統(tǒng), 于2013年6月完成驗收.另一個里程碑是已實現(xiàn)除嵌套時鐘外Lustre全部特性的一個單時鐘L2C編譯器版本, 完全能夠滿足國內(nèi)該安全攸關領域目前的實際應用需求, 并于2015年4月完成嚴格的企業(yè)級驗收, 這些工作的相關技術(shù)和代碼已在實際應用中發(fā)揮作用.

在上述第2個里程碑之后, 項目組對L2C編譯器的設計框架進行了較大程度的優(yōu)化調(diào)整, 目標是拓展應用領域以及開源系統(tǒng)的建設.目前, L2C編譯器進入了第3個里程碑的發(fā)展階段, 其目標是在目前面向企業(yè)的版本 (不開源) 基礎上裁減并適當改造, 形成了覆蓋Lustre V6^[19]全部特性的可開源版本.目前, 這一L2C編譯器的單時鐘版本 (L2C-MC) 已經(jīng)開放源碼 (https://github.com/l2ctsinghua/l2c/releases/tag/version-0.8), 支持嵌套時鐘的版本處于測試與完善的周期, 其源碼不久也將開放.

2、源語言的特性

L2C編譯器的不同版本, 其源語言 (Lustre*) 可能有所不同, 本文以目前支持的最多特性為準.Lustre*覆蓋了Lustre V6的全部特性, 并且根據(jù)實際應用的需求在此基礎上有許多擴展, 特別是在高階運算方面比Lustre V6更加豐富.

圖1展示一個簡單的Lustre程序, 可見, 一個Lustre程序 (program) 由多個節(jié)點 (node) 組成, 節(jié)點中包含輸入?yún)?shù) (parameters)、輸出參數(shù) (returns) 和函數(shù)體 (body), 其中函數(shù)體又由局部變量 (local variables) 和等式 (或語句) 序列組成, 結(jié)構(gòu)清晰.

下面以圖1示的Lustre程序為例來闡述Lustre的某些重要語言特性, 并且在圖2中給出圖1中主節(jié)點Main的一組合理輸入與輸出來直觀展示Lustre*語言的這些特性.

(1) 流數(shù)據(jù)對象.圖 2展示的輸入輸出很直觀地體現(xiàn)了Lustre程序區(qū)別于C語言程序的一個很重要的特性, 即在Lustre中每一個變量都是一個無窮長的流 (stream) 數(shù)據(jù)對象, 而不僅僅是一個單個的值.每一個周期 (cycle), 變量都可能會有不同的值或者沒有值, 其中圖 2截取了輸入輸出前10個周期的值, 后面還有無窮個周期.雖然每個周期的值可能會變化, 但處理邏輯每個周期都一樣, 如圖 1所示的主節(jié)點Main的代碼邏輯, 每個周期都一樣.Lustre*是同步語言的一種, 所有同步語言均滿足同步假設:當前周期的輸入時間出現(xiàn)時, 系統(tǒng)能夠在下個周期的輸入時間出現(xiàn)之間計算出當前周期的輸出.這一重要的同步假設使得同步語言在嵌入式實時控制系統(tǒng)中得到大規(guī)模應用.

(2) 數(shù)據(jù)流并發(fā)性.不同于C程序, Lustre程序具有數(shù)據(jù)流并發(fā)性, Lustre節(jié)點中的等式 (相當于語句) 雖然在書寫時有先后順序, 但都是并發(fā)執(zhí)行的.更復雜的情況是, Lustre程序中的等式 (或語句) 之間存在因果關系, 所以在并發(fā)執(zhí)行時還需要考慮等式 (或語句) 間的拓撲關系.如圖 1中第7行~第8行所示, 這兩行就存在因果關系.第7行k*的賦值依賴于第8行執(zhí)行的結(jié)果, 所以第7行應該在第8行之后執(zhí)行.這里拓撲關系的具體含義可參見第4節(jié).

(3) 高階算子.Lustre支持如map, re等10多個高階算子, 這些高階算子可以很方便地操作數(shù)組對象, 在編寫程序時會更加便利.如圖 1中第10行所示的map算子, 以節(jié)點 (或稱函數(shù)) Max以及兩個數(shù)組x1和x2作為參數(shù), 返回另一個數(shù)組p*.語義上, 相當于并行執(zhí)行“p[i]=Max (x1[i], x2[i])”(i從0變到1).

(4) 時態(tài)與時鐘算子.由于Lustre的流數(shù)據(jù)對象特性, 語言提供了時態(tài)算子, 比如pre, fby, arrow (→) 等, 可以對流數(shù)據(jù)進行操作.另外, Lustre還支持嵌套的時鐘, 提供了可改變時鐘快慢的算子, 如when使時鐘變慢形成下一層嵌套的時鐘, 而current與merge使時鐘變快, 回到上一層嵌套時鐘.如圖 2所示, 使用when算子后, 主節(jié)點中y1的時鐘相對于x3的時鐘變慢了 (根據(jù)布爾量b取值為true時進行采樣); 使用了fby算子之后, 主節(jié)點中s相對于y1時鐘周期不變, 但每個周期的值向后shift了1個周期 (注意, 這里指相對于y1時鐘的shift, 即對應于b取值為true時的時鐘周期).

3、L2C編譯器的主體翻譯框架

隨著源語言 (Lustre*) 特性的增加以及不同開發(fā)階段的不同理念, L2C可信編譯器的翻譯框架也在不斷變化, 先后出現(xiàn)過接近10個穩(wěn)定的框架圖,?圖 3是其中最近的一個.國產(chǎn)主可控的嵌入式仿真測試軟件SkyEye與可信編譯器L2C的核心翻譯介紹

如圖 3所示, Lustre源程序經(jīng)過詞法、語法以及靜態(tài)語義分析 (類型檢查), 翻譯到類型良好的抽象語法樹 (abstract syntax tree, 簡稱AST) 形式的高級中間語言Well-typed Lustre AST代碼. Well-typed Lustre* AST代碼經(jīng)過一些簡單的預處理變換 (LustreSGen) 生成一種具有規(guī)范形式的中間語言LustreS代碼.預處理變換主要包括全局常量和類型的合并、拆分表達式列表、通過引入新變量提升某些特殊表達式 (如call和fby表達式) 至等式 (或語句) 級別等.

對于這部分的翻譯過程, 目前我們沒有去進行形式化驗證, 故在圖 3中用虛線箭頭來表示.詞法和語法分析算法或者相關的工具是比較成熟的, 比較可信, 但若要驗證它們的正確性卻是很困難的, 因此目前的可信編譯器 (包括CompCert) 基本上不驗證這一部分工作.此外, 其余的翻譯工作 (包括類型檢查) 相對比較簡單, 也比較容易驗證, 同時也因為它們是受Lustre*變化影響較大的部分, 所以我們在整個L2C可信編譯器的實現(xiàn)中將這部分驗證工作放在了最低的優(yōu)先級.另外, 這些翻譯過程的翻譯確認程序是比較容易實現(xiàn)的, 這也是我們不急于完成這部分驗證工作的重要原因之一.

高性能嵌入式仿真軟件SkyEye

隨著科技的發(fā)展，系統(tǒng)工程的設計體量逐漸龐大起來，尤其是對于軌道交通、航空航天、核電站等安全關鍵領域中，如何在復雜度逐年變大的同時保證其安全性和可靠性，是近年來各大公司需要研究的課題。最近比較火熱的基于模型的系統(tǒng)工程（MBSE）技術(shù)則給大家提供了一種全新的技術(shù)方向，分享一種全數(shù)字實時仿真的安全關鍵領域解決方案，提供一種新的解決思路。國產(chǎn)主可控的嵌入式仿真測試軟件SkyEye與可信編譯器L2C的核心翻譯介紹，提供高效的運算速度，提高研發(fā)效率和安全性。

新一代全數(shù)字仿真平臺SkyEye

基于模型的全數(shù)字研發(fā)解決方案MBSE工具軟件SkyEye是能夠滿足模擬或仿真外部硬件行為進行軟件運行和測試需求的工具。該工具運用國際流行的仿真、測試腳本語言來編寫外部硬件邏輯行為所產(chǎn)生外部激勵事件以構(gòu)成嵌入式軟件的外部信號激勵或數(shù)據(jù)輸入，從而滿足軟件在全數(shù)字仿真運行環(huán)境下無須人的干預而閉環(huán)運行的要求。國產(chǎn)主可控的嵌入式仿真測試軟件SkyEye與可信編譯器L2C的核心翻譯介紹

作為基于嵌入式應用的特點，嵌入式軟件全數(shù)字仿真測試支撐平臺SkyEye要為嵌入式系統(tǒng)提供全數(shù)字仿真測試環(huán)境或測試平臺，實現(xiàn)對嵌入式系統(tǒng)進行實時、閉環(huán)的系統(tǒng)測試。在該平臺上完成被測軟件的分析、運行和測試，最重要的是要實現(xiàn)嵌入式系統(tǒng)外部事件的全數(shù)字仿真平臺，使得嵌入式軟件就像在真實硬件環(huán)境下連續(xù)不中斷地運行。

---

本文標題：國產(chǎn)主可控的嵌入式仿真測試軟件SkyEye與可信編譯器L2C的核心翻譯介紹

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

總結(jié)

以上是生活随笔為你收集整理的国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。