基于模型檢查的民用飛機(jī)飛控系統(tǒng)安全性評(píng)估

范基坪 洪驥宇

(上海飛機(jī)設(shè)計(jì)研究院，上海 201210)

0 引言

基于ARP 4754A[1]，ARP 4761[2]的傳統(tǒng)安全性評(píng)估流程在民用航空領(lǐng)域已經(jīng)得到了廣泛的應(yīng)用。然而，近20年來(lái)計(jì)算機(jī)科學(xué)與集成電路制造工藝的發(fā)展促使了產(chǎn)品機(jī)電系統(tǒng)的深度融合，嵌入式軟件控制方式逐漸代替?zhèn)鹘y(tǒng)的機(jī)械控制，系統(tǒng)復(fù)雜度急劇上升。傳統(tǒng)安全性評(píng)估流程嚴(yán)重依賴于安全分析人員的經(jīng)驗(yàn)，面對(duì)新型安全關(guān)鍵系統(tǒng)軟硬件深度集成，復(fù)雜度高的特征時(shí)，面臨著系統(tǒng)描述能力不足、分析結(jié)果不準(zhǔn)確、分析工作迭代困難等問(wèn)題[3-4]。

針對(duì)系統(tǒng)安全性研制流程中產(chǎn)生的新問(wèn)題，在系統(tǒng)工程思想指導(dǎo)下，一種面向基于模型的系統(tǒng)工程的新型安全性評(píng)估理念[5-8]——基于模型的安全性評(píng)估(Model-Based Safety Assessment, 簡(jiǎn)稱MBSA)，得到了學(xué)術(shù)界與工業(yè)界的廣泛認(rèn)可。在基于模型的安全性評(píng)估過(guò)程中，安全性要求的評(píng)估通過(guò)模型檢查等形式化方法自動(dòng)實(shí)現(xiàn)[9-10]。通過(guò)在安全性評(píng)估過(guò)程中引入形式化的模型與規(guī)范，將評(píng)估過(guò)程轉(zhuǎn)化為系統(tǒng)模型的規(guī)范驗(yàn)證過(guò)程。

本文采用當(dāng)前MBSA研究領(lǐng)域較為成熟的模型檢查方法，針對(duì)模型檢查的建模特點(diǎn)，基于SMV語(yǔ)言提出安全性建模與規(guī)約方法。以某延程型寬體客機(jī)飛控系統(tǒng)為對(duì)象，構(gòu)建該機(jī)型飛控系統(tǒng)的功能模型，并定義形式化的安全性要求，開展安全性評(píng)估，從而驗(yàn)證基于形式化方法的安全性評(píng)估在民機(jī)系統(tǒng)安全性工作中的可行性。

1 模型檢查的基本內(nèi)涵

模型檢查是形式化方法的重要分支[11]，基本思想是利用時(shí)態(tài)邏輯描述目標(biāo)系統(tǒng)所需滿足的性質(zhì)φ，有限狀態(tài)機(jī)(FSM)描述系統(tǒng)的狀態(tài)轉(zhuǎn)移關(guān)系s，以及模型檢查的算法遍歷FSM來(lái)檢驗(yàn)時(shí)態(tài)邏輯公式的正確性，即s╞φ，如圖1所示。對(duì)不滿足的系統(tǒng)規(guī)范，可以得到一個(gè)反例，說(shuō)明系統(tǒng)不滿足要求的狀態(tài)路徑。

圖1 模型檢查基本原理

模型檢查所構(gòu)建的系統(tǒng)模型往往并非目標(biāo)系統(tǒng)實(shí)際所采用的建模形式，因此必須將目標(biāo)系統(tǒng)轉(zhuǎn)換為某一模型檢查工具所支持的輸入形式。構(gòu)建系統(tǒng)模型時(shí)需要結(jié)合待驗(yàn)證的屬性對(duì)系統(tǒng)進(jìn)行必要的抽象和簡(jiǎn)化。建模時(shí)抽象度過(guò)高會(huì)導(dǎo)致模型與真實(shí)系統(tǒng)差別增大，導(dǎo)致驗(yàn)證工作漏掉某些真正的錯(cuò)誤，而抽象程度過(guò)低則會(huì)增加驗(yàn)證模型的復(fù)雜性，因此對(duì)模型抽象的過(guò)程在整個(gè)模型檢查過(guò)程中需要占用大量的時(shí)間。

1.1 有限狀態(tài)機(jī)

