作者 |徐奕龍飛上海控安可信軟件創(chuàng)新研究院系統建模組

(資料圖)

版塊 |鑒源論壇· 觀模

社群 |添加微信號“TICPShanghai”加入“上海控安51fusa安全社區(qū)”

01

摘要

本文主要探討了形式化方法在航空領域中的工業(yè)應用。航空領域作為安全攸關領域，其機載系統軟件的開發(fā)有著高度復雜和嚴格的安全標準要求，以確保其安全可靠性。但是由于機載系統軟件功能的增加，軟件系統規(guī)模增大，系統整體更為復雜，使得傳統方法難以滿足飛行控制系統的驗證需求。為解決航空領域的痛點，形式化方法成為一種有效的解決方案。形式化方法是一種基于數學和形式邏輯的工程方法，可用于系統設計、驗證和分析。形式化方法的應用有助于確保飛行安全性、提高飛機性能和優(yōu)化飛行控制系統。

02

航空領域的應用背景

在航空領域，飛行控制系統軟件是核心的組成部分，對整個航空器起著決定性的作用，其安全性和可靠性對航空器的正常運行有著至關重要的作用，一旦軟件出現故障，其造成的損失將會十分巨大。然而由于現代飛行控制系統軟件非常復雜，涉及到軟件和硬件的協同交互，傳統的測試方法不僅需要耗費大量的人力資源和時間成本，還難以做到覆蓋所有可能的情況，從而徹底規(guī)避安全隱患。這就使得在系統軟件開發(fā)的流程中存在著需求或系統設計出現問題的風險。歷史上，由于此類問題而造成的重大損失的災難事故觸目驚心。2007年，美國空軍戰(zhàn)斗機F-22的飛控軟件設計時未考慮時差因素, 在跨越國際日期變更線時飛行員變更系統時間致使飛控系統鎖死；2018年和2019年兩架飛機由于飛行控制軟件中反失速系統機動特性增強系統(MCAS)的缺陷發(fā)生了墜機事故導致總共三百余人死亡。

人類航空史上血淚的教訓促成了適航審定標準的不斷完善。為了更好地保障機載軟件的安全性和正確性，航空領域提出了DO-333標準。DO-333標準由RTCA專委會（航空無線電技術委員會）和EUROCAE工作組（歐洲民用航空設備組織）撰寫，并已于2011年12月13日由RTCA程序管理委員會（PMC）審定通過，名為"Formal Methods Supplement to DO-178C and DO-278A"。其中DO-178C是航空領域的飛行器軟件開發(fā)標準，而DO-278A是相關地面系統軟件的開發(fā)標準。而DO-333是對兩者的補充說明，旨在引導航空軟件開發(fā)團隊在軟件開發(fā)生命周期中應用形式化方法。DO-333中對原有DO-178C中給出的目標、活動、解釋性文字以及軟件生命周期過程數據進行某些改變與補充。這些更改和補充包括了若干用形式化語言描述的文檔，以及建立在這些形式化文檔基礎之上的形式化驗證佐證材料。為此，DO-333專門作出了針對性的增補和調整。DO-333適航標準中將軟件開發(fā)過程定義為四個環(huán)節(jié)，分別是軟件需求過程，軟件設計過程，軟件編碼過程和軟件繼承過程。并對各個軟件開發(fā)過程提出了驗證目標，并解釋了如何應用形式化方法于軟件開發(fā)的四個環(huán)節(jié)之中，闡述了其優(yōu)劣所在。該標準的提出說明了在安全攸關的航空領域，形式化方法在工程上提升機載軟件安全可靠性的能力得到了一定的認可，從而也引發(fā)了如何將其更好地應用于機載軟件的研發(fā)和認證過程之中的探討。

03

形式化方法的解決方案

形式化方法是建立在嚴格的數學基礎上的針對數字化系統進行規(guī)格說明撰寫、軟件開發(fā)、軟件驗證的技術。形式化的數學基礎主要包括形式邏輯、離散數學和機器可識別語言。形式化方法主要研究理念是工程人員希望通過合理的理論和工程方法特別是數學分析手段對軟件設計的健壯性和正確性進行嚴格的分析，找出人力審查難以發(fā)掘的軟件缺陷，滿足人們對高質量軟件可信的期望。形式化方法的主要特點是明確、無二義性的描述軟件系統的需求，通過軟件的形式化表達為軟件的一致性、準確性提供嚴格驗證。

