基于故障耦合模型的增强飞行视景系统形式化建模与分析

伍小辉

(中航机载系统共性技术有限公司，江苏 扬州 225000)

0 引言

增强飞行视景系统(Enhanced Flight Vision System， EFVS)是一种能够提高飞机起降能力和飞行安全的机载电子系统，获取飞机前方外景的红外图像，计算生成各种飞行操纵信息，信息叠加后投射至飞行员前方，以降低机组工作负荷[1-3]。

针对复杂关键系统的失效分析与验证，学术界已逐步引入SIMFIA[4]，AltaRica[5]，概率模型[6]以及架构分析与设计语言[7-8]等形式化方法。相较于传统分析方法，基于模型的安全性分析利用形式化模型提高了分析过程与效率。然而，现有的形式化方法主要针对系统的功能架构与运行状态展开建模，并未考虑系统的失效模式及故障传播行为，无法适应EFVS多样复杂的失效模式。

基于此，本文提出一种基于故障耦合模型的EFVS形式化建模方法，从故障传播的角度，建立EFVS分层故障耦合模型，结合EFVS典型的系统失效状态，引入NuSMV模型检验工具[9]，输出最小割集。

1 EFVS故障传播分析

不同的应用场景对模型的复杂程度要求不同，针对EFVS的故障传播分析，构建如图1所示EFVS功能架构模型。

图1中，EFVS包含增强视景系统(Enhanced Vision System，EVS)、平显计算机(Head-Up Display Computer，HUDC)、平显投影组件(Head-Up Display Projector Unit，HPU)和平显组合仪(Head-Up Display Combiner Unit，HCU)4个子系统[3]。在此基础上，从EFVS故障传播的静态特性和动态特性两个方面分析故障传播关系。一方面，通过构建EFVS功能层与资源层之间的映射交互关系分析EFVS故障传播模式；另一方面，结合EFVS功能架构，分析EFVS系统故障传播模式。

图1 EFVS功能架构图Fig.1 The functional architecture of EFVS

1.1 EFVS功能交互模型构建

EFVS设计目标可通过特定的功能来实现。EFVS主体顶层功能包括飞行与导引信息显示、EFVS系统控制、EFVS工作状态管理以及画面调节4大功能。上述功能的实现依托于系统底层成像模块、非均匀校正模块、图像格式转换模块、数据处理模块以及监控模块等。基于此，从功能-资源层两个维度，构建EFVS功能交互模型，输出EFVS不同层级间的映射关系，确定EFVS故障传播粒度。

EFVS功能和系统资源层之间的分布和映射关系可以概括为一对一、一对多、多对一和多对多。系统的故障传播源主要包括系统部件自身失效、各模块间的失效耦合、人为因素以及外部环境影响等。根据摄动理论[10]，系统底层模块失效或性能偏差等摄动因素的积累是系统故障传播的主要因素，系统部件的单一失效通常不会导致系统故障。实际情况中，EFVS资源层各模块间的功能交互复杂，EFVS系统故障从较低的模块级层次结构传播到较高的层次结构。基于此，本文通过EFVS资源层引入故障传播问题，将资源层模块级元素功能失效作为故障触发点,如图2所示。

图2 EFVS功能交互模型Fig.2 The functional interaction model of EFVS

1.2 EFVS故障传播模式分析

根据图1所示EFVS功能层次架构，分析EFVS系统底层各模块间的数据流，将EFVS系统的故障传播分为子系统内传播与不同子系统间传播两种模式，如图3所示。

图3 EFVS故障传播模式Fig.3 Fault propagation patterns of EFVS

1) 子系统内故障传播模式。

如图3所示，在子系统内故障传播模式下，故障通过EVS中GPM模块与ICM模块之间的功能交互传播。GPM模块的故障状态决定了其输出的故障模式，并通过其接口传播到ICM模块作为其输入故障模式。系统临界状态下，同一子系统中紧耦合模块之间的故障传播可能直接导致系统功能失效[11]。此外，故障在同一子系统中的传播是最简单的传播模式，也是后续其他故障传播类型的基础。

