形式化建模視角下航空電子系統檢測研究

劉美山

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

1 航空電子系統的形式化建模

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

圖1 航空電子系統抽象軟件體系結構

1.1 航空電子系統的靜態建模

整體的航空電子系統在功能上和結構上可分為多個分系統，而每個分系統的運行又需要多種計算機軟件的協調合作才能實現預計功能，在結構上通過調用接口和外界相連。將這些用于集成的接口設定為軟件訪問接口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的參數；(4)Bin是一個關于輸入接口Iin的約束集合；(5)Bout則用來表示輸出接的Iout約束集合。

1.2 航空電子系統的動態窗口樹建模

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

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

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

1.3 航空電子系統執行過程狀態圖模型

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

圖2 航空電子系統探測任務流轉圖

2 形式化的系統級綜合檢測方法

2.1 靜態檢測方法

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

2.2 動態檢測方法

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

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

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

（3）系統可用性問題。總系統的功能實現依靠所有分系統之間的相互協調和配合，如果分系統運行環境異常，功能失效，則會影響整個航空電子系統的正常運行，降低航空電子系統的動態運行可靠性。

3 形式化建模視角下航空電子系統檢測

3.1 系統配置級檢測

3.1.1 配置文件一致性檢測

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

3.1.2 狀態適配性檢測

系統環境的狀態適配性檢測，主要檢測分系統的計算機環境對資源的需求，通過逐一讀取標準的性能指標數據與系統數據進行對比檢測。檢測的最終目的是按照系統運行所需的性能指標對分系統進行改進與調整，使其發揮良好使用性能。

3.2 系統運行時檢測

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

圖3 動態監測流程

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

4 結語

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