作者 |徐奕龍飛上?？匕部尚跑浖?chuàng)新研究院系統(tǒng)建模組

版塊 |鑒源論壇 · 觀模

社群 |添加微信號(hào)“TICPShanghai”加入“上?？匕?1fusa安全社區(qū)”

01

摘要

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

02

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

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

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

03

形式化方法的解決方案

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

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

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

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

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

04

應(yīng)用案例

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

4.1 模式邏輯概述

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

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

圖2 Non-Arming Mode

2. 布防模式（Arming Mode）：該模式有三個(gè)狀態(tài)：ARMED、ACTIVE和SELECTED。ARMED和ACTIVE是SELECTED狀態(tài)的子狀態(tài)，即當(dāng)模式處于ARMED或ACTIVE狀態(tài)時(shí)，它同時(shí)也處于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)引和自動(dòng)駕駛系統(tǒng)生成指令。

圖4 Capture/Track Mode

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

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

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

4.3 模型檢查工具和方法

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

驗(yàn)證流程：

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

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

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

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

驗(yàn)證結(jié)果：

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

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

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

圖5 模型檢查得到的錯(cuò)誤示例

圖6 模型檢查得到的反例

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

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

主要參考文獻(xiàn)：

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.

審核編輯 黃宇