基于概率模型檢驗的民機平視顯示系統(tǒng)建模與安全性分析

王 鵬, 張 帆, 董 磊, 趙長嘯

(中國民航大學,a.天津市民用航空器適航與維修重點實驗室; b.適航學院，天津 300300)

基于概率模型檢驗的民機平視顯示系統(tǒng)建模與安全性分析

王 鵬a, 張 帆b, 董 磊a, 趙長嘯a

(中國民航大學,a.天津市民用航空器適航與維修重點實驗室; b.適航學院，天津 300300)

民機平視顯示系統(tǒng)(HUD)作為安全關(guān)鍵系統(tǒng)，由于其高度復雜且與其他機載系統(tǒng)結(jié)合使用，使得傳統(tǒng)系統(tǒng)安全性評估方法難以滿足定量安全性分析需求。因此，需要開發(fā)基于形式化模型的安全性評估(MBSA)方法，在明確概率模型檢驗原理及系統(tǒng)高層建模規(guī)范基礎(chǔ)上，研究平顯系統(tǒng)概率模型分層建模方法，建立平顯系統(tǒng)概率模型，并描述系統(tǒng)定量安全性屬性，展開自動概率模型檢驗，得出定量安全性分析結(jié)論，提高安全性分析效率與運算結(jié)果精確度。

平視顯示器； 民機； 概率模型檢驗； 形式化模型； 定量分析； 安全性

0 引言

作為民用飛機航行新技術(shù)，平視顯示系統(tǒng)(HUD)與其他系統(tǒng)相互綜合，將重要的飛行參數(shù)(如飛行高度、飛行速度、姿態(tài)、航向等)以圖形、字符的形式，通過光學部件投影到座艙正前方組合儀上[1]。由于該組合儀高度大致與飛行員的眼睛處于水平位置，因此飛行員透過平顯觀察艙外景物時，幾乎不用改變眼睛焦距就能同時觀測到平顯上顯示的圖形和字符信息，從而及時修正飛行姿態(tài)，對于減輕飛行員負擔，提高飛行員環(huán)境感知能力，增強飛行安全性具有重要意義。

隨著平顯系統(tǒng)集成化程度的提高，平顯系統(tǒng)部分功能以模塊化形式集成到綜合模塊化的航電系統(tǒng)(IMA)中，且通過飛控系統(tǒng)、增強視景系統(tǒng)等獲取數(shù)據(jù)及視頻信息，使得平顯系統(tǒng)高度復雜。作為航電安全關(guān)鍵系統(tǒng)，由于傳統(tǒng)基于雙V的安全性評估方法[2]存在工作量大、依賴于專家經(jīng)驗且易于出錯等問題[3]，需要開發(fā)新型的基于模型的自動化分析方法，對民機平顯系統(tǒng)展開定量分析，提高安全性評估效率。

針對上述問題，采用基于概率模型檢驗的形式化安全性分析技術(shù)，在分析平顯系統(tǒng)物理架構(gòu)及功能基礎(chǔ)上，探索平顯系統(tǒng)分層建模方法，深入分析系統(tǒng)內(nèi)部失效轉(zhuǎn)移邏輯，對系統(tǒng)定量安全性屬性展開自動化驗證，得出分析結(jié)論。

1 概率模型檢驗

1.1 概率模型檢驗概述

概率模型檢驗(Probabilistic Model Checking)通過形式化方法，驗證具有隨機行為的系統(tǒng)定量屬性[4]?；谄斤@系統(tǒng)的概率模型檢驗框架如圖1所示，包括以下兩項輸入[5]。

1) 系統(tǒng)高層模型?；趪栏竦钠斤@系統(tǒng)物理架構(gòu)及功能分析，捕獲平顯系統(tǒng)內(nèi)部各模塊失效模式、失效概率及失效轉(zhuǎn)移路徑，對系統(tǒng)進行高層模型建模。

2) 形式化屬性規(guī)范。通過分析平顯系統(tǒng)定量安全性需求，將其以時序或穩(wěn)態(tài)邏輯形式表達為系統(tǒng)屬性規(guī)范。

