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

版塊 |鑒源論壇 · 觀模

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

01

摘要

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

02

航空領(lǐng)域的應(yīng)用背景

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

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

03

形式化方法的解決方案

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

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

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

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

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

04

應(yīng)用案例

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

4.1 模式邏輯概述

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

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

圖2 Non-Arming Mode

2. 布防模式（Arming Mode）：該模式有三個狀態(tài)：ARMED、ACTIVE和SELECTED。ARMED和ACTIVE是SELECTED狀態(tài)的子狀態(tài)，即當(dāng)模式處于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)，即為飛行導(dǎo)引和自動駕駛系統(tǒng)生成指令。

圖4 Capture/Track Mode

4.2 模型檢查案例目標(biāo)

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

表1 軟件驗證目標(biāo)

4.3 模型檢查工具和方法

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

驗證流程：

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

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

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

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

驗證結(jié)果：

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

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

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

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

圖6 模型檢查得到的反例

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

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

主要參考文獻：

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 lattice model 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.

審核編輯 黃宇