王 鵬, 張 帆, 董 磊, 趙長(zhǎng)嘯

(中國(guó)民航大學(xué),a.天津市民用航空器適航與維修重點(diǎn)實(shí)驗(yàn)室; b.適航學(xué)院，天津 300300)

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

王 鵬a, 張 帆b, 董 磊a, 趙長(zhǎng)嘯a

(中國(guó)民航大學(xué),a.天津市民用航空器適航與維修重點(diǎn)實(shí)驗(yàn)室; b.適航學(xué)院，天津 300300)

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

平視顯示器； 民機(jī)； 概率模型檢驗(yàn)； 形式化模型； 定量分析； 安全性

0 引言

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

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

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

1 概率模型檢驗(yàn)

1.1 概率模型檢驗(yàn)概述

概率模型檢驗(yàn)(Probabilistic Model Checking)通過(guò)形式化方法，驗(yàn)證具有隨機(jī)行為的系統(tǒng)定量屬性[4]。基于平顯系統(tǒng)的概率模型檢驗(yàn)框架如圖1所示，包括以下兩項(xiàng)輸入[5]。

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

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

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

圖1 概率模型檢驗(yàn)框架Fig.1 An overview of probabilistic model checking

1.2 概率模型檢驗(yàn)原理

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

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

設(shè)過(guò)程{X(t),t≥0}為連續(xù)時(shí)間的隨機(jī)過(guò)程，若對(duì)于一切s,t≥0和非負(fù)整數(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)

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

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

(2)

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

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

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

(3)

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

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

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

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

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

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

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

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

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

表2 平顯系統(tǒng)災(zāi)難性失效狀態(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)系到飛機(jī)整機(jī)的可靠性與安全性。由于平顯系統(tǒng)具備模塊化、資源共享等特點(diǎn)，因此對(duì)其進(jìn)行概率模型建模與安全性分析面臨技術(shù)困難。此外，由于模型檢驗(yàn)方法的本質(zhì)是基于對(duì)狀態(tài)空間的窮舉搜索，對(duì)于并發(fā)系統(tǒng)，其狀態(tài)數(shù)目會(huì)隨著并發(fā)量的增加而呈指數(shù)增長(zhǎng)，出現(xiàn)狀態(tài)爆炸問(wèn)題[10]。解決上述問(wèn)題，對(duì)其進(jìn)行概率模型建模時(shí)，采用基于不同粒度的分層建模方法，降低系統(tǒng)復(fù)雜程度，減少狀態(tài)空間數(shù)量。

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

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

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

2.3.1 功能模塊級(jí)概率模型建模

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

設(shè)備級(jí)建模指的是設(shè)備內(nèi)部軟硬件建模。建立設(shè)備級(jí)概率模型時(shí)，首先需要分析設(shè)備整體的失效路徑，即分析失效模式組合導(dǎo)致設(shè)備特定功能失效的失效邏輯。作為HUD內(nèi)部的一個(gè)LRU(航線(xiàn)可更換單元)，左側(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為等式標(biāo)簽，等號(hào)左端為HUDC_L原因造成姿態(tài)誤顯示，等號(hào)右端為HUDC_L內(nèi)部各功能模塊失效模式間失效邏輯。通過(guò)建立上述邏輯等式描述，完成設(shè)備內(nèi)部功能模塊失效模式向設(shè)備級(jí)封裝，即完成設(shè)備級(jí)建模過(guò)程。按上述方法依次完成平顯系統(tǒng)其他設(shè)備的設(shè)備級(jí)建模，在此不再贅述。

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

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

對(duì)于另一子系統(tǒng)，ADN數(shù)據(jù)網(wǎng)絡(luò)原因?qū)е伦藨B(tài)誤顯示，當(dāng)來(lái)自左側(cè)慣性系統(tǒng)的姿態(tài)數(shù)據(jù)經(jīng)過(guò)ADN網(wǎng)絡(luò)后出現(xiàn)錯(cuò)誤，則會(huì)導(dǎo)致左側(cè)平顯姿態(tài)誤顯示，ADN網(wǎng)絡(luò)為雙通道網(wǎng)絡(luò)，當(dāng)A，B兩個(gè)通道均失效時(shí)，對(duì)應(yīng)左側(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)級(jí)概率模型建模

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

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ī)范描述

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

3.2 定量安全性分析

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

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

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

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

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

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

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

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

4 結(jié)論

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

[1] 吳連慧.機(jī)載平顯圖形生成與視頻處理算法研究及其FPGA實(shí)現(xiàn)[D].南京:南京航空航天大學(xué),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.隨機(jī)過(guò)程[M].龔光魯，譯.2版.北京:機(jī)械工業(yè)出版社,2015.

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

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

[10] 侯剛,周寬久,勇嘉偉,等.模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述[J].計(jì)算機(jī)科學(xué),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

王鵬，張帆，董磊，等.基于概率模型檢驗(yàn)的民機(jī)平視顯示系統(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

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

王 鵬(1982 —),男，天津人，碩士，副教授，研究方向?yàn)槊駲C(jī)系統(tǒng)安全性設(shè)計(jì)與評(píng)估、機(jī)載電子硬件適航技術(shù)。

V240.2

A

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