完成上述平顯系統(tǒng)建模與屬性規(guī)范表達后，基于狀態(tài)機原理進行自動化底層系統(tǒng)失效狀態(tài)轉(zhuǎn)移建模，分析失效路徑并計算各狀態(tài)定量概率，得出安全性分析結(jié)論。

圖1 概率模型檢驗框架Fig.1 An overview of probabilistic model checking

1.2 概率模型檢驗原理

自動分析系統(tǒng)概率行為并建立系統(tǒng)高層模型，是概率模型檢驗的關(guān)鍵內(nèi)容。概率模型檢驗支持離散時間Markov鏈(DTMC)、連續(xù)時間Markov鏈(CTMC)及Markov決策過程(MDP)[6]。在民機系統(tǒng)安全性分析過程中，采用CTMC對系統(tǒng)行為進行分析。

1) 連續(xù)時間Markov鏈定義。

設(shè)過程{X(t),t≥0}為連續(xù)時間的隨機過程，若對于一切s,t≥0和非負整數(shù)i,j,x(u),0≤u≤s,有

P{X(t+s)=j|X(s)=i,X(u)=x(u),0≤uP{X(t+s)=j|X(s)=i}

(1)

則稱過程{X(t),t≥0}是一個連續(xù)時間Markov鏈[7]。通常，以Pij(t)表示當前處于狀態(tài)i的Markov鏈在附加時間t后處于狀態(tài)j的概率，即

Pij(t)=P{X(t+s)=j|X(s)=i} 。

(2)

2) 狀態(tài)轉(zhuǎn)移及運算原理。

連續(xù)時間Markov鏈能夠表示隨著時間變化，系統(tǒng)可能出現(xiàn)的各種狀態(tài)及狀態(tài)間的轉(zhuǎn)移關(guān)系。在基于概率模型檢驗的民機系統(tǒng)安全性分析中，各狀態(tài)指的是系統(tǒng)可能出現(xiàn)的失效模式，轉(zhuǎn)移關(guān)系指正常模式與失效模式以及各失效模式之間的轉(zhuǎn)換邏輯。完成系統(tǒng)高層建模后，概率模型基于CTMC將高層模型轉(zhuǎn)換為底層模型，進行概率計算，以支持定量安全性分析。對應底層模型舉例如圖2所示，并得到其相應的微分方程組。

圖2 CTMC底層模型Fig.2 CTMC bottom-level model

(3)

通過拉氏變換，概率模型檢驗將自動求解上述微分方程，可得到經(jīng)過確定的時間t，處于上述4種狀態(tài)的概率，完成定量計算過程。

1.3 概率模型高層建模規(guī)范

概率模型檢驗方法通過結(jié)構(gòu)化的高級語言對系統(tǒng)建模,該語言由最基本的模塊及變量組成。通過建立一系列表示系統(tǒng)各組分的并行模塊，以變量形式定義各模塊的失效模式及其概率，并采用邏輯等式的方式，表達模塊中變量之間、模塊與模塊間的相互關(guān)系。模塊的失效行為由一系列命令表示，對于CTMC，采用以下語法表達命令：[action](guard) -> (rate):(up-date);其中，命令起始于[]，action為同步符號；(guard)表示模塊中的變量，在系統(tǒng)安全性分析建模中，變量通常為失效模式；->表示狀態(tài)轉(zhuǎn)移，執(zhí)行該狀態(tài)轉(zhuǎn)移的條件是(guard)為真；(update)表示轉(zhuǎn)移后的狀態(tài)；(rate)表示發(fā)生該轉(zhuǎn)移的概率。

概率模型采用標準的CSP并行代數(shù)處理器將各模塊進行集成，可更精確地指定模塊間的同步關(guān)系。同時，對于模塊中各狀態(tài)之間、模塊與模塊之間的邏輯關(guān)系，通過邏輯等式的形式描述?；诓紶柋磉_式，邏輯等式將模塊變量以基礎(chǔ)邏輯形式(如NOT：！，AND：&，OR：|)銜接，在系統(tǒng)安全性分析建模時，便于模塊及功能的封裝。

