有限狀態(tài)機(jī)在導(dǎo)彈發(fā)射安全性分析中的應(yīng)用*

劉旭，劉艷，王冬，韓穎超，張為雯

(北京電子工程總體研究所，北京 100854)

0 引言

空空導(dǎo)彈發(fā)射過程表現(xiàn)出復(fù)雜的邏輯關(guān)聯(lián)，其飛控系統(tǒng)需要監(jiān)測和控制相關(guān)彈上設(shè)備狀態(tài)，同時輸入輸出變量之間存在復(fù)雜的邏輯關(guān)聯(lián)，對其邏輯特性進(jìn)行安全性分析，即驗證系統(tǒng)的狀態(tài)遷移序列是否按照合理有效的順序執(zhí)行，是開展機(jī)彈安全性分析過程中的一大重點。

有限狀態(tài)機(jī)模型提供了描述和控制功能邏輯非常強(qiáng)大的方法，復(fù)雜邏輯往往可以通過圖表化形式表述，規(guī)則簡單，它通過對狀態(tài)圖、流程圖的創(chuàng)建，對事件驅(qū)動系統(tǒng)進(jìn)行建模分析[1-6]。

國外Simfia軟件可將狀態(tài)機(jī)模型自動轉(zhuǎn)化為相應(yīng)的AltaRica形式化模型，再利用AltaRica模型的特征，自動仿真推演某個事件觸發(fā)后可能引發(fā)的故障行為。然而，形式化方法采用有嚴(yán)格定義的語義及符號對系統(tǒng)的各部分建模，按照規(guī)范對研究對象進(jìn)行嚴(yán)格的安全性驗證，可增強(qiáng)對系統(tǒng)細(xì)節(jié)的理解，盡早發(fā)現(xiàn)系統(tǒng)規(guī)范中存在模糊性、二義性的地方，但形式化方法不利于理解，且建模過程復(fù)雜[7]。

為此，本文以有限狀態(tài)機(jī)的完備功能邏輯提取特性為基礎(chǔ)，研究提出狀態(tài)遷移建模分析方法，有效兼顧了描述系統(tǒng)功能的狀態(tài)機(jī)模型涉及到的初始狀態(tài)、有效狀態(tài)、狀態(tài)轉(zhuǎn)移條件等各分析要素[8-9]，表述形式直觀易懂，較之傳統(tǒng)的有限狀態(tài)機(jī)理論具有更大的工程可操作性，極大地降低了形式化建模語言帶來的分析難度。

1 基于有限狀態(tài)機(jī)的狀態(tài)遷移建模分析方法

1.1 有限狀態(tài)機(jī)基本原理

有限狀態(tài)機(jī)作為一種具有離散輸入和輸出系統(tǒng)的數(shù)學(xué)模型，是指系統(tǒng)內(nèi)有有限個內(nèi)部狀態(tài)，在某些事件發(fā)生時，系統(tǒng)從一個狀態(tài)轉(zhuǎn)換到另一個狀態(tài)，又稱為事件驅(qū)動系統(tǒng)。

有限狀態(tài)機(jī)的要素包括：狀態(tài)集(若干個狀態(tài))；狀態(tài)之間的轉(zhuǎn)換關(guān)系(全體有向弧表示這種關(guān)系)；輸入集(狀態(tài)之間的轉(zhuǎn)換所需輸入構(gòu)成)；開始和結(jié)束狀態(tài)。利用形式化語言定義，可將有限狀態(tài)機(jī)定義為6元組[10]：

M=(Σ,O,S,S0,Δ,Λ)，

(1)

式中：Σ為輸入集合；O為輸出集合；S為M中有限狀態(tài)的集合；S0為初始狀態(tài)的集合；Δ(s,x)為狀態(tài)轉(zhuǎn)移函數(shù)(Δ：S×Σ→S)；Λ(s,x)為輸出函數(shù)(Λ：S×Σ→O)；集合Σ，O，S定義為非空集合；Δ和Λ是多輸出的布爾函數(shù)。

M中的轉(zhuǎn)移關(guān)系TM:S×Σ×S→{0,1}，它描述了所有由一段弧連接的狀態(tài)對(x,y)∈S×S，將弧標(biāo)記為ω，ω∈Σ，Tm定義為

