基于概率模型检验的民机平视显示系统建模与安全性分析

王 鹏, 张 帆, 董 磊, 赵长啸

(中国民航大学,a.天津市民用航空器适航与维修重点实验室; b.适航学院，天津 300300)

基于概率模型检验的民机平视显示系统建模与安全性分析

王 鹏a, 张 帆b, 董 磊a, 赵长啸a

(中国民航大学,a.天津市民用航空器适航与维修重点实验室; b.适航学院，天津 300300)

民机平视显示系统(HUD)作为安全关键系统，由于其高度复杂且与其他机载系统结合使用，使得传统系统安全性评估方法难以满足定量安全性分析需求。因此，需要开发基于形式化模型的安全性评估(MBSA)方法，在明确概率模型检验原理及系统高层建模规范基础上，研究平显系统概率模型分层建模方法，建立平显系统概率模型，并描述系统定量安全性属性，展开自动概率模型检验，得出定量安全性分析结论，提高安全性分析效率与运算结果精确度。

平视显示器； 民机； 概率模型检验； 形式化模型； 定量分析； 安全性

0 引言

作为民用飞机航行新技术，平视显示系统(HUD)与其他系统相互综合，将重要的飞行参数(如飞行高度、飞行速度、姿态、航向等)以图形、字符的形式，通过光学部件投影到座舱正前方组合仪上[1]。由于该组合仪高度大致与飞行员的眼睛处于水平位置，因此飞行员透过平显观察舱外景物时，几乎不用改变眼睛焦距就能同时观测到平显上显示的图形和字符信息，从而及时修正飞行姿态，对于减轻飞行员负担，提高飞行员环境感知能力，增强飞行安全性具有重要意义。

随着平显系统集成化程度的提高，平显系统部分功能以模块化形式集成到综合模块化的航电系统(IMA)中，且通过飞控系统、增强视景系统等获取数据及视频信息，使得平显系统高度复杂。作为航电安全关键系统，由于传统基于双V的安全性评估方法[2]存在工作量大、依赖于专家经验且易于出错等问题[3]，需要开发新型的基于模型的自动化分析方法，对民机平显系统展开定量分析，提高安全性评估效率。

针对上述问题，采用基于概率模型检验的形式化安全性分析技术，在分析平显系统物理架构及功能基础上，探索平显系统分层建模方法，深入分析系统内部失效转移逻辑，对系统定量安全性属性展开自动化验证，得出分析结论。

1 概率模型检验

1.1 概率模型检验概述

概率模型检验(Probabilistic Model Checking)通过形式化方法，验证具有随机行为的系统定量属性[4]。基于平显系统的概率模型检验框架如图1所示，包括以下两项输入[5]。

1) 系统高层模型。基于严格的平显系统物理架构及功能分析，捕获平显系统内部各模块失效模式、失效概率及失效转移路径，对系统进行高层模型建模。

2) 形式化属性规范。通过分析平显系统定量安全性需求，将其以时序或稳态逻辑形式表达为系统属性规范。

完成上述平显系统建模与属性规范表达后，基于状态机原理进行自动化底层系统失效状态转移建模，分析失效路径并计算各状态定量概率，得出安全性分析结论。

图1 概率模型检验框架Fig.1 An overview of probabilistic model checking

1.2 概率模型检验原理

自动分析系统概率行为并建立系统高层模型，是概率模型检验的关键内容。概率模型检验支持离散时间Markov链(DTMC)、连续时间Markov链(CTMC)及Markov决策过程(MDP)[6]。在民机系统安全性分析过程中，采用CTMC对系统行为进行分析。

1) 连续时间Markov链定义。

设过程{X(t),t≥0}为连续时间的随机过程，若对于一切s,t≥0和非负整数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}是一个连续时间Markov链[7]。通常，以Pij(t)表示当前处于状态i的Markov链在附加时间t后处于状态j的概率，即

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

(2)

2) 状态转移及运算原理。