2) 不同子系统间故障传播模式。

不同子系统间故障传播模式是模式1)的扩展，故障通过不同子系统中各模块之间的功能交互传播，反映了故障在系统各子系统间的扩散交互性。如图3所示，从EVS中ICM模块到HUDC中ITM模块的故障传播行为涉及到的模块位于不同的子系统中，反映了系统中不同子系统之间的功能交互。

2 EFVS故障耦合形式化建模

考虑到EFVS多层级的复杂架构以及底层模块间的复杂交互关系，本文提出一种基于故障耦合模型EFVS形式化建模方法。引入SMV形式化模型语言，结合上文所述EFVS故障传播模式，采用分层建模方式从故障传播的角度构建EFVS形式化模型。

EFVS建模流程总体分为3个阶段：首先，对EFVS架构及数据流进行抽象，定义模块级Module，包括各模块的功能描述及接口定义，在此基础上输出EFVS底层各模块的名义模型；其次，EFVS故障耦合模型的构建依托于EFVS各模块的失效行为扩展描述、各模块故障状态与正常状态间的关联分析以及故障触发条件的定义；最后,通过分析各模块间的功能交互关系，定义各子系统间逻辑关系与接口，自底向上对EFVS模型进行封装。

2.1 EFVS模块级名义模型构建

1) EFVS架构及数据流抽象。

针对EFVS故障传播与建模分析，系统架构自上而下抽象为系统—子系统—模块级。根据EFVS的系统物理架构、系统设计规范及系统需求文档，识别EFVS的飞行与导引信息显示、系统控制、系统工作状态管理以及画面调节4大功能。此外，EFVS功能危害性评估得出Ⅲ类及以上失效状态均与系统显示功能相关。基于此，本文从飞行信息数据、图像数据以及飞行导引信息3方面对EFVS数据流进行抽象。

2) EFVS模块功能描述及接口定义。

EFVS内部模块是执行其特定功能的最小单元，分析底层各模块输入输出，明确模块间功能交互关系及内部处理逻辑，定义各模块接口，建立EFVS模块级名义模型。考虑篇幅，后续建模过程以EVS内部模块接口控制模块ICM为例展开说明。

ICM模块旨在对压缩前图像数据进行数据格式转换，并判断转换前后的图像数据一致性，若不一致，则输出“画面不一致”警告信息，此外，ICM模块还接收前沿4个模块的工作状态信息，判断其工作状态，输出警告信息。

根据前述EFVS数据流抽象，对ICM模块的输入和输出进行离散化抽象，模块正常状态下，当ICM检测到数据格式转换前后的图像相同，且监测到前沿4个模块工作状态正常，即无警告信息输出，图像数据包括正常(Normal)和空(Empty)两个状态,其中,Empty表示ICM模块未接收或未发送的数据。ICM模块名义模型如下所示。

Module

EVS_Interface_Control(image_in1,image_in2,OSM_status1,

DM_status2,NUCM_status3,GPM_status4)

Var

out1:{Normal,Empty,};

out2:{0,1};

Assign

next(out1):=

case

(next(image_in2)=Normal):Normal;

(next(image_in2)=Empty):Empty;

True:out1;

esac;

next(out2):=

case

((next(image_in1)=next(image_in2)) &

next(OSM_status1) & next(DM_status2) &

next(NUCM_status3) & next(GPM_status4)):True;

True:out2;

esac;

Assign

init(out1):= image_in2;

init(out2):= True。

2.2 EFVS模块耦合模型构建

1) EFVS模块故障行为描述及影响分析。

EFVS底层模块的故障行为形式化描述是构建系统层次耦合模型的关键步骤，建模过程中应重点考虑各模块故障传播的初始状态、故障传播的目标模块及其对目标模块的失效影响。针对EFVS层次耦合模型，不同的Module对应不同的模块，不同的层次结构对应不同的子系统。