模型檢查中系統(tǒng)模型的有限狀態(tài)機(jī)稱為Kripke結(jié)構(gòu)。Kripke結(jié)構(gòu)是一種嚴(yán)格的數(shù)學(xué)結(jié)構(gòu)，是狀態(tài)轉(zhuǎn)移圖的一種變形，能夠很好地描述系統(tǒng)的狀態(tài)轉(zhuǎn)移及時(shí)序邏輯關(guān)系。典型Kriple結(jié)構(gòu)是一個(gè)五元組：

M=

其中：S是有限狀態(tài)集合，S0?S是初始狀態(tài)集合，R表示狀態(tài)轉(zhuǎn)移關(guān)系，R?S×S，L:S→2AP稱為標(biāo)記函數(shù)，用于標(biāo)記每個(gè)狀態(tài)中成立的所有原子命題集合，AP是所有原子命題與其否命題的集合，該集合是AP的一個(gè)子集。

在一個(gè)Kripke結(jié)構(gòu)M中，從任意某一狀態(tài)s開始產(chǎn)生的無(wú)限長(zhǎng)的狀態(tài)序列n=s0s1s2...被稱為該結(jié)構(gòu)中的一條路徑，該路徑中s0=s，對(duì)所有i≥0，都有R(si,si+1)成立。系統(tǒng)動(dòng)態(tài)運(yùn)行中的屬性通常描述為一系列原子命題的動(dòng)態(tài)滿足過(guò)程。

圖2左邊為一個(gè)簡(jiǎn)單Kripke結(jié)構(gòu)的示例，圓表示狀態(tài)，箭頭線代表狀態(tài)轉(zhuǎn)移關(guān)系，箭頭兩端的狀態(tài)及轉(zhuǎn)移的首位兩個(gè)狀態(tài)，沒有起始端的箭頭表示系統(tǒng)進(jìn)入初始狀態(tài)，狀態(tài)內(nèi)標(biāo)注的原子命題組成Kripke的標(biāo)記函數(shù)，當(dāng)某一狀態(tài)激活時(shí)，狀態(tài)內(nèi)的原子命題成立。

圖2 簡(jiǎn)單Kripke結(jié)構(gòu)示例

對(duì)于該Kripke結(jié)構(gòu)，S={so,s1,s2}，S0={so}，AP={a,b,c,a,b,c}，R={,,,}，L(s0)={a,b}，L(s1)={a,c}，L(s2)={b,c}，將系統(tǒng)狀態(tài)關(guān)系展開得到圖2右側(cè)所示結(jié)構(gòu)。

可以得出以下結(jié)論，Kripke結(jié)構(gòu)的狀態(tài)關(guān)系展開類似樹狀結(jié)構(gòu)，除去根節(jié)點(diǎn)外，每一節(jié)點(diǎn)僅有一個(gè)前端節(jié)點(diǎn)，可以任意訪問(wèn)其后端節(jié)點(diǎn)，從而構(gòu)成一棵無(wú)限深度的樹。

1.2 時(shí)態(tài)邏輯

時(shí)態(tài)邏輯公式是模型檢查中用于描述動(dòng)態(tài)系統(tǒng)屬性的形式化命題方法。常見的時(shí)態(tài)邏輯包括兩種：線性時(shí)態(tài)邏輯(linear temporal logic，簡(jiǎn)稱LTL)與計(jì)算樹邏輯(computation tree logic，簡(jiǎn)稱CTL)。

線性時(shí)態(tài)邏輯將系統(tǒng)時(shí)間定義為無(wú)限長(zhǎng)的時(shí)態(tài)序列，稱為計(jì)算路徑，當(dāng)前時(shí)刻存在唯一的下一時(shí)刻狀態(tài)，對(duì)于存在多種未來(lái)狀態(tài)的系統(tǒng)，利用一組路徑表示不同的時(shí)態(tài)序列。線性時(shí)態(tài)邏輯命題由時(shí)態(tài)算子與原子命題組成。常用時(shí)態(tài)邏輯算子包括：

G(Glabal)：未來(lái)所有狀態(tài)；F(Final)：未來(lái)某個(gè)狀態(tài)；X(neXt)：下一個(gè)狀態(tài)；U(Until)：直到…都；R(Release)：直到…才；W(Wait)：弱…直到。

線性時(shí)態(tài)邏輯無(wú)法描述多條路徑之間的相互關(guān)系，在描述分支并發(fā)系統(tǒng)時(shí)，采用計(jì)算樹邏輯描述系統(tǒng)時(shí)間特性。計(jì)算樹邏輯以Kripke初始節(jié)點(diǎn)為根節(jié)點(diǎn)，將Kripke結(jié)構(gòu)展開為無(wú)線樹形結(jié)構(gòu)，相比線型時(shí)態(tài)邏輯，計(jì)算樹定義路徑量詞A(對(duì)于所有路徑)與E(存在一條路徑)，且不存在時(shí)態(tài)算子R、W。

