劉美山

（中國飛行試驗研究院，陜西西安，710089）

1 航空電子系統(tǒng)的形式化建模

航空電子系統(tǒng)是一種電子任務程序，該程序可對不同級別的軟件提供支持，是一種較為開放式的系統(tǒng)。復雜、完善的航空電子系統(tǒng)由各種機載硬件設備和相對應的軟件組成，以實現(xiàn)航空電子系統(tǒng)的信息采集、信息處理、信息管理和顯示功能。到目前，在航空電子系統(tǒng)的發(fā)展歷程中，航空電子系統(tǒng)結構從分立式到聯(lián)合式、到綜合式、再到高度綜合式。由航空電子系統(tǒng)的四個發(fā)展階段可以預測到綜合模塊化的航空電子系統(tǒng)是其未來的發(fā)展方向。

圖1 航空電子系統(tǒng)抽象軟件體系結構

1.1 航空電子系統(tǒng)的靜態(tài)建模

整體的航空電子系統(tǒng)在功能上和結構上可分為多個分系統(tǒng)，而每個分系統(tǒng)的運行又需要多種計算機軟件的協(xié)調(diào)合作才能實現(xiàn)預計功能，在結構上通過調(diào)用接口和外界相連。將這些用于集成的接口設定為軟件訪問接口API，并將其作好定義，如下所示：應用程序訪問接口API。API=(api_Name,Iin,Iout,Bin,Bout)。其中，(1)api_Name的含義即字面意識，表示接口的名稱，是為每個api設定的獨立標識；(2)Iin={P1，P2,...，Pm}(M≥0)表示接口I的輸入（in）接口，Pi是Iin的元素 ；(3)Iout={P1，P2,...，Pn}(n ≥ 0)表示接口 I 的輸出（out）接口，Pi同樣表示Iout的參數(shù)；(4)Bin是一個關于輸入接口Iin的約束集合；(5)Bout則用來表示輸出接的Iout約束集合。

1.2 航空電子系統(tǒng)的動態(tài)窗口樹建模

在航空電子系統(tǒng)中，指令和響應的執(zhí)行相當于各API接口之間的有效、順序對接，在所有的API中，并不是一個API接口只負責一個功能，在航空電子系統(tǒng)的整體結構劃分上，會有相對更加重要和關鍵的API接口，作為航空電子系統(tǒng)一些主要功能的轉接入口，而且這些API接口可能以并列關系存在，接口的劃分和使用是依據(jù)輸入數(shù)據(jù)的參數(shù)特征，不同數(shù)據(jù)進入不同功能的API接口進行下一步的任務執(zhí)行。在模型上，將并列的API接口集合定義為一個窗口，這個窗口可能包含多個API接口，通過窗口樹模型之間的流轉，不同數(shù)據(jù)和指令傳輸?shù)较乱粋€窗口。

一般情況下，一個完整的航空電子系統(tǒng)會有非常多的窗口，這些窗口之間有一定的規(guī)格和順序，有條不紊地進行著任務的執(zhí)行，從前一個窗口到下一個窗口的傳輸流轉過程中，可能經(jīng)過一個事件或多個事件。上文提到，在航空電子系統(tǒng)進行任務的執(zhí)行時，指令進入API接口的原則是依據(jù)參數(shù)的特征，不同的接口代表不同的流轉方向，那么復雜、全面的航空電子系統(tǒng)任務執(zhí)行的全部流程，會形成類似一棵樹的模型，窗口樹中的每條路徑分別代表航空電子系統(tǒng)每一次任務的運行行為。