连续时间Markov链能够表示随着时间变化，系统可能出现的各种状态及状态间的转移关系。在基于概率模型检验的民机系统安全性分析中，各状态指的是系统可能出现的失效模式，转移关系指正常模式与失效模式以及各失效模式之间的转换逻辑。完成系统高层建模后，概率模型基于CTMC将高层模型转换为底层模型，进行概率计算，以支持定量安全性分析。对应底层模型举例如图2所示，并得到其相应的微分方程组。

图2 CTMC底层模型Fig.2 CTMC bottom-level model

(3)

通过拉氏变换，概率模型检验将自动求解上述微分方程，可得到经过确定的时间t，处于上述4种状态的概率，完成定量计算过程。

1.3 概率模型高层建模规范

概率模型检验方法通过结构化的高级语言对系统建模,该语言由最基本的模块及变量组成。通过建立一系列表示系统各组分的并行模块，以变量形式定义各模块的失效模式及其概率，并采用逻辑等式的方式，表达模块中变量之间、模块与模块间的相互关系。模块的失效行为由一系列命令表示，对于CTMC，采用以下语法表达命令：[action](guard) -> (rate):(up-date);其中，命令起始于[]，action为同步符号；(guard)表示模块中的变量，在系统安全性分析建模中，变量通常为失效模式；->表示状态转移，执行该状态转移的条件是(guard)为真；(update)表示转移后的状态；(rate)表示发生该转移的概率。

概率模型采用标准的CSP并行代数处理器将各模块进行集成，可更精确地指定模块间的同步关系。同时，对于模块中各状态之间、模块与模块之间的逻辑关系，通过逻辑等式的形式描述。基于布尔表达式，逻辑等式将模块变量以基础逻辑形式(如NOT：！，AND：&，OR：|)衔接，在系统安全性分析建模时，便于模块及功能的封装。

2 基于概率模型检验的平显系统建模

2.1 平显系统物理架构与典型功能分析

典型的民用飞机平显系统主要是由平显计算机(HUDC)、组合仪(HCU)、投影组件(HPU)组成[8]。通过ADN数据网络及航空总线，由左右两侧HUDC接收来自于飞机其他航电设备的各种数据，如速度、加速度、姿态、位置、风速、导航信息、引导提示、告警信息等[9]，经处理、融合后生成HUD 显示图像，再经过总线分别传递至左右两侧HPU，最终显示于机长与副驾HCU。根据平显系统的主要功能，识别其交互界面，如表1所示。

作为概率模型检验的系统安全性需求输入之一，通过功能危害性评估(FHA)识别出平显系统的失效状态及影响等级，其中,灾难性失效状态(I类)如表2所示。此处，选取双侧HUD姿态误指示这种失效状态，作为安全性分析的对象。图3是HUD在显示飞行姿态功能下对应的系统物理架构。

表1 平显系统主要功能及交互界面

表2 平显系统灾难性失效状态

图3 基于飞行姿态显示功能的平显物理架构Fig.3 HUD physical architecture based on attitude display

2.2 平显系统概率模型分层建模方法

平显系统作为重要航电系统，关系到飞机整机的可靠性与安全性。由于平显系统具备模块化、资源共享等特点，因此对其进行概率模型建模与安全性分析面临技术困难。此外，由于模型检验方法的本质是基于对状态空间的穷举搜索，对于并发系统，其状态数目会随着并发量的增加而呈指数增长，出现状态爆炸问题[10]。解决上述问题，对其进行概率模型建模时，采用基于不同粒度的分层建模方法，降低系统复杂程度，减少状态空间数量。

由于在进行初步系统安全性评估(PSSA)时，需要根据ARP 4754A[11]，将功能研制保证等级由系统向子系统、设备及软硬件分解，因此，在概率模型分层建模时，以功能为上下层级连接依据，从软硬件功能模块或内部元件开始建模，通过逻辑等式逐步向上一级封装，分别建立元件级/功能模块级、设备级、子系统级、系统级4层模型，建模层次如图4所示。