(2)

式中:x1,…,xm為當(dāng)前狀態(tài)變量；ω1,…,ωm為原始的輸入變量；y1，…，ym為有限狀態(tài)機(jī)的下個狀態(tài)變量。形式化方法實質(zhì)是采用數(shù)學(xué)理論描述復(fù)雜邏輯系統(tǒng)采用嚴(yán)格定義語言完成系統(tǒng)各部分的建模，具有嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)基礎(chǔ)。隨著導(dǎo)彈發(fā)射控制涉及的硬件和軟件規(guī)模的擴(kuò)大，系統(tǒng)復(fù)雜度也大大提高，需借助于一套復(fù)雜的狀態(tài)表達(dá)式和路徑表達(dá)式來操作時鐘、控制等各類變量及其計算模型，基于形式化分析與驗證越發(fā)困難[11-15]。

1.2 狀態(tài)遷移建模要素及方法

本文基于有限狀態(tài)機(jī)原理提出了具有工程可操作性的狀態(tài)遷移模型，半定性地描述系統(tǒng)工作狀態(tài)之間的遷移條件關(guān)系，以及工作狀態(tài)與相應(yīng)功能和接口之間的關(guān)聯(lián)關(guān)系及約束關(guān)系。這種支持圖形界面的定性方法相對于形式化建模分析語言更易于理解。

狀態(tài)遷移模型的圖形化建模元素包括：

(1) 工作狀態(tài)：系統(tǒng)運行過程中所有可能的工作狀態(tài)或模式。

(2) 遷移條件：某個工作狀態(tài)向其他工作狀態(tài)發(fā)生遷移的條件關(guān)系。遷移條件通常可由系統(tǒng)外部輸入輸出接口、功能等其他需求模型元素進(jìn)行描述。需要說明的是，一個工作狀態(tài)既有遷入條件，又有遷出條件。

(3) 初始狀態(tài)：系統(tǒng)運行起始點，只用于狀態(tài)遷移圖的起始描述，不具備實際意義。

(4) 結(jié)束狀態(tài)：系統(tǒng)運行終點，只用于狀態(tài)遷移圖的終止描述，不具備實際意義。

(5) 注釋：在圖形化建模過程中，可利用“注釋”對話框來注明每項建模元素的備注信息(例如約束信息、展開描述等)。

狀態(tài)遷移模型的圖形化建模元素圖例如表1所示。

表1 狀態(tài)遷移模型建模元素Table 1 Composition of state migration model

狀態(tài)遷移建模分析流程如圖1所示。

狀態(tài)遷移建模是一個重復(fù)的過程，在存在并行執(zhí)行的狀態(tài)下，有的遷移流程可能會缺少初始狀態(tài)。需要把最初定義的初始狀態(tài)細(xì)化成各個轉(zhuǎn)移流程中的初始狀態(tài)，從而引出新的狀態(tài)。因此，在進(jìn)行后一步工作時，要不斷地返回上一步進(jìn)行修改或完善，從而使建模更加準(zhǔn)確和清晰。

2 空空導(dǎo)彈發(fā)射安全性分析

2.1 確定發(fā)射狀態(tài)遷移模型

針對空空導(dǎo)彈典型作戰(zhàn)過程中不同階段狀態(tài)遷移進(jìn)行建模，將導(dǎo)彈發(fā)射生存周期狀態(tài)劃分成加電、自檢、對準(zhǔn)、準(zhǔn)備、發(fā)射、自主飛行、故障和應(yīng)急投棄狀態(tài)，以導(dǎo)彈狀態(tài)、載機(jī)參數(shù)條件、飛行員操作作為狀態(tài)轉(zhuǎn)換條件，建立的空空導(dǎo)彈典型發(fā)射狀態(tài)遷移圖形化建模如圖2所示。圖中各個狀態(tài)的描述見表2。

2.2 分析發(fā)射狀態(tài)轉(zhuǎn)移關(guān)系模型

