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

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

0 引言

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

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

國(guó)外Simfia軟件可將狀態(tài)機(jī)模型自動(dòng)轉(zhuǎn)化為相應(yīng)的AltaRica形式化模型，再利用AltaRica模型的特征，自動(dòng)仿真推演某個(gè)事件觸發(fā)后可能引發(fā)的故障行為。然而，形式化方法采用有嚴(yán)格定義的語(yǔ)義及符號(hào)對(duì)系統(tǒng)的各部分建模，按照規(guī)范對(duì)研究對(duì)象進(jìn)行嚴(yán)格的安全性驗(yàn)證，可增強(qiáng)對(duì)系統(tǒng)細(xì)節(jié)的理解，盡早發(fā)現(xiàn)系統(tǒng)規(guī)范中存在模糊性、二義性的地方，但形式化方法不利于理解，且建模過(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ī)理論具有更大的工程可操作性，極大地降低了形式化建模語(yǔ)言帶來(lái)的分析難度。

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

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

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

有限狀態(tài)機(jī)的要素包括：狀態(tài)集(若干個(gè)狀態(tài))；狀態(tài)之間的轉(zhuǎn)換關(guān)系(全體有向弧表示這種關(guān)系)；輸入集(狀態(tài)之間的轉(zhuǎn)換所需輸入構(gòu)成)；開始和結(jié)束狀態(tài)。利用形式化語(yǔ)言定義，可將有限狀態(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)對(duì)(x,y)∈S×S，將弧標(biāo)記為ω，ω∈Σ，Tm定義為

(2)

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

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

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

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

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

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

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

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

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

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

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

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

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

針對(duì)空空導(dǎo)彈典型作戰(zhàn)過(guò)程中不同階段狀態(tài)遷移進(jìn)行建模，將導(dǎo)彈發(fā)射生存周期狀態(tài)劃分成加電、自檢、對(duì)準(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所示。圖中各個(gè)狀態(tài)的描述見表2。

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

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

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

針對(duì)上一步驟識(shí)別的每個(gè)狀態(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ā)射過(guò)程狀態(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)無(wú)法滿足等。

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

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

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

因此，從條件充分性方面分析出“進(jìn)入應(yīng)急投放狀態(tài)時(shí)，缺少飛機(jī)輪載信號(hào)的判斷”這一異常狀態(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)安全性分析，分析點(diǎn)包括在所有對(duì)應(yīng)的功能中，關(guān)聯(lián)度高的若干功能同時(shí)失效的安全性問(wèn)題；或者從路徑角度分析，如果路徑遷移設(shè)計(jì)得不夠周到所存在的安全性問(wèn)題，最終基于以上2方面的結(jié)果得出潛在的導(dǎo)致空空導(dǎo)彈發(fā)射危險(xiǎn)的不安全遷移條件及其控制措施，見表5。

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

3 結(jié)束語(yǔ)

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