《航電系統軟體可靠性的形式化驗證技術研究》是依託南京航空航天大學，由陳哲擔任項目負責人的聯合基金項目。
基本介紹
- 中文名：航電系統軟體可靠性的形式化驗證技術研究
- 項目類別：聯合基金項目
- 項目負責人：陳哲
- 依託單位：南京航空航天大學
項目摘要,結題摘要,
項目摘要
確保民用飛機航電系統軟體的可靠性與安全性是現代航電系統開發中面臨的重大挑戰。根據國際權威的適航認證標準DO-178C，為了確保航電軟體的可靠性與安全性，要求使用形式化驗證方法和基於模型的驗證方法。本項目主要針對航電軟體的領域特徵，研究模型檢驗和運行時驗證這兩種主流的形式化驗證技術：首先提出一種新的針對航電軟體模型和代碼的形式化規約語言，用於準確描述UML、SysML、AADL、Lustre等航電軟體模型和嵌入式C程式必須滿足的正確性性質；然後通過理論分析，證明新的規約語言的可判定性、可監測性和表達能力，以期獲得比現有規約語言更有航電軟體領域特徵、表達能力更強的規約語言；最後，在軟體模型層次和代碼層次上，針對該規約語言設計形式化驗證算法及其反例生成算法，並開發驗證工具，從而實現覆蓋航電軟體開發過程的全面驗證，提升驗證的自動化程度，減少軟體缺陷，提高軟體質量，並為適航認證提供有力的技術支持。
結題摘要
確保民用飛機航電系統軟體的可靠性與安全性是現代航電系統開發中面臨的重大挑戰。根據國際權威的適航認證標準DO-178C，為了確保航電軟體的可靠性與安全性，要求使用形式化驗證方法和基於模型的驗證方法。本項目主要針對航電軟體的領域特徵，研究模型檢驗和運行時驗證這兩種主流的形式化驗證技術。本項目的主要研究內容和重要結果包括： （1）我們提出了一種新的規約語言，用於準確描述航電軟體必須滿足的正確性性質，用戶可以方便地針對程式中的事件定義基於線性時序邏輯和模式語言的形式化規約，該規約語言為用戶提供了一種與驗證工具互動、可以方便而準確地表達待驗證性質的方式； （2）我們提出並實現了規約語言的可滿足性和可監測性判定算法，並證明了針對正則語言的參數化運行時驗證問題的計算複雜度為NP完全的，解決了規約語言判定算法和驗證問題計算複雜度方面的若干開放問題； （3）我們研究了針對Lustre模型的模型檢驗算法。我們可以通過實現顯式狀態模型檢驗算法生成模型的狀態空間，然後使用偏序約減技術在驗證過程中對狀態空間進行約減；也可以將模型轉化為邏輯公式，然後調用SAT/SMT求解器對邏輯公式求解，得到驗證結果； （4）我們研究了針對C代碼的運行時驗證算法，被驗證的正確性性質包括通用性質和用戶自定義性質，該算法可以用於構造C程式的運行時驗證工具，套用於對航電軟體代碼的驗證，提升驗證的自動化程度，減少軟體缺陷，提高軟體質量； （5）本研究展示了模型檢驗對機載軟體適航認證的支持，例如提供證據證明高級需求與低級需求的一致性、低級需求與軟體模型的一致性、以及軟體模型與代碼的一致性，可以為機載軟體的安全性保障和DO-178C/DO-333適航認證提供技術支持；我們提出使用源到源的轉換來實現動態分析工具，由於插樁後檔案是原始碼形式，因此可以依照DO-178C的標準對它進行代碼審查、分析和驗證，從而達到適航認證的要求。