基于導(dǎo)彈發(fā)射控制狀態(tài)機(jī)模型，識別狀態(tài)遷移關(guān)系。由此建立的源狀態(tài)至目的狀態(tài)的遷移關(guān)系見表3。

2.3 發(fā)射異常遷移條件識別

針對上一步驟識別的每個狀態(tài)遷移關(guān)系，按照表4的要求，依次進(jìn)行當(dāng)前遷移條件分析及異常狀態(tài)遷移條件分析。

圖1 狀態(tài)遷移建模分析流程Fig.1 Flow chart of state migration modeling

圖2 空空導(dǎo)彈發(fā)射過程狀態(tài)遷移圖Fig.2 State migration diagram of air-to-air missile launching

以應(yīng)急投棄為目的狀態(tài)的所有狀態(tài)遷移(1→9，2→9，3→9，4→9，5→9，6→9，8→9)為例填寫上表，則：

(1) 狀態(tài)遷移：填寫所分析的狀態(tài)遷移，即“1→9,2→9,3→9,4→9,5→9,6→9,8→9”。

(2) 當(dāng)前遷移條件：當(dāng)飛行員進(jìn)行按壓應(yīng)急投棄開關(guān)的操作，觸發(fā)相應(yīng)遷移。因此，在“飛行員操作”一欄填寫“按壓應(yīng)急投棄開關(guān)”。

(3) 異常遷移條件：可從以下方面開展分析當(dāng)前遷移條件的不合理因素，包括。

1) 條件充分性：如各狀態(tài)的進(jìn)入條件、退出條件、約束條件不夠完整；等等。

2) 條件協(xié)調(diào)性：如各狀態(tài)的進(jìn)入條件和退出條件不一致、狀態(tài)退出條件永遠(yuǎn)無法滿足等。

3) 多狀態(tài)遷移：如當(dāng)前狀態(tài)下，向多個狀態(tài)的轉(zhuǎn)移條件同時成立等。

4) 潛通路：如不可相互遷移的狀態(tài)間發(fā)生了狀態(tài)遷移。

5) 狀態(tài)沖突：如互斥狀態(tài)遷移同時出現(xiàn)等。

因此，從條件充分性方面分析出“進(jìn)入應(yīng)急投放狀態(tài)時，缺少飛機(jī)輪載信號的判斷”這一異常狀態(tài)遷移條件。從潛通路方面分析出“響應(yīng)誤操作按壓的投棄致使意外拋棄導(dǎo)彈”這一異常狀態(tài)遷移條件。

表3 狀態(tài)遷移關(guān)系Table 3 Migrating workflow

表4 異常狀態(tài)遷移分析Table 4 Analysis of abnormal precondition of state change

2.4 發(fā)射異常遷移條件控制

從異常遷移條件出發(fā)進(jìn)行系統(tǒng)安全性分析，分析點包括在所有對應(yīng)的功能中，關(guān)聯(lián)度高的若干功能同時失效的安全性問題；或者從路徑角度分析，如果路徑遷移設(shè)計得不夠周到所存在的安全性問題，最終基于以上2方面的結(jié)果得出潛在的導(dǎo)致空空導(dǎo)彈發(fā)射危險的不安全遷移條件及其控制措施，見表5。

表5 異常遷移條件控制措施示例Table 5 Example of prevention and control on abnormal precondition of state change

3 結(jié)束語

本文將有限狀態(tài)機(jī)理論應(yīng)用于復(fù)雜裝備安全性建模分析中，通過對狀態(tài)機(jī)理論模型中涉及到狀態(tài)和轉(zhuǎn)移部分進(jìn)行簡化，建立了由初始狀態(tài)、狀態(tài)和轉(zhuǎn)移關(guān)系所構(gòu)成的狀態(tài)遷移模型。以“狀態(tài)圖”這種半形式化模型與“分析表格”相結(jié)合的方式，可以清晰、簡潔地反映出復(fù)雜系統(tǒng)動態(tài)邏輯關(guān)系，為明確事故的動態(tài)變化過程和制定控制措施提供了依據(jù)，彌補(bǔ)了基于形式化建模語言的有限狀態(tài)機(jī)模型抽象、不易理解而難以在工程上推廣應(yīng)用的不足。