形式化方法通常包含兩類關鍵技術，分別是形式化建模和形式化分析。其中兩者各自具有多種類型的實現技術。在形式化建模中，可以通過多種方法生成一個由無歧義的數學語法和語義定義的形式化模型，譬如說有形式化的圖形模型，這里圖的各個組件和他們之間的連接都有著嚴格的數學定義的語法和語義，比如SCADE工具中的狀態(tài)機就是典型的形式化圖形建模的案例。還有使用形式化建模語言描述的模型，例如Z語言、B方法、BIP。形式化分析方法可以歸為3類：1）演繹方法（deductive），如定理證明，2）模型檢查，3）抽象解釋。

1）演繹方法：涉及數學推理，即通過數學方法證明形式模型性質。性質的數學證明為軟件性質的正確性提供了嚴格證據。數學證明通常借助自動或交互式的定理證明系統。在一些情況下，即使借助定理證明系統，構建數學證明也會很困難，甚至無法構建。不過，一旦證明能構建成功，自動檢查證明的正確性將會變得很容易。

2）模型檢查：探索形式模型所有可能行為，從而判定指定性質是否成立。當性質不成立，模型檢查算法自動生成一個反例，以確定該性質在何處不成立以及不成立的原因。在一些情況下，模型檢查工具可能無法判定給定的性質是否成立。

3）抽象解釋：是一種構建程序語言語義的保守表示（conservative）的理論（保守表示以確?？煽啃裕?。實踐中，該技術針對無限狀態(tài)系統設計基于程序語義的分析算法，能靜態(tài)、自動及可靠地分析系統動態(tài)性質。借助相應的工具 ，抽象解釋為具體的性質產生形式模型。該技術可以看作部分地執(zhí)行計算機程序，在無需實際操作所有計算任務的同時，確定程序間的重要影響關系（如控制流結構，信息流，堆棧大小，時鐘周期的數目等）。

04

應用案例

本應用案例來源于" Formal methods case studies for DO-333."，該資料分享了形式化方法在航空航天領域中的案例研究。為了檢查系統規(guī)約是否滿足特定性質和要求，應用模型檢查來驗證飛行導引系統（FGS）單側模式邏輯的正確性。模式邏輯是飛行控制系統中的關鍵組成部分，它決定了飛機的導航和自動駕駛行為，其正確性對于確保飛行安全至關重要。在FGS中，模式邏輯相對復雜，但輸入和輸出僅有布爾值組成，這使得它適合使用模型檢查進行形式化驗證。

4.1 模式邏輯概述

模式指的是系統行為的互斥集合，對于FGS系統而言，模式對應于單個（或一組）FGS行為的系統配置，更貼切地說，FGS的模式就是其飛行控制法則的抽象，其模式邏輯主要包括三種不同類型的模式。

1. 非布防模式(Non-Arming Mode)：該模式只有CLEARED和SELECTED兩個實際狀態(tài)。如果由飛行機組手動請求或由FMS等子系統自動請求，模式被認為是SELECTED狀態(tài)，否則被認為是CLEARED狀態(tài)。

圖2 Non-Arming Mode

2. 布防模式（Arming Mode）：該模式有三個狀態(tài)：ARMED、ACTIVE和SELECTED。ARMED和ACTIVE是SELECTED狀態(tài)的子狀態(tài)，即當模式處于ARMED或ACTIVE狀態(tài)時，它同時也處于SELECTED狀態(tài)。

圖3 Arming Mode

3. 捕獲/跟蹤模式（Capture/Track Mode）：該模式相比前一模式在ACTIVE中區(qū)分了捕獲和跟蹤狀態(tài)。CAPTURE和TRACK狀態(tài)都是ACTIVE狀態(tài)的子狀態(tài)，并且模式的飛行控制法則在這兩種狀態(tài)下都處于ACTIVE狀態(tài)，即為飛行導引和自動駕駛系統生成指令。

圖4 Capture/Track Mode

4.2 模型檢查案例目標