针对EFVS底层模块故障行为描述，以ICM模块为例，声明模块初始状态、状态转移条件和相应的参数，对前述ICM名义模型数据流进行扩展，引入故障变量“ICM_data_loss”和“ICM_data_error”，同时可通过Define定义各模块失效模式和关联参数，以声明上述故障变量对应的局部影响。建模细节如下所示。

Module

EVS_Interface_Control_Clog(image_in1,image_in2,OSM

status1,DM_status2,NUCM_status3,GPM_status4)

Var

out1:{Normal,Empty,error,loss};

out2:{0,1};

IVar

ICM_data_error:boolean;

ICM_data_loss:boolean;

Assign

init(out1):= image_in2; init(out2):= True;

next(out1,out2):=

…

Affects out1,out2 With

Mode nonuniform_correction_error:Permanent

(data term_1 << Empty,data term_2 <

input_1 <> out1,data input_2 <

data varout_2 >> out2,event failure >>

ICM_data_error);

Mode nonuniform_correction_loss:Permanent

…

Define

out1:= loss >> HUDC_ITM1_data1;

out2:= False。

2) EFVS模块故障状态与正常状态关联分析。

EFVS某一模块故障状态与正常状态的关联分析即为故障模型与名义模型的集成耦合。引入Assign和Define定义独立变量与独立状态，构建对应模块的耦合模型。考虑到简化建模过程，无需在耦合模块定义原始模型的重复变量，上述变量可通过对应的故障或名义模型的输出状态直接调用。以接口控制模块ICM为例，建模如下所示。

Module

EVS_Interface_Control_Cou:{Normal,Clog};

EVS_ICM_Normal:EVS_Interface_Control;

EVS_ICM_Clog:EVS_Interface_Control_Clog;

Assign

next(Coupling_out1):=

…

next(Coupling_out2):=

…

Define

In_Coupling:=!(EVS_Interface_Control_Cou=Clog);

Coupling_out1:=

…

Coupling_out2:=

…。

3) EFVS各模块故障触发条件定义。

针对EFVS故障触发条件定义，以接口控制模块ICM为例，结合上述ICM名义模型以及1.2节故障传播模式，明确ICM输入输出事件，分析其对目标构件的失效影响，具体建模细节如下所示。

Module

EVS_Interface_Control_Cou:{Normal,Clog};

EVS_ICM_Normal:EVS_Interface_Control;

EVS_ICM_Clog:EVS_Interface_Control_Clog;

Assign

init(Coupling_out2):= True;

next(Coupling_out2):=

case

(!(next(image_in1)=next(image_in2))

| !next(OSM_status1) | !next(DM_status2)

|!next(NUCM_status3) | !next(GPM_status4)):

False;

True:Coupling_out2;

esac;

…。

2.3 EFVS和子系统级模型封装

1) EFVS子系统级模型封装。

EFVS子系统级模型封装主要过程包括子系统内部各模块间功能交互分析、子系统输入输出以及内部逻辑分析。针对EFVS内部各模块间功能分析，首先将其视为黑盒模型，确定外部输入输出，然后将其视为白盒模型，分析系统内部数据传输逻辑，以增强视景系统子系统EFVS子系统为例，其内部数据处理先后经过格式转换、畸变校正直至最后接口控制模块的图像数据格式转换与压缩。对应到实际的建模过程中，模型的封装过程即为底层模块实例化为上层模型的Module，将底层模块的外部输入作为上层模块Module的形式参量，即将底层模块作为上层变量(Var)声明，根据图1所示EFVS功能架构及数据流抽象，各模块一一整合封装，即为对应的EFVS子系统模型。相关EVS模型如下所示。

Module

EVS_Cou_model(image_environment,BFD_to_EVS)

Var

OSM_Cou:EVS_Optical_Imaging_Cou(image_environment);

OSM _Cou:EVS_Optical_Imaging_Cou(image_environment);

DM_Cou:EVS_Detector_Cou(OSM_Cou.out);

NUCM_Cou:EVS_NonUniform_Correction_Cou

(DM_Cou.out1,BFD_to_EVS);

