《面向航空關鍵系統的AADL轉換語義及其特性保持證明研究》是依託北京航空航天大學，由胡凱擔任項目負責人的面上項目。
基本介紹
- 中文名：面向航空關鍵系統的AADL轉換語義及其特性保持證明研究
- 依託單位：北京航空航天大學
- 項目負責人：胡凱
- 項目類別：面上項目
項目摘要,結題摘要,
項目摘要
航空航天等領域的嵌入式實時系統日趨複雜，由於分式結構以及模式變換、分區等機制的引入，給系統性質驗證和分析帶來了新的挑戰。AADL是近年提出來的一種嵌入式實時系統體系結構分析與設計語言國際標準。當前，AADL模型驗證、分析以及自動代碼生成，主要是採用模型轉換方式，而精確的轉換語義及其特性保持是模型轉換的基礎。課題提出了一種基於時間抽象狀態機(TASM)的AADL轉換語義方法，形式化刻畫AADL和時間抽象狀態機的抽象語法、類型系統及操作語義，使轉換語義更加精確、抽象；提出了一種基於定理證明器Coq的AADL特性保持證明方法，採用Coq對AADL轉換語義進行重寫，提供通用的AADL語義基礎，並給出特性保持的證明；研究該轉換語義模型的可調度、資源最佳化等關鍵性質驗證和分析方法；最後，基於模型轉換語言ATL實現AADL模型到TASM模型的自動轉換，構建一體化的驗證與分析框架。
結題摘要
航空航天等領域的嵌入式實時系統是一種安全關鍵實時系統，如何設計與實現高質量的安全關鍵實時系統，是學術界和工業界共同面臨的難題。作為複雜嵌入式實時系統的體系結構設計與分析語言標準，AADL已成為一個新的研究熱點,而對AADL模型進行形式驗證與分析是實現高可信安全關鍵實時系統的一個關鍵環節。目前，模型轉換是AADL驗證與分析的主要途徑。其關鍵問題在於：（1）對AADL標準定義的語義是否有清晰和正確的理解；（2）AADL語義在模型轉換中是否得到保持；（3）用戶期望驗證的性質在模型轉換中是否得到保持。 本項目提出了一種新的AADL模型形式驗證與分析方法，重點研究了AADL形式轉換語義、AADL模型轉換的語義保持以及驗證性質保持證明（合稱為特性保持）方法三個關鍵問題，並設計和開發了一體化的AADL建模與驗證框架。主要研究成果如下： （1）提出了一種基於時間抽象狀態機（Timed Abstract State Machine，TASM）的AADL 形式轉換語義框架－AADL2TASM。針對一個較為完整的AADL研究子集，給出了研究子集的形式定義和抽象語法，給出了TASM 的抽象語法及其操作語義，並基於語義函式和類ML的元語言形式定義轉換語義規則。 （2）提出了一種基於雙版本形式語義的AADL 模型轉換的語義保持證明方法。給出了時間變遷系統TTS及其操作的定義；和形式轉換語義對應，基於TTS以操作語義的方式給出了相應AADL 研究子集的語義；同時，將轉換語義定義中的TASM表示和TASM語言本身的操作語義進行組合，構成TTS；最後，通過證明兩個TTS滿足模擬等價關係，證明了AADL研究子集的語義在AADL到TASM 的模型轉換中得到保持。為了提高證明的可信度，基於定理證明器Coq對相關定理進行了證明。 （3）提出了AADL模型到TASM模型的驗證性質保持證明方法。給出了考慮原子命題的時間變遷系統及其操作的定義；給出了時序邏輯ACTL、ECTL的語法和語義；給出了一種比較通用的驗證性質保持的證明思路，基於結構歸納法，從而整個性質得到保持。因此，使用時序邏輯表達的無死鎖性、安全性、實時性質以及資源性質能夠得到保持。同時，基於定理證明器Coq對相關定理進行了證明。 （4）在上述理論工作的基礎上設計並實現了 AADL 建模與驗證框架。同時，基於太空飛行器GNC系統中的子系統進行了實例性驗證。