2 基于概率模型檢驗的平顯系統(tǒng)建模

2.1 平顯系統(tǒng)物理架構(gòu)與典型功能分析

典型的民用飛機平顯系統(tǒng)主要是由平顯計算機(HUDC)、組合儀(HCU)、投影組件(HPU)組成[8]。通過ADN數(shù)據(jù)網(wǎng)絡(luò)及航空總線，由左右兩側(cè)HUDC接收來自于飛機其他航電設(shè)備的各種數(shù)據(jù)，如速度、加速度、姿態(tài)、位置、風速、導航信息、引導提示、告警信息等[9]，經(jīng)處理、融合后生成HUD 顯示圖像，再經(jīng)過總線分別傳遞至左右兩側(cè)HPU，最終顯示于機長與副駕HCU。根據(jù)平顯系統(tǒng)的主要功能，識別其交互界面，如表1所示。

作為概率模型檢驗的系統(tǒng)安全性需求輸入之一，通過功能危害性評估(FHA)識別出平顯系統(tǒng)的失效狀態(tài)及影響等級，其中,災難性失效狀態(tài)(I類)如表2所示。此處，選取雙側(cè)HUD姿態(tài)誤指示這種失效狀態(tài)，作為安全性分析的對象。圖3是HUD在顯示飛行姿態(tài)功能下對應的系統(tǒng)物理架構(gòu)。

表1 平顯系統(tǒng)主要功能及交互界面

表2 平顯系統(tǒng)災難性失效狀態(tài)

圖3 基于飛行姿態(tài)顯示功能的平顯物理架構(gòu)Fig.3 HUD physical architecture based on attitude display

2.2 平顯系統(tǒng)概率模型分層建模方法

平顯系統(tǒng)作為重要航電系統(tǒng)，關(guān)系到飛機整機的可靠性與安全性。由于平顯系統(tǒng)具備模塊化、資源共享等特點，因此對其進行概率模型建模與安全性分析面臨技術(shù)困難。此外，由于模型檢驗方法的本質(zhì)是基于對狀態(tài)空間的窮舉搜索，對于并發(fā)系統(tǒng)，其狀態(tài)數(shù)目會隨著并發(fā)量的增加而呈指數(shù)增長，出現(xiàn)狀態(tài)爆炸問題[10]。解決上述問題，對其進行概率模型建模時，采用基于不同粒度的分層建模方法，降低系統(tǒng)復雜程度，減少狀態(tài)空間數(shù)量。

由于在進行初步系統(tǒng)安全性評估(PSSA)時，需要根據(jù)ARP 4754A[11]，將功能研制保證等級由系統(tǒng)向子系統(tǒng)、設(shè)備及軟硬件分解，因此，在概率模型分層建模時，以功能為上下層級連接依據(jù)，從軟硬件功能模塊或內(nèi)部元件開始建模，通過邏輯等式逐步向上一級封裝，分別建立元件級/功能模塊級、設(shè)備級、子系統(tǒng)級、系統(tǒng)級4層模型，建模層次如圖4所示。

圖4 概率模型層次圖Fig.4 Hierarchical probabilistic model

2.3 平顯系統(tǒng)概率模型建模

2.3.1 功能模塊級概率模型建模

平顯系統(tǒng)概率模型建模從設(shè)備內(nèi)部軟硬件功能模塊開始。由于平顯系統(tǒng)為復雜航電系統(tǒng)，因此設(shè)備內(nèi)部軟硬件功能模塊復雜，不再詳細描述。此處以圖3中左側(cè)HUDC(HUDC_L)為例，根據(jù)選定的失效狀態(tài)，雙側(cè)HUD飛行姿態(tài)誤顯示，識別相應失效信息如表3所示，對應概率模型為3個模塊，圖形處理、圖形存儲與數(shù)據(jù)傳輸；每個模塊內(nèi)定義了失效模式及發(fā)生概率。

表3 左側(cè)HUDC故障模式與影響分析

根據(jù)表3失效信息，建立左側(cè)HUDC概率模型如下。

