有限狀態(tài)機在導彈發(fā)射安全性分析中的應用*

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

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

0 引言

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

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

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

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

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

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

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

有限狀態(tài)機的要素包括：狀態(tài)集(若干個狀態(tài))；狀態(tài)之間的轉(zhuǎn)換關系(全體有向弧表示這種關系)；輸入集(狀態(tài)之間的轉(zhuǎn)換所需輸入構(gòu)成)；開始和結(jié)束狀態(tài)。利用形式化語言定義，可將有限狀態(tài)機定義為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)移關系TM:S×Σ×S→{0,1}，它描述了所有由一段弧連接的狀態(tài)對(x,y)∈S×S，將弧標記為ω，ω∈Σ，Tm定義為

(2)

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

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

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

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

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

(2) 遷移條件：某個工作狀態(tài)向其他工作狀態(tài)發(fā)生遷移的條件關系。遷移條件通常可由系統(tǒng)外部輸入輸出接口、功能等其他需求模型元素進行描述。需要說明的是，一個工作狀態(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)遷移建模是一個重復的過程，在存在并行執(zhí)行的狀態(tài)下，有的遷移流程可能會缺少初始狀態(tài)。需要把最初定義的初始狀態(tài)細化成各個轉(zhuǎn)移流程中的初始狀態(tài)，從而引出新的狀態(tài)。因此，在進行后一步工作時，要不斷地返回上一步進行修改或完善，從而使建模更加準確和清晰。

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

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

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

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

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

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

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

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

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

以應急投棄為目的狀態(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) 當前遷移條件：當飛行員進行按壓應急投棄開關的操作，觸發(fā)相應遷移。因此，在“飛行員操作”一欄填寫“按壓應急投棄開關”。

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

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

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

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

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

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

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

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

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

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

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

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

3 結(jié)束語

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