本案例的目標是對FGS單側的模式邏輯進行形式化驗證，以確保它滿足規(guī)約中的要求和飛行控制法則。使用模型檢查來執(zhí)行與軟件設計過程的輸出相關的驗證活動，重點關注 DO-178C 中表 A-4 和 DO-333 中表 FM.A-4 的目標。這些驗證活動的目的是檢測軟件設計過程中可能引入的任何錯誤（DO-178C 第 5.2 節(jié)）。具體來說，本案例將驗證FGS一側模式邏輯的低層軟件需求，并表明軟件架構和低層軟件需求符合高層軟件需求。其詳細驗證目標如表1所示。

表1 軟件驗證目標

4.3 模型檢查工具和方法

在本案例中，使用了兩種主要的模型檢查器：隱式狀態(tài)BDD模型檢查器（如NuSMV）和SMT模型檢查器（如Kind）。這兩種模型檢查器分別適用于不同類型的規(guī)約和驗證需求。

驗證流程：

1. 首先，將FGS的模式邏輯描述轉化為模型檢查器可接受的形式，例如Lustre形式的規(guī)范語言。

2. 確定并規(guī)定模式邏輯的各種狀態(tài)和狀態(tài)轉換。

3. 編寫規(guī)約和性質規(guī)范，涵蓋所有目標驗證要求。

4. 使用模型檢查器對規(guī)約和性質進行驗證，以查找可能的錯誤和反例。

驗證結果：

通過模型檢查器的驗證，得到模式邏輯是否滿足規(guī)約和飛行控制法則的結果。如果模型檢查器找到了錯誤或反例，開發(fā)團隊可以進行修正，重新驗證，直到所有目標都得到滿足。最終使用Kind模型檢查器驗證FGS模型的模態(tài)邏輯時，發(fā)現了共十六個錯誤。

模型檢查發(fā)現的錯誤示例：

下面我們詳細闡述如何使用模型檢查工具發(fā)現錯誤的過程，圖5是一個非常簡單但是常見的命名錯誤，在退出ACTIVE模式時，輸出變量LGA_Active（正確情況應該是VGA_Active）被設置為false。通過Kind模型檢查器檢測到了這個錯誤。Kind模型檢查器產生的反例如圖6所示。

圖5 模型檢查得到的錯誤示例

圖6 模型檢查得到的反例

該反例共有3個步長，顯示了每一步的相關輸入和輸出的值。未發(fā)生變化的值用灰色文本顯示?；疑尘皹顺隽俗钪匾闹?，以幫助讀者理解反例。在初始步驟中，ROLL_Active模式如預期一樣處于活動狀態(tài)。在第二步中，按下GA開關，激活了LGA模式。這同時激活了VGA模式。在第三步中，VS_Pitch_Wheel_Rotated激活，清除VGA模式，即從ACTIVE轉變?yōu)镃LEARED狀態(tài)，但是，實際上在第三步中并沒有清除LGA模式，但由于命名錯誤，輸出變量LGA_Active卻被錯誤地設置為false。

綜上，形式化方法在航空領域已經開始受到越來越多的重視，并逐漸進入相關評審流程中。通過工業(yè)界實際的應用，形式化方法展現出了其在提高機載軟件系統安全性和可靠性方面的價值。通過形式化方法，我們可以在軟件開發(fā)生命周期的不同階段，精確地定義系統規(guī)范和性質，并自動化地驗證系統的正確性。形式化方法的發(fā)展將持續(xù)推動航空領域軟件開發(fā)的創(chuàng)新和進步，為飛行安全提供更加可靠的保障。通過不斷深入研究和實踐，形式化方法將在航空領域繼續(xù)發(fā)揮重要作用，為飛行控制系統的安全性和可靠性提供持續(xù)支持。未來，我們將繼續(xù)介紹更多形式化方法的技術細節(jié)和更多的應用案例。

主要參考文獻：

1. RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A (December 2011)

2. Cofer D, Miller S P. Formal methods case studies for DO-333[R]. 2014.

3. Platzer A, Quesel J D. European Train Control System: A case study in formal verification[C]//International Conference on Formal Engineering Methods. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009: 246-265.

4. Clarke E M. Model checking[C]//Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17. Springer Berlin Heidelberg, 1997: 54-56.

5. Cousot P, Cousot R. Abstract interpretation: a unified latticemodel for static analysis of programs by construction or approximation of fixpoints[C]//Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1977: 238-252.審核編輯 黃宇

關鍵詞：