例如，民航航空電子系統(tǒng)在執(zhí)行氣象探測任務的時候，可建立窗口樹模型，實現(xiàn)對窗口流轉關系的模擬。為了保障飛機飛行的安全性和舒適性，航空電子系統(tǒng)需要及時對飛機飛行軌跡前方的有危險性氣象區(qū)域進行不斷探測，為飛行軌跡的改變提供數(shù)據(jù)支撐。首先啟動雷達，設置雷達參數(shù)對氣象區(qū)域進行掃描，將收集到的信息作為對目標進行判斷和處理的依據(jù)。只要雷達有探測到目標，就會進行下一步的任務階段，進入到系統(tǒng)響應階段，雷達分系統(tǒng)會將多次收集到的航跡進行計算綜合，然后將這些有用的數(shù)據(jù)全都傳輸給指控分系統(tǒng)，在下一步的流程中，依據(jù)情報綜合窗口，對收集的數(shù)據(jù)進行威脅程度判定，威脅程度低的目標不予處理，對威脅程度高的目標進行相應地調(diào)整和改變，做出對危險氣象合理的躲避與引導方案。

1.3 航空電子系統(tǒng)執(zhí)行過程狀態(tài)圖模型

圖2為航空電子系統(tǒng)探測任務的流轉狀態(tài)。該狀態(tài)是依據(jù)航空電子系統(tǒng)各個環(huán)節(jié)的行為狀態(tài)及任務流轉來分析決定的。在電子系統(tǒng)中，所有的指令操作都是從顯控開始。當系統(tǒng)中觸動雷達參數(shù)設置后，系統(tǒng)自動進入雷達，擬制狀態(tài)，這表示任務即將流轉下一階段。當雷達接受到指令后會對其進行編輯，然后將整理好的綜合航空數(shù)據(jù)快速傳輸?shù)街缚仉A段，屆時進入指控，編輯狀態(tài)。操作人員通過顯控臺查看傳送的各項參數(shù)，并對其進行相應操作后發(fā)送給指控，擬制，最終形成完整的數(shù)據(jù)鏈，直至結束。這是一次完整的信息處理流程，中途若有不符合的狀態(tài)或不符合的事件，則直接發(fā)送至結束狀態(tài)。

圖2 航空電子系統(tǒng)探測任務流轉圖

2 形式化的系統(tǒng)級綜合檢測方法

2.1 靜態(tài)檢測方法

在靜止狀態(tài)下，系統(tǒng)配置級檢測方法一般檢測系統(tǒng)的配置環(huán)境情況，檢測環(huán)境會不會對航空電子系統(tǒng)的正常運行造成影響，通常對系統(tǒng)的一致性和適配性進行檢測，例如，航空電子系統(tǒng)分系統(tǒng)和功能模塊的安裝程序、執(zhí)行文件等是否一致未被改動，或者模塊版本更新時軟件性能和版本的設計是否匹配，二者的配合度能否滿足用戶對軟件的使用，系統(tǒng)不同模塊之間運行原則是否一致，各接口是否能實現(xiàn)任務的正常流轉等一系列有關航空電子系統(tǒng)一致性和適配性的問題。

2.2 動態(tài)檢測方法

靜態(tài)檢查完成后，若無其他問題，系統(tǒng)則自動進入動態(tài)檢測。在航空電子系統(tǒng)的運行過程中，可能由于多種原因，導致系統(tǒng)沒有沿著設定路徑運行，出現(xiàn)各種影響總系統(tǒng)正常運行和飛機航空安全的問題，例如，功能模塊失效、數(shù)據(jù)不具備精確性和時效性、接口電路失效、路徑錯誤等問題。根據(jù)對系統(tǒng)等級的影響，將問題分為以下幾類：

（1）軟件模塊可用性。系統(tǒng)功能模塊的運行需要良好前提條件，若總系統(tǒng)或者其他模塊在動態(tài)運行中對此功能模塊的正常運行造成障礙，導致運行環(huán)境無法支持該功能模塊的良好運行，很有可能造成該模塊達不到預期效果甚至無法完成系統(tǒng)任務。

（2）分系統(tǒng)可用性問題。當運行環(huán)境受到影響，分系統(tǒng)的功能實現(xiàn)以及路徑選擇都可能出現(xiàn)差錯，分系統(tǒng)軟件設定和硬件單元執(zhí)行可能無法實現(xiàn)有效對接，導致分系統(tǒng)部分功能不可用甚至系統(tǒng)錯亂。