ctmc

muduleHUDC_processor

HUDC_antialiasing_failure_mode:boolinit false;

HUDC_predistortion_failure_mode:boolinit false;

HUDC_rotate_failure_mode:boolinit false;

[](!HUDC_anatialiasing_failure_mode)->(3.56-5):(HUDC_analialiasing_failure_mode’=true);

[](!HUDC_predistortion_failure_mode)->(1.27E-5):(HUDC_predistortion_failure_mode’=true);

[](!HUDC_rotate_failure_mode)->(6.17E-6):(HUDC_rotate_failure_mode’=true);

endmodule

moduleHUDC_storage

HUDC_storage_failure_mode:boolinit false;

[](!HUDC_storage_failure_mode)->(4.33E-6):(HUDC_storage_failure_mode’=true);

endmodule

moduleHUDC_data

HUDC_data_failure_mode:boolinit false;

[](!HUDC_data_failure_mode)->(1.78E-6):(HUDC_data_failure_mode’=true);

endmodule

2.3.2 設(shè)備級概率模型建模

設(shè)備級建模指的是設(shè)備內(nèi)部軟硬件建模。建立設(shè)備級概率模型時，首先需要分析設(shè)備整體的失效路徑，即分析失效模式組合導致設(shè)備特定功能失效的失效邏輯。作為HUD內(nèi)部的一個LRU(航線可更換單元)，左側(cè)HUDC內(nèi)部模塊失效模式造成姿態(tài)誤顯示的失效邏輯如下：formulaHUDC_L_wrong_attitude=(HUDC_antialiasing_failure_mode)|(HUDC_predistortion_failure_mode)|(HUDC_rotate_failure_mode)|(HUDC_storage_failure_mode)|(HUDC_data_failure_mode)。

其中，formula為等式標簽，等號左端為HUDC_L原因造成姿態(tài)誤顯示，等號右端為HUDC_L內(nèi)部各功能模塊失效模式間失效邏輯。通過建立上述邏輯等式描述，完成設(shè)備內(nèi)部功能模塊失效模式向設(shè)備級封裝，即完成設(shè)備級建模過程。按上述方法依次完成平顯系統(tǒng)其他設(shè)備的設(shè)備級建模，在此不再贅述。

2.3.3 子系統(tǒng)級概率模型建模

平顯系統(tǒng)包括兩個子系統(tǒng)，分別為平顯及ADN數(shù)據(jù)網(wǎng)絡(luò)。同理，在明確子系統(tǒng)內(nèi)部各設(shè)備特定功能失效的條件下，通過建立各設(shè)備失效邏輯，可完成設(shè)備向子系統(tǒng)的封裝，即子系統(tǒng)級概率模型建模。首先分析左側(cè)平顯子系統(tǒng)姿態(tài)誤顯示失效邏輯，左側(cè)平顯姿態(tài)誤顯示是由HUDC_L圖像缺陷、左側(cè)HPU圖像缺陷及A429誤碼導致，對應子系統(tǒng)級建模如下：formulaHUD_L_wrong_attitude=(HUDC_L_wrong_attitude)|(HPU_L_wrong_image_failure_mode)|(A429_7_wrong_data_failure_mode)。

對于另一子系統(tǒng)，ADN數(shù)據(jù)網(wǎng)絡(luò)原因?qū)е伦藨B(tài)誤顯示，當來自左側(cè)慣性系統(tǒng)的姿態(tài)數(shù)據(jù)經(jīng)過ADN網(wǎng)絡(luò)后出現(xiàn)錯誤，則會導致左側(cè)平顯姿態(tài)誤顯示，ADN網(wǎng)絡(luò)為雙通道網(wǎng)絡(luò)，當A，B兩個通道均失效時，對應左側(cè)平顯姿態(tài)誤顯示。子系統(tǒng)建模如下：formula ADN_L_wrong_attitude=(RDIU_3_data_failure_mode)|(((A664_1_wrong_data_failure_mode)|(ACS_1_data_failure_mode)|(A664_5_wrong_data_failure_mode)|(ARS_1_data_failure_mode)|(A664_7_wrong_data_failure_mode)|(RDIU_15_data_failure_mode)|(A429_3_wrong_data_failure_mode))&((A664_2_wrong_data_failure_mode)|(ARS_4_data_failure_mode)|(A664_8_wrong_data_failure_mode)|(RDIU_16_data_failure_mode)|(A429_5_wrong_data_failure_mode)))。