图4 概率模型层次图Fig.4 Hierarchical probabilistic model

2.3 平显系统概率模型建模

2.3.1 功能模块级概率模型建模

平显系统概率模型建模从设备内部软硬件功能模块开始。由于平显系统为复杂航电系统，因此设备内部软硬件功能模块复杂，不再详细描述。此处以图3中左侧HUDC(HUDC_L)为例，根据选定的失效状态，双侧HUD飞行姿态误显示，识别相应失效信息如表3所示，对应概率模型为3个模块，图形处理、图形存储与数据传输；每个模块内定义了失效模式及发生概率。

表3 左侧HUDC故障模式与影响分析

根据表3失效信息，建立左侧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 设备级概率模型建模

设备级建模指的是设备内部软硬件建模。建立设备级概率模型时，首先需要分析设备整体的失效路径，即分析失效模式组合导致设备特定功能失效的失效逻辑。作为HUD内部的一个LRU(航线可更换单元)，左侧HUDC内部模块失效模式造成姿态误显示的失效逻辑如下：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原因造成姿态误显示，等号右端为HUDC_L内部各功能模块失效模式间失效逻辑。通过建立上述逻辑等式描述，完成设备内部功能模块失效模式向设备级封装，即完成设备级建模过程。按上述方法依次完成平显系统其他设备的设备级建模，在此不再赘述。

2.3.3 子系统级概率模型建模

平显系统包括两个子系统，分别为平显及ADN数据网络。同理，在明确子系统内部各设备特定功能失效的条件下，通过建立各设备失效逻辑，可完成设备向子系统的封装，即子系统级概率模型建模。首先分析左侧平显子系统姿态误显示失效逻辑，左侧平显姿态误显示是由HUDC_L图像缺陷、左侧HPU图像缺陷及A429误码导致，对应子系统级建模如下：formulaHUD_L_wrong_attitude=(HUDC_L_wrong_attitude)|(HPU_L_wrong_image_failure_mode)|(A429_7_wrong_data_failure_mode)。

对于另一子系统，ADN数据网络原因导致姿态误显示，当来自左侧惯性系统的姿态数据经过ADN网络后出现错误，则会导致左侧平显姿态误显示，ADN网络为双通道网络，当A，B两个通道均失效时，对应左侧平显姿态误显示。子系统建模如下：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 系统级概率模型建模

完成上述子系统建模后，对子系统进行逻辑等式封装，得到左侧平显姿态误显示系统级概率模型，其失效由惯性系统或ADN数据网络或平显导致；同理可得右侧系统级概率模型，二者同时发生，导致失效状态双侧平显姿态误显示发生。对应左、右两侧及双侧系统级模型为：

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 平显系统定量安全性分析

3.1 系统属性规范描述

验证系统行为是否满足定量安全性需求，必须将系统行为进行形式化描述，即系统属性规范描述。针对CTMC的定量属性验证，应在捕获系统定量属性需求的基础上，采用CSL连续随机逻辑语言对系统属性进行形式化规范。基于CSL语言的逻辑形式包括两种，时序逻辑和稳态逻辑[12]。通常，稳态逻辑用于检验系统长时间运行条件下，某状态出现的概率。然而由于稳态逻辑受限于平衡状态，对于飞机系统安全性评估中需要检验的属性，如平均每飞行小时某失效状态出现的概率，应采用时序逻辑形式描述。如果系统在2 h之内发生失效状态A的概率可以表示为：P=？[true U<=2(system_FC_A)]。完成属性描述后，概率模型将自动展开属性检验，得出结论。

3.2 定量安全性分析

完成平显系统概率模型建模后，对其定量安全性属性展开自动化验证。根据系统安全性需求，要求双侧HUD姿态误指示发生概率应小于等于1E-9平均每飞行小时，设该机型飞机每次飞行平均飞行小时为2 h，根据这个需求从设备级起逐级展开定量验证，相应左侧系统、右侧系统及系统整体失效的时序逻辑如下：

