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

1、L2C編譯器簡介

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

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

2、源語言的特性

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

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

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

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

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

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

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

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

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

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

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

高性能嵌入式仿真軟件SkyEye

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

新一代全數字仿真平臺SkyEye

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

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

---

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

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

總結

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

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