2.3.4 系統(tǒng)級概率模型建模

完成上述子系統(tǒng)建模后，對子系統(tǒng)進行邏輯等式封裝，得到左側(cè)平顯姿態(tài)誤顯示系統(tǒng)級概率模型，其失效由慣性系統(tǒng)或ADN數(shù)據(jù)網(wǎng)絡(luò)或平顯導致；同理可得右側(cè)系統(tǒng)級概率模型，二者同時發(fā)生，導致失效狀態(tài)雙側(cè)平顯姿態(tài)誤顯示發(fā)生。對應左、右兩側(cè)及雙側(cè)系統(tǒng)級模型為：

formulasystem_L_wrong_attitude=(IRU_L_attitude_failure_mode)|(A429_1_wrong_data_failure_mode)|(ADN_L_wrong_attitude)|(HUD_L_wrong_attitude);

formulasystem_R_wrong_attitude=(IRU_R_attitude_failure_mode)|(A429_2_wrong_data_failure_mode)|(ADN_R_wrong_attitude)|(HUD_R_wrong_attitude);

formulasystem_wrong_attitude=(system_L_wrong_attitude)&(system_R_wrong_attitude)。

3 平顯系統(tǒng)定量安全性分析

3.1 系統(tǒng)屬性規(guī)范描述

驗證系統(tǒng)行為是否滿足定量安全性需求，必須將系統(tǒng)行為進行形式化描述，即系統(tǒng)屬性規(guī)范描述。針對CTMC的定量屬性驗證，應在捕獲系統(tǒng)定量屬性需求的基礎(chǔ)上，采用CSL連續(xù)隨機邏輯語言對系統(tǒng)屬性進行形式化規(guī)范?；贑SL語言的邏輯形式包括兩種，時序邏輯和穩(wěn)態(tài)邏輯[12]。通常，穩(wěn)態(tài)邏輯用于檢驗系統(tǒng)長時間運行條件下，某狀態(tài)出現(xiàn)的概率。然而由于穩(wěn)態(tài)邏輯受限于平衡狀態(tài)，對于飛機系統(tǒng)安全性評估中需要檢驗的屬性，如平均每飛行小時某失效狀態(tài)出現(xiàn)的概率，應采用時序邏輯形式描述。如果系統(tǒng)在2 h之內(nèi)發(fā)生失效狀態(tài)A的概率可以表示為：P=？[true U<=2(system_FC_A)]。完成屬性描述后，概率模型將自動展開屬性檢驗，得出結(jié)論。

3.2 定量安全性分析

完成平顯系統(tǒng)概率模型建模后，對其定量安全性屬性展開自動化驗證。根據(jù)系統(tǒng)安全性需求，要求雙側(cè)HUD姿態(tài)誤指示發(fā)生概率應小于等于1E-9平均每飛行小時，設(shè)該機型飛機每次飛行平均飛行小時為2 h，根據(jù)這個需求從設(shè)備級起逐級展開定量驗證，相應左側(cè)系統(tǒng)、右側(cè)系統(tǒng)及系統(tǒng)整體失效的時序邏輯如下：

概率模型檢驗器基于Markov狀態(tài)轉(zhuǎn)移原理，建立系統(tǒng)底層運算模型，并通過基于符號模型檢測的MTBDD(多終端二叉決策圖)對狀態(tài)進行歸并與化簡，且進一步利用稀疏引擎、MTBDD引擎及混合引擎[13]展開自動定量概率運算后，得到雙側(cè)平顯系統(tǒng)姿態(tài)誤指示的定量安全性分析結(jié)果如表4所示。

表4 雙側(cè)平顯系統(tǒng)失效概率分析