2 系統(tǒng)建模方法及安全屬性定義

2.1 系統(tǒng)模型構(gòu)建方法

不同模型檢查工具對(duì)應(yīng)不同的自動(dòng)機(jī)語(yǔ)言，構(gòu)建系統(tǒng)模型時(shí)需要根據(jù)特定語(yǔ)言的特點(diǎn)確定模型結(jié)構(gòu)與部件描述方式。以SMV為例，構(gòu)建系統(tǒng)SMV模型的基本步驟如下：

1)確定目標(biāo)系統(tǒng)的基本結(jié)構(gòu)，包括系統(tǒng)層次劃分與同一層次的部件，為每個(gè)部件及系統(tǒng)層級(jí)定義Module，按照系統(tǒng)自上而下結(jié)構(gòu)從模型main模塊開始逐層實(shí)例化。

2)根據(jù)部件內(nèi)部工作情況與部件間接口關(guān)系，定義各個(gè)模塊所需內(nèi)部變量及類型，確定每個(gè)模塊輸入變量。系統(tǒng)模型的狀態(tài)空間規(guī)模由變量數(shù)量決定，在定義變量過(guò)程中應(yīng)盡量減少冗余變量。

3)在每個(gè)模塊的ASSIGN及DEFINE部分定義系統(tǒng)行為。根據(jù)MBSA模型構(gòu)建的兩種策略，失效建模分為名義系統(tǒng)+故障注入以及直接失效行為兩種，圖3和圖4分別描述了兩種建模方式。名義系統(tǒng)+故障注入的方式將部件模型分為名義模塊nominal_comp與失效模塊failure_comp兩部分，在另一模塊extend_comp中實(shí)例化兩類模塊，根據(jù)部件狀態(tài)調(diào)用nominal_comp與failure_comp中參數(shù)值；直接故障行為描述則在同一模塊中同時(shí)定義正常與失效狀態(tài)輸出。

圖3 直接系統(tǒng)建模

2.2 安全屬性的定義

傳統(tǒng)安全性評(píng)估過(guò)程中，通過(guò)FHA確定初始安全性要求，并在研制流程中逐漸細(xì)化分解。模型檢查的驗(yàn)證與分析工作在原有研制流程基礎(chǔ)上開展，通用自動(dòng)化檢驗(yàn)是否滿足安全屬性來(lái)判斷系統(tǒng)的安全性水平。系統(tǒng)安全屬性的來(lái)源包括：FHA結(jié)論，初步故障樹結(jié)論及FMEA，前一階段模型檢查所得結(jié)論等。

將已知的安全性需求形式化表示為時(shí)態(tài)邏輯命題，要針對(duì)時(shí)態(tài)邏輯命題所涉及的部件，在模塊中定義相應(yīng)原子命題的標(biāo)識(shí)變量。以圖4為例，如果需要定義安全屬性為：部件在failure_mode1時(shí)value值不能低于5，利用CTL公式可以定義為：

AG (work=failure_mode1 >failure_comp.value>=5)

選擇CTL或者LTL的基本原則是依據(jù)命題的描述特性。對(duì)于存在類型的命題，例如證明系統(tǒng)能否到達(dá)某一狀態(tài)，可以采用CTL描述特性；對(duì)于強(qiáng)調(diào)狀態(tài)序列特性的問(wèn)題，例如某些狀態(tài)的先后次序，可以采用LTL描述。

圖4 名義系統(tǒng)建模+故障注入

3 某民用飛機(jī)案例驗(yàn)證

3.1 民機(jī)飛控系統(tǒng)

某民用飛機(jī)采用電傳+機(jī)械的組合控制模式，其功能控制模型是軟件、硬件、機(jī)電結(jié)構(gòu)高度綜合的復(fù)雜系統(tǒng)，以副翼控制功能為例，考慮影響副翼控制功能的飛控部件，簡(jiǎn)化飛控系統(tǒng)功能模型如圖5所示。

圖5 典型民用飛機(jī)飛控系統(tǒng)簡(jiǎn)化功能框圖