GPM_Cou:EVS_Graphic_Processing_Cou(NUCM_ Cou.out1);

ICM_Cou:EVS_Interface_Control_Cou

(GPM.out1,GTM.out1,DM.out2,NUCM.out2,

GPM.out2,GTM.out2)。

2) EFVS系统级模型封装。

针对系统级模型的封装，同理将子系统模型实例化为顶层Main Module的形式参量，子系统依次声明变量Var，即为最终EFVS形式化模型，最后进行EFVS形式化模型的验证。EFVS形式化模型如下所示。

Module

Var

image_environment:{Normal,error,Empty};

BFD_to_EVS:{Normal,error,Empty};

BFD_to_HUDC_Primary:{Normal,Empty,

implicit_error,explicit_error};

BFD_to_HUDC_Standby:{Normal,Empty,

implicit_error,explicit_error};

EVS:EVS_Cou_model(image_environment,

BFD_to_EVS);

HUDC:Head_Up_Display_Computer_Cou

(EVS.ICM_Cou.out1,BFD_to_HUDC_Primary,

BFD_to_HUDC_Standby);

HPU:HUD_Project_Unit_Cou(HUDC.ITM2_Cou.out1,

HUDC.ITM2_Cou.out2,HUDC.ITM2_Cou.out3);

HCU:HUD_Combine_Unit_Cou(HPU.ISM_Cou.out1,

HPU.ISM_Cou.out2,HPU.ISM_Cou.out3,

EVS.ICM_Cou.out2,HUDC.DPM_Cou.out3,

HUDC.MM_Cou.out4,HPU.MM_Cou.out)。

3 EFVS耦合模型形式化验证与分析

EFVS耦合模型的形式化验证，旨在确保形式化模型的正确性。根据图1所示EFVS的功能物理架构、系统设计规范及系统需求文档，将EFVS的系统需求分配至系统各部件和模块，采用计算树逻辑(Computation Tree Logic，CTL)构造EFVS形式化规约，引入模型检验工具NuSMV进行模型检验。若某项规约不满足，即上述EFVS耦合模型未通过验证，需要检查建模过程并修改模型，直至所有规约都满足。

1) EFVS需求形式化规约描述与验证。

根据2.1节EFVS数据流抽象均与系统显示功能相关，故后续形式化规约描述以显示功能相关需求为主。以HUDC某一需求为例：HUDC内部数据处理模块DPM输出的飞行数据和导引信息不能出现机器可识别的明显错误，相应CTL形式化规约为SPEC AG(!(DPM.out1=explicit_error)&!(DPM.out2=explicit_error))，针对EFVS故障耦合模型形式化验证结果如图4所示，由图可知各需求均通过验证。

图4 EFVS形式化模型验证结果Fig.4 Verification results of the formal model of EFVS

2) 最小割集生成。

模型检验工具NuSMV可以自动化检查模型，以验证模型是否满足指定的系统属性或需求。将EFVS顶层失效状态以形式化规约的形式作为检验过程的输入，可得到该顶事件对应的所有失效组合集，通过分析失效事件间逻辑关系，得到顶事件的最小割集。以EFVS典型顶层失效状态“空速显示错误且无告警”为例，构造失效状态形式化规约，引入检验工具，输出以该失效状态为顶事件、以各模块故障模式为底事件的故障树最小割集，整理如表1所示。

表1 失效状态“空速显示错误且无告警”最小割集Table 1 The minimum cut set of failure state “Airspeed display error with no alarm”

4 结论

本文提出了一种基于故障耦合模型的EFVS形式化建模方法。构建了EFVS的功能交互模型，得出了2种系统故障传播模式；在此基础上，对EFVS的物理架构及数据流进行了抽象，从EFVS模块级名义模型的构建、模块级耦合模型的构建以及系统模型的封装3个方面建立了EFVS故障耦合形式化模型；最后，引入模型检验工具对EFVS模型进行了验证，给出了典型失效状态最小割集。上述工作有助于提高失效分析过程的效率，同时为EFVS安全性分析提供指导。