經(jīng)過對雙側(cè)平顯系統(tǒng)姿態(tài)誤指示的概率模型自動驗證，共分析了4 194 304個狀態(tài)，可能的狀態(tài)轉(zhuǎn)移達46 137 345個，通過遍歷驗證，最終得到失效狀態(tài)“雙側(cè)平顯系統(tǒng)姿態(tài)誤指示”的概率為平均每飛行小時6.035E-9。根據(jù)系統(tǒng)安全性需求，該值應小于等于平均每飛行小時1E-9，因此，不滿足系統(tǒng)安全性需求，可通過提供計算保守性證明或重新設(shè)計調(diào)整物理架構(gòu)，以進一步滿足該安全性需求。

在此，考慮對物理架構(gòu)重新調(diào)整，使系統(tǒng)滿足安全性需求。逐級檢驗左側(cè)平顯系統(tǒng)定量屬性，得到安全性結(jié)果如表5所示。

表5 左側(cè)平顯系統(tǒng)失效概率分析

根據(jù)表5結(jié)果可知，左側(cè)HUDC及HPU失效導致姿態(tài)誤指示發(fā)生的概率較大，因此對兩側(cè)HUDC物理架構(gòu)重新進行安全性設(shè)計。由于HUDC功能模塊中圖形處理模塊承擔著圖形反走樣、預畸變處理以及分辨率調(diào)整等重要功能，且這些功能均由同一個FPGA執(zhí)行，因此，考慮在HUDC內(nèi)部設(shè)置CPU，對該功能模塊進行監(jiān)控，當處理后的圖像不符合處理前信息時，由CPU發(fā)出錯誤指令，終止圖像顯示。在該物理架構(gòu)下，經(jīng)過屬性驗證，HUDC失效導致姿態(tài)誤指示的概率為平均每飛行小時6.382 8E-9，平顯系統(tǒng)姿態(tài)誤指示的定量安全性分析結(jié)果如表6所示。

表6 新架構(gòu)下雙側(cè)平顯系統(tǒng)失效概率分析

架構(gòu)調(diào)整后，失效狀態(tài)“雙側(cè)平顯系統(tǒng)姿態(tài)誤指示”的概率為平均每飛行小時2.602E-10，滿足系統(tǒng)安全性需求，定量系統(tǒng)安全性分析工作完成。

上述定量安全性分析均由概率模型檢驗器PRISM完成,該工具是由英國伯明翰大學、牛津大學及格拉斯哥大學共同設(shè)計開發(fā)的形式化建模與定量驗證工具。目前已廣泛應用于不同領(lǐng)域，包括通信、多媒體協(xié)議、安全協(xié)議、動態(tài)資源管理規(guī)劃、生物系統(tǒng)等，為系統(tǒng)安全性分析提供了巨大支持[4]。在此基礎(chǔ)上，將其運用于民機復雜航電系統(tǒng)定量安全性分析，具有一定價值與意義。

4 結(jié)論

本文提出了基于概率模型檢驗的形式化安全性分析方法，有效解決了平視顯示系統(tǒng)高復雜性、模塊化程度高的問題?；贛arkov理論，將系統(tǒng)內(nèi)各模塊失效模式作為Markov狀態(tài)，在明確各狀態(tài)間的轉(zhuǎn)移關(guān)系基礎(chǔ)上，采用分層建模技術(shù)，建立各層級概率模型，有效降低了系統(tǒng)復雜程度；最后通過時序邏輯描述檢驗系統(tǒng)定量安全性需求，以遍歷方式自動完成所有狀態(tài)及轉(zhuǎn)移檢驗，得出定量概率驗證結(jié)果，該結(jié)果能為系統(tǒng)安全性評估提供有效支持，降低安全性評估工作量，提高定量分析精度。

[1] 吳連慧.機載平顯圖形生成與視頻處理算法研究及其FPGA實現(xiàn)[D].南京:南京航空航天大學,2014.

[2] SAE.ARP4761 guidelines and methods for conducting the safety assessment process on civil airborne systems[S].[S.l.]:SAE International,1996.