（3）系統(tǒng)可用性問題?？傁到y(tǒng)的功能實現(xiàn)依靠所有分系統(tǒng)之間的相互協(xié)調(diào)和配合，如果分系統(tǒng)運行環(huán)境異常，功能失效，則會影響整個航空電子系統(tǒng)的正常運行，降低航空電子系統(tǒng)的動態(tài)運行可靠性。

3 形式化建模視角下航空電子系統(tǒng)檢測

3.1 系統(tǒng)配置級檢測

3.1.1 配置文件一致性檢測

對航空電子系統(tǒng)配置文件一致性進行檢測時，分系統(tǒng)級的配置文件是主要檢測對象，提取一個分系統(tǒng)在軟件模塊方面的配置文件數(shù)據(jù)，與標準的配置文件信息進行比對，檢測兩者數(shù)據(jù)是否一致，有沒有被惡意更改，以保證航空電子系統(tǒng)計算機軟件的安全性。與標準的配置文件信息對比過程需要調(diào)用標準庫SL，這是事先建立好的一種數(shù)據(jù)庫，其中具有每個功能模塊正確的配置文件信息。

3.1.2 狀態(tài)適配性檢測

系統(tǒng)環(huán)境的狀態(tài)適配性檢測，主要檢測分系統(tǒng)的計算機環(huán)境對資源的需求，通過逐一讀取標準的性能指標數(shù)據(jù)與系統(tǒng)數(shù)據(jù)進行對比檢測。檢測的最終目的是按照系統(tǒng)運行所需的性能指標對分系統(tǒng)進行改進與調(diào)整，使其發(fā)揮良好使用性能。

3.2 系統(tǒng)運行時檢測

在飛機航空電子系統(tǒng)運轉中或者飛行狀態(tài)下進行的檢測稱為動態(tài)檢測，以有限狀態(tài)自動機檢測航空飛行路線是否符合系統(tǒng)設計。一般主要的動態(tài)監(jiān)測流程為：分析航空電子系統(tǒng)總體設計，將任務主體按照階段進行劃分，得到任務運行的階段流程分析圖，在形式化建模視角下，選取系統(tǒng)關鍵功能和對應的API接口，構建窗口樹模型，窗口樹模型的每一條路徑都代表著事件的流轉，以事件流為基礎生成檢測用例集，明確以任務為主體的狀態(tài)執(zhí)行路徑，并將其轉換為計算機可接受識別的有限狀態(tài)自動機。航空電子系統(tǒng)動態(tài)監(jiān)測流程如圖3所示。

圖3 動態(tài)監(jiān)測流程

在航空電子系統(tǒng)的檢測過程中，有限狀態(tài)自動機是系統(tǒng)動態(tài)監(jiān)測的核心，由圖3可知，首先要根據(jù)形式化模型的窗口樹設置一定數(shù)量的檢查點，設置檢測用例的參數(shù)，經(jīng)系統(tǒng)實現(xiàn)之后，獲得系統(tǒng)的行為軌跡，為保證下一步任務狀態(tài)機的有效識別，需要將這些行為軌跡符號轉換為計算機可以識別的輸入符號序列∑+，將這些符號序列∑+輸入到有限狀態(tài)自動機中進行運行，如果得到輸出，則認為該檢測用例經(jīng)系統(tǒng)實現(xiàn)以后，得到的系統(tǒng)行為軌跡能被源自系統(tǒng)設計的有限狀態(tài)自動機所接受[6]。

4 結語

復雜的航空電子系統(tǒng)在分系統(tǒng)和功能模塊的相互協(xié)調(diào)下完成各項任務的執(zhí)行，文章在靜態(tài)和動態(tài)下對航空電子系統(tǒng)進行了形式化建模，提出了任務在對應API接口流轉的窗口樹建模方法，提出了基于形式化的系統(tǒng)級綜合檢測方法，同樣從靜態(tài)的系統(tǒng)配置級檢測和動態(tài)系統(tǒng)運行檢測兩方面對航空電子系統(tǒng)進行綜合性檢測研究，以提升航空電子系統(tǒng)運行的可靠性和高效性[7-8]。