概率模型检验器基于Markov状态转移原理，建立系统底层运算模型，并通过基于符号模型检测的MTBDD(多终端二叉决策图)对状态进行归并与化简，且进一步利用稀疏引擎、MTBDD引擎及混合引擎[13]展开自动定量概率运算后，得到双侧平显系统姿态误指示的定量安全性分析结果如表4所示。

表4 双侧平显系统失效概率分析

经过对双侧平显系统姿态误指示的概率模型自动验证，共分析了4 194 304个状态，可能的状态转移达46 137 345个，通过遍历验证，最终得到失效状态“双侧平显系统姿态误指示”的概率为平均每飞行小时6.035E-9。根据系统安全性需求，该值应小于等于平均每飞行小时1E-9，因此，不满足系统安全性需求，可通过提供计算保守性证明或重新设计调整物理架构，以进一步满足该安全性需求。

在此，考虑对物理架构重新调整，使系统满足安全性需求。逐级检验左侧平显系统定量属性，得到安全性结果如表5所示。

表5 左侧平显系统失效概率分析

根据表5结果可知，左侧HUDC及HPU失效导致姿态误指示发生的概率较大，因此对两侧HUDC物理架构重新进行安全性设计。由于HUDC功能模块中图形处理模块承担着图形反走样、预畸变处理以及分辨率调整等重要功能，且这些功能均由同一个FPGA执行，因此，考虑在HUDC内部设置CPU，对该功能模块进行监控，当处理后的图像不符合处理前信息时，由CPU发出错误指令，终止图像显示。在该物理架构下，经过属性验证，HUDC失效导致姿态误指示的概率为平均每飞行小时6.382 8E-9，平显系统姿态误指示的定量安全性分析结果如表6所示。

表6 新架构下双侧平显系统失效概率分析

架构调整后，失效状态“双侧平显系统姿态误指示”的概率为平均每飞行小时2.602E-10，满足系统安全性需求，定量系统安全性分析工作完成。

上述定量安全性分析均由概率模型检验器PRISM完成,该工具是由英国伯明翰大学、牛津大学及格拉斯哥大学共同设计开发的形式化建模与定量验证工具。目前已广泛应用于不同领域，包括通信、多媒体协议、安全协议、动态资源管理规划、生物系统等，为系统安全性分析提供了巨大支持[4]。在此基础上，将其运用于民机复杂航电系统定量安全性分析，具有一定价值与意义。

4 结论

本文提出了基于概率模型检验的形式化安全性分析方法，有效解决了平视显示系统高复杂性、模块化程度高的问题。基于Markov理论，将系统内各模块失效模式作为Markov状态，在明确各状态间的转移关系基础上，采用分层建模技术，建立各层级概率模型，有效降低了系统复杂程度；最后通过时序逻辑描述检验系统定量安全性需求，以遍历方式自动完成所有状态及转移检验，得出定量概率验证结果，该结果能为系统安全性评估提供有效支持，降低安全性评估工作量，提高定量分析精度。

[1] 吴连慧.机载平显图形生成与视频处理算法研究及其FPGA实现[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版.北京:机械工业出版社,2015.

[8] 王全忠,高文正.平视显示器在民用飞机上的应用研究[J].电光与控制,2014，21(8):1-5.

[9] 费益,季小琴,程金陵.平视显示系统在民用飞机上的应用[J].电光与控制,2012，19(3):95-99.

[10] 侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[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

王鹏，张帆，董磊，等.基于概率模型检验的民机平视显示系统建模与安全性分析[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

国家自然科学基金委员会-中国民航局民航联合研究基金资助(U1533105)；中国民航大学科研启动基金项目(2013QD 04X)；天津市自然科学基金联合资助项目(15JCQNJC42800)；中国民航大学科技创新基金(Y17-25)

王 鹏(1982 —),男，天津人，硕士，副教授，研究方向为民机系统安全性设计与评估、机载电子硬件适航技术。

V240.2

A

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