[3] KWIATKOWSKA M，NORMAN G，PARKER D.Advances and challenges of probabilistic model checking[J].Communication,Control,& Computing,2010,111(2):1691-1698.

[4] NORMAN G,PARKER D.Quantitative verification:formal guarantees for timeliness,reliability and performance[R].London:London Mathematical Society and Smith Institute, 2014.

[5] KWIATKOWSKA M，NORMAN G，PARKER D.PRISM:probabilistic model checking for performance and reliability analysis[J].ACM Sigmetrics Performance Evaluation Review,2009,36(4):40-45.

[6] ELMQVIST J,NADJM-TEHRANI S.Formal support for quantitative analysis of residual risks in safety-critical systems[C]//HASE′08 Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium,Washing-ton: IEEE Computer Society,2008:154-164.

[7] ROSS S M.隨機過程[M].龔光魯，譯.2版.北京:機械工業(yè)出版社,2015.

[8] 王全忠,高文正.平視顯示器在民用飛機上的應用研究[J].電光與控制,2014，21(8):1-5.

[9] 費益,季小琴,程金陵.平視顯示系統(tǒng)在民用飛機上的應用[J].電光與控制,2012，19(3):95-99.

[10] 侯剛,周寬久,勇嘉偉,等.模型檢測中狀態(tài)爆炸問題研究綜述[J].計算機科學,2013,40(s1):77-86.

[11] SAE.ARP4754A guidelines for development of civil aircraft and systems[S].[S.l.]:SAE International,2010.

[12] GE X C,PAIGE R F,MCDERMID J A.Analysing system failure behaviours with PRISM[C]//Fourth International Conference on Secure Software Integration and Reliability Improvement Companion,IEEE Computer Society,2010:130-136.

[13] YAN S,ZHANG H,ZHANG Y.Reliability prediction of a hydraulic system with probabilistic model checking[C]//International Conference on Reliability Systems Engineering,IEEE,2016:1-7.

ProbabilityModelCheckBasedModelingandSafetyAnalysisofHUDSystemonCivilAircrafts

WANG Penga, ZHANG Fanb, DONG Leia, ZHAO Chang-xiaoa

(Civil Aviation University of China,a.Civil Aircraft Airworthiness and Repair Key Laboratory of Tianjin;b.College of Airworthiness,Tianjin 300300,China)

Head-Up Display (HUD) onboard civil aircrafts is a crucial safety system.Because of its high complexity and other airborne systems combined with it,the traditional system-safety-assessment method has difficulty in meeting the requirements of a quantitative safety analysis.Therefore,it’s necessary to develop a Model-Based Safety-Assessment (MBSA) method.On the basis of clearly defining the principles of the probability model check and the high-level system-modeling specifications,we studied the method for hierarchical modeling of the probability model of the HUD system,built the probability model of the HUD system,described the quantitative safety properties of the system,and carried out automatic probability model checks.The conclusion of the quantitative safety analysis was obtained,which can improve the efficiency of the safety analysis and the accuracy of the calculating results.

head-up display; civil aircraft; probability model check; formalized model; quantitative analysis; safety

王鵬，張帆，董磊，等.基于概率模型檢驗的民機平視顯示系統(tǒng)建模與安全性分析[J].電光與控制，2017，24 ( 11) : 64-69.WANG P，ZHANG F，DONG L，et al.Probability model check based modeling and safety analysis of HUD system on civil aircrafts[J].Electronics Optics & Control，2017，24( 11) : 64-69．

2017-01-13

2017-03-29

國家自然科學基金委員會-中國民航局民航聯(lián)合研究基金資助(U1533105)；中國民航大學科研啟動基金項目(2013QD 04X)；天津市自然科學基金聯(lián)合資助項目(15JCQNJC42800)；中國民航大學科技創(chuàng)新基金(Y17-25)

王 鵬(1982 —),男，天津人，碩士，副教授，研究方向為民機系統(tǒng)安全性設(shè)計與評估、機載電子硬件適航技術(shù)。

V240.2

A

10.3969/j.issn.1671-637X.2017.11.013