桿位移傳感器、慣性測(cè)量組件將動(dòng)作數(shù)據(jù)及測(cè)量數(shù)據(jù)輸入至飛控計(jì)算機(jī)，由飛控計(jì)算機(jī)解算得到的相應(yīng)控制信號(hào)經(jīng)伺服放大回路輸出值左右副翼舵機(jī)。28 V交流發(fā)電機(jī)與永磁發(fā)電機(jī)為飛控計(jì)算機(jī)供電。建立系統(tǒng)模型時(shí)，考慮飛機(jī)在AFCS、DDC、EFCS三種工作狀態(tài)下的部件接口關(guān)系差異，其中飛控計(jì)算EFCS板僅在EFCS模式下運(yùn)行，DDC模式下MBI與AIN板工作狀態(tài)對(duì)副翼控制功能無(wú)影響。根據(jù)系統(tǒng)描述構(gòu)建SMV模型，圖6所示為飛控計(jì)算機(jī)MBI板SMV模塊示例。

圖6 飛控計(jì)算機(jī)MBI板模型

定義系統(tǒng)安全屬性為左右副翼舵機(jī)不能同時(shí)進(jìn)入失效狀態(tài)，將命題形式化描述如下：

AG!(left_servo.status=failure&right_servo.status=failure)

3.2 NuSMV仿真

模型檢查在檢測(cè)系統(tǒng)規(guī)范時(shí)會(huì)遍歷系統(tǒng)狀態(tài)空間，基于BDD的NuSMV模型檢查器目前能夠支持2120的狀態(tài)空間，但是運(yùn)算時(shí)間會(huì)隨著系統(tǒng)狀態(tài)空間的擴(kuò)大迅速增加。因此在執(zhí)行系統(tǒng)規(guī)范的嚴(yán)格檢查之前，運(yùn)用仿真方式模擬系統(tǒng)狀態(tài)變化路徑，對(duì)系統(tǒng)行為進(jìn)行初步的分析。案例所建系統(tǒng)包含69個(gè)變量，系統(tǒng)可達(dá)狀態(tài)數(shù)達(dá)到263次。通過(guò)仿真尋找系統(tǒng)失效路徑，圖7所示為其中一條包含50個(gè)仿真步長(zhǎng)單位的系統(tǒng)失效路徑。

圖7 一條仿真狀態(tài)路徑

圖7所示的一條狀態(tài)路徑展現(xiàn)了一個(gè)特定失效場(chǎng)景，State1.1為系統(tǒng)初始狀態(tài)，飛控系統(tǒng)處于PFCS工作模態(tài)，部件運(yùn)行正常，State1.2時(shí)28 V發(fā)電機(jī)發(fā)生失效，State1.18時(shí)系統(tǒng)進(jìn)入DDC工作模態(tài)，慣性測(cè)量組件失效對(duì)系統(tǒng)功能無(wú)影響，State1.51時(shí)右副翼舵機(jī)失效。

3.3 系統(tǒng)規(guī)范驗(yàn)證

NuSMV系統(tǒng)模塊運(yùn)行方式分為同步與異步兩類，模型檢查及仿真過(guò)程中狀態(tài)空間與模塊運(yùn)行方式有關(guān)，在驗(yàn)證系統(tǒng)規(guī)范時(shí)，采用同步運(yùn)行方式以降低狀態(tài)空間規(guī)模，提高檢查效率。在NuSMV Shell中執(zhí)行：

check_ctlspec & show_property

命令得到規(guī)范檢查結(jié)果如圖8所示。

圖8 副翼控制功能反例

檢查發(fā)現(xiàn)命題：

AG !(left_servo.status=failure&right_servo.status=failure)

是錯(cuò)誤的，分析生成的反例可知系統(tǒng)在EFCS模式下發(fā)生了EFCS板的同時(shí)失效，此時(shí)可以根據(jù)系統(tǒng)反例所描述的失效場(chǎng)景通過(guò)限制條件的異步仿真尋找EFCS板同時(shí)失效的原因。

4 結(jié)論

本文針對(duì)模型檢查器NuSMV的特點(diǎn)，提出基于SMV語(yǔ)言的安全性模型構(gòu)建思路，闡述了系統(tǒng)規(guī)范的來(lái)源與實(shí)現(xiàn)方式，并通過(guò)典型民用飛機(jī)電傳飛控系統(tǒng)案例演示利用NuSMV建模與屬性驗(yàn)證過(guò)程。

NuSMV作為最經(jīng)典的模型檢查工具，基于BDD的運(yùn)算方法雖然提高了執(zhí)行效率與建模規(guī)模，但仍在定量計(jì)算、反例優(yōu)化等方面存在局限。作為MBSA的核心工作，如何協(xié)調(diào)安全評(píng)估與模型檢查的關(guān)系仍然值得研究。