面向驾驶舱显示系统需求的形式化建模与分析

战芸娇，魏 欧，胡 军，王立松，谷青范

(1.南京航空航天大学 计算机科学与技术学院，江苏 南京 211106;2.中国航空无线电电子研究所，上海 200000)

1 概 述

需求分析是软件开发流程中的第一步，也是最重要的一步。在航空航天领域等实际的安全关键系统中，由于需求的复杂性、缺乏统一的需求模型、需求描述的结构混乱和语言歧义等原因[1]，往往造成需求中存在大量的不一致和不完备。相关研究表明，在系统维护阶段修改所发现的需求错误所需要的工作量，大约是更改需求分析阶段发现的错误所需的工作量的200倍[2]。因此，减少需求中的错误至关重要，不仅能够保证系统的安全性，也可以减少系统开发的成本。

驾驶舱显示系统[3](cockpit display system)是驾驶员和飞机进行信息交互重要的机载系统。通过将传统的飞行仪表信息进行数字化综合处理，驾驶舱显示系统采用多种显示器按需展现各种不同数据，如主飞行显示器、导航显示器等，增强了驾驶员的态势感知能力，简化了对飞机的操纵导航，使得驾驶员能够专注于最为相关的信息，降低飞行成本。

机载软件[4-5]通常都具有规模庞大，数据关联复杂，安全级别要求高等特点。其需求存在可维护性差，相同操作描述不一致，不可验证信息较多和低层次与高层次需求不平衡等问题。在显示系统广泛应用的同时，在实际中也时常发生由于显示系统错误而引起的安全事故。例如，2005年8月1日，马来西亚航空公司的一架波音777-200ER从珀斯飞回吉隆坡，期间主飞行显示器(PFD)的速度显示区域发生显示了飞机同时接近高速极限值和低速极限值的冲突信息，致使飞行员立即解除自动驾驶并紧急降落在珀斯[6]。这些事故都造成了生命、财产等的重大损失，影响巨大。对于驾驶舱显示系统而言，为保障驾驶员能够对飞机飞行中的状况做出正确的判断、避免事故的发生，在开发早期发现需求中存在的错误，可以减少需求错误对系统造成的影响，提高系统的安全性。因此，对驾驶舱显示系统的需求进行严格的定义和分析以及错误检测显得尤为重要。

针对驾驶舱显示系统这样特定应用的系统需求，需要判定其是否满足一致性和完备性。从广义上来说，一致性保证需求中不存在矛盾的信息，完备性保证需求中必须包含那些对于系统正常工作、保证系统安全所必要的信息。因此，应检测需求中是否存在以下问题：

(1)检测出需求中未定义的显示情况，即完备性问题。目的是避免显示器上出现需求中没有定义的某种显示信息。

(2)检测出需求中出现的显示不确定性问题，即一致性问题。目的是避免显示器上出现矛盾的信息显示。

(3)检测出需求中缺失的并且影响系统安全的信息，如数据的时间边界、数据的有效性等。

T-VEC工具是对复杂系统的需求阶段进行错误检测与验证，并对设计阶段进行仿真的工具。1989年以来，其广泛应用在飞机领域的安全关键性系统、实时系统和许多嵌入式系统中。文中主要利用T-VEC的测试向量生成工具，对表格式需求进行测试验证。通过对变量和条件等相关需求模型的输入，对需求进行编译，以检测需求中的各种错误和特性。

针对以上问题，为了找到驾驶舱显示系统这样的安全关键系统需求中的错误，就需要一套完整的方法来对需求进行一致性和完备性检测工作。文中以四变量模型为基础，提出了具体的建立驾驶舱显示系统的需求模型的方法，包括对需求描述方式和严格的语义，支持需求的一致性和完备性的T-VEC检测工具。

2 四变量模型

四变量模型[7-9](four-variable model)是由Parnas提出来的用以指明需求的方法，如图1所示。

图1 四变量模型

四变量模型中的变量是时间连续型函数，分为四类变量：

(1)监督变量(monitored variables，MON)：系统需要观测的外部环境量；

(2)受控变量(controlled variables，CON)：受系统控制的环境量；

(3)输入变量(input variables，INPUT)：由传感器等输入设备将监督变量转换而来的变量；

(4)输出变量(output variables，OUTPUT)：发送到输出设备上的、改变受控变量的变量。

例如，监督变量可以是飞机在飞行中的飞行高度和飞行速度，受控变量可以是显示仪表盘上飞行高度和飞行速度值的显示；相应的输入输出变量可以是软件读入的、写出的ARINC-429总线上的数据。

在这些变量上，定义了4种数学关系：

(1)NAT：施加在环境量上的自然限制，例如飞机的最大爬升率；

(2)REQ：定义了系统需求，指明受控变量与监督变量的关系。系统需求REQ是可行的，当且仅当REQ中考虑了NAT中的所有环境限制条件。

(3)IN：描述了监督变量和输入变量之间的关系。IN模拟了输入硬件接口，如传感器和模数转化器；

(4)OUT：描述输出变量和受控变量之间的关系。OUT模拟了输出硬件接口，如数模转换器和作动器。

3 驾驶舱显示系统的需求模型

结合驾驶舱显示系统的特点，利用四变量模型框架找出需求中的变量和关系，再利用表格符号的形式将需求中的关系表示出来，建立需求模型。

3.1 需求的组成

对系统进行准确的描述从而形成需求，意味着需要确定系统、子系统和组件的行为(并无必要知道行为是如何具体实现的)。Parnas最初提出的四变量模型是用来准确描述系统需求、并形成相应需求文档的方法。

针对驾驶舱显示系统中输入变量对显示信息的影响——一组输入变量取值情况对同一显示造成的影响不同，且这些变量之间存在依赖关系，对输入变量进行分类。在驾驶舱显示系统上所显示的信息包括两类：一类是数值、文本或图形信息，另一类是数值、文本或图形的样式信息(如颜色和字体)。将驾驶舱显示系统需求的输入变量分为显性变量(explicit variables)和隐性变量(implicit variables)。显性变量：参数(输入变量)的值直接决定了显示器上数值、文本或图形信息的显示；隐性变量：参数的值仅仅影响数值、文本或图形的显示样式。其中，显性变量和隐性变量对系统安全造成的影响有所不同，显性变量失效直接造成显示器上相关区域的读数/文本、图形信息为空，飞行员无法从显示器上得知任何有关飞机的状态信息，而隐性变量仅仅影响了显示器上显示信息的样式；隐性变量在显示器上的显示依赖于显性变量的有效性/取值情况，只有在显性变量有效且取特定值情况下，隐性变量的取值情况才会对显示信息造成影响。

另外，为了更好地利用四变量模型准确描述驾驶舱显示系统需求，以便用表格符号对需求中的关系进行表示，需要提供两种额外的结构：条件(condition)和事件(events)。条件是定义在系统输入和输出上的谓词；当两个或多个隐性变量之间的大小关系发生变化，就表示一个事件发生。

图2是结合显示系统的体系结构[10]，参考四变量模型，描述驾驶舱显示系统需求的结构概念图。其中，传感器(sensor)采集外部环境的监督变量(monitor variables)，将其转换成系统可识别的输入变量，并传递给显示系统控制单元；子系统(subsystem)采集来自系统内部的监督变量—飞机系统自身的状态信息，如：FADEC采集引擎参数和控制引擎，通过转换传递给显示系统控制单元；cockpit display controller unit表示处理从传感器和其他子系统传递而来的参数的处理单元，一方面，它将处理后的显示信息指令传递给显示单元，另一方面，将产生的指令反馈给自身(如图中黑色箭头所示)，作为系统内部其他功能的控制条件；cockpit display unit表示显示单元，接收来自处理单元处理后产生的显示信息指令，并在显示器上给予特定的显示。

图2 驾驶舱显示系统需求结构概念图

3.2 需求的表格符号表示

系统开发工程师发现：利用表格表示需求[11]，不仅有利于开发人员对系统的理解和开发，还能将大量的需求信息准确地表示出来[12]。因此，在利用四变量模型找出系统需求中存在的各个组件和变量的基础上，利用表格符号[13]来表示需求中变量之间的关系。鉴于驾驶舱显示系统内部各个组件的功能不同，分别定义不同的表格予以表示：对于传感器和子系统，这两种组件都是将监督变量(来自内部环境和外部环境)转换成显示系统控制单元可识别的量，因此，定义输入映射表(mapping table of input)作为监督变量和输入变量的对应关系；对于显示单元，它接收来自显示控制单元的输出变量(显示指令)，并控制显示单元的受控变量的显示，因此，定义输出映射表(mapping table of output)作为输出变量和受控变量的对应关系；对于驾驶舱显示系统控制单元到显示单元的特殊性—在不同的显示逻辑下，将从传感器和其他子系统传递而来的参数，在显示单元上予以相应的显示—定义三种表格：映射表(mapping table)、事件表(event table)和条件表(condition table)。这三种表格都对应了四变量模型中的SOF，而且，这里的显示控制单元的输出变量是与受控变量有关的，每一个表格中的输出变量(输出变量组)都唯一对应一个受控变量。映射表：与受控变量相关的输出变量的取值情况由输入变量的取值情况确定；事件表：与受控变量相关的输出变量的取值情况取决于输入变量的取值情况和所发生的事件；条件表：与受控变量相关的输出变量的取值情况取决于输入变量的取值情况和当前的条件。除此之外，还需要定义输入变量表格(input table)和输出变量表格(output table)，确定输入和输出变量的类型、取值范围，不仅有利于查看系统中所有的输入和输出变量，还方便后续对需求的一致性和完备性检测工作。

4 需求模型的语义

上一节，通过参考四变量模型，利用表格符号，将用自然语言描述的需求转换成表格符号表示的需求，建立需求模型。接下来，需要为需求模型提供精确的语义[14]。这里的需求模型，对于SOF，定义了输出根据输入或者输入、条件(事件)的改变而发生的变化；描述了从表格中导出的表格函数(table function)—表格符号的形式化表示。这些表格函数不仅定义了从输入到输出或者输入、条件(事件)到输出的映射关系，还定义了监督变量和输入变量、输出变量和受控变量的映射关系。定义一个七元组(MV,CV,D,C,E,F,VS)来表示该需求模型，其中D表示数据项，包含输入和输出变量，D={IP,OP}，输入变量分为显性变量和隐性变量，即IP={EX_IP,IM_IP}。

为了阐述形式化模型，有关元组的定义如下：

(1)七元组元素：模型中的监督变量、输入、输出和受控变量，以及条件、事件、输入输出的取值范围。定义以下集合：

MV：非空的不相交的监督变量集合，MV={mv1,mv2,…,mvl}，mv1,mv2,…,mvl称为监督变量；

CV：非空的不相交的受控变量集合，CV={cv1,cv2,…,cvk}，cv1,cv2,…,cvk称为受控变量；

IP：非空的不相交的输入变量集合，IP={ip1,ip2,…,ipl}，ip1,ip2,…,ipl称为输入；

OP：非空的不相交的输出变量集合，OP={op1,op2,…,opm}，op1,op2,…,opm称为输出；

VS：表示输入输出变量的所有取值范围。假设r代表输入或者输出变量，那么其取值范围为VS(r)；

C：条件，条件是定义在输入或输出上的谓词。条件，如真、假或者逻辑表达式r⊙r'或r⊙a，其中r,r'表示输入、输出变量，a表示常数值，⊙∈{=,<,>,≠,>=,<=}表示关系操作符；

F：系统功能，在第3节中，所有的组件的功能都可以用表格表示，这些表格都描述成表格函数fi。

(2)输入映射表：该表格描述了所有的监督变量到所有的输入变量的映射关系fMI:MV→IP，准确地定义ρMI={(mvi,ipi)∈MV×IP},i=1,2,…,n，ρMI必须满足：

(a)对于任意的监督变量都存在唯一(∃!)的输入变量与其对应，∀mvi∃!ipi:ipi=fMI(mvi)；

(b)对于任意的输入变量只存在唯一的监督变量与其对应。

(3)输出映射表：该表格描述了所有的输出变量到所有的受控变量的映射关系fOC:OP→CV，准确地定义ρOC={((opi,…,opj),cvi)∈OP×CV};i,j=1,2,…,n，关系ρOC必须满足：

(a)对于任意的输出变量都存在唯一(∃!)的受控变量与其对应，∀opi∃!cvi:cvi=fMI(opi)；

(b)同一个受控变量可能对应多个输出变量。

(4)受控变量CV映射表：在输入变量取值不同情况下，相对应的输出变量取值情况。准确地定义ρi={(∪IPi,k,∪OPi,k)∈∪VS(IPi)×∪VS(OPi)},k=1,2,…,n。其中∪VS(IPi)作为与受控变量cv相关的所有输入组成的输入变量组取值情况的集合，∪VS(OPi)作为与cv相关的所有输出组成的输出变量组取值情况的集合，IPi,k表示单个输入变量IPi的取值。关系ρi必须满足以下属性：

为了明确具体的输出和输入之间的关系，用表格函数fi替换关系ρi，其中属性(a)、(b)、(c)保证了fi是一个函数，属性(c)、(d)保证了fi是双射：

(1)

(5)受控变量CV条件表：在输入变量取值不同的情况下，输出变量的取值情况。准确地定义ρi={((∪IPi,k,ci,j),∪OPi,k)∈(∪VS(IPi)×{Ci,1,Ci,2})×∪VS(OPi)},k=1,2,…,n;j=1,2。其中Ci是与受控变量相关的条件，ci,j表示保证条件Ci的真假情况。关系ρi必须满足以下属性：

(d)表格中，在所有输入变量取值确定的情况下，其对应的条件Ci的所有取值情况ci,j都包含在表格内，因为Ci只可以取布尔值，所以对于任意的i:ci,1=T∧ci,2=F；

用表格函数fi替换关系ρi，其中属性(a)、(c)、(d)、(e)保证fi是一个函数，属性(b)、(c)保证fi是双射：

OPi=fi(IPi,Ci)=

(2)

(6)受控变量CV事件表：在发生事件的情况下，输入变量取值如何影响与受控变量相关的输出变量的取值。由于事件表同条件表类似，只是将条件替换为事件，因此不再赘述。

5 案例分析

引擎指示和机组警告系统[15](engine-indicating and crew-alerting system,EICAS)是为飞机机组显示提供飞机引擎和其他系统运转情况的综合显示系统。

EICAS通常包含多种引擎参数显示仪表，如引擎转速、引擎温度、燃料流速和燃料量、油压等。被EICAS系统监督的其他飞机系统包括液压、气动、电力、除冰系统、飞行操作系统等。EICAS是驾驶舱显示系统的重要组成部分，以软件驱动的电子系统取代了原有的模拟仪表装置，其大部分显示区域用作导航和定位显示。机组警告系统(CAS)用来取代旧式系统中的信号指示面板，CAS不再单单以亮起指示灯来显示系统故障，而是在EICAS的指示区域显示一系列的信息来告知机组人员系统故障。

表1是驾驶舱显示系统中EICAS需求的一部分(由于篇幅原因，并没有将完整的需求文档内容进行展示，展示的是用表格符号表示后的需求)。它是关于引擎推力模式显示的条件表：在飞机飞行的不同阶段，飞机引擎的推力模式不同，EICAS系统通过接收从其他相关子系统传递来的参数，根据参数的取值情况确定并显示当前引擎推力的模式。其中，ipFADECEngineNormalTOSelected代表引擎正常全推力起飞模式是否被选中的参数，当参数取值为True时代表被选中(下同)；ipFADECEngineFlexTOSelected代表非全推力起飞模式是否被选中的参数；ipFADECEngine-NormalCLBSelected代表飞机是否处于全推力爬升模式的参数；ipFADECEngineCruiseSelected代表飞机引擎是否以巡航模式运作的参数；ipFADECEngineGASelected代表飞机引擎是否以复飞模式运作的参数；ipFADECEngineMCTSelected代表飞机引擎是否以最大连续推力模式运作的参数；ipFADECEngineTO1DerateSelected代表飞机是否以减推力模式1起飞的参数；ipFADECEngineTO2DerateSelected代表飞机是否以减推力模式2起飞的参数；条件Reduced thrusttakeoff代表减推力起飞模式是否被选择；输出项的模式文本显示opText_cvThrustMode取值：TO(正常全推力起飞)、FLEX-TO(非全推力起飞)、D-TO1(减推力模式1起飞)、D-TO2(减推力模式2起飞)、CLB(全推力爬升模式)、CON(连续最大推力飞行模式)、CRZ(巡航模式)、G/A(复飞模式)，opFont_cvThrustMode为输出模式文本的字体，opColor_cvThrustMode为输出模式文本的颜色。

表1 引擎推力模式cvThrustMode条件表

该条件表所表示的函数如下所示：

(opi,cvi)=fi(ip1,ip2,…,ip8,ci)=

(3)

其中，ip1,ip2,…,ip8表示输入变量；RTT表示条件Reduced Thrust Takeoff；op1,op2,op3表示输出变量。

6 结束语

需求的一致性和完备性对于系统的安全性起着至关重要的作用。找出需求中存在的错误，避免其对系统造成的不良影响，可以提高系统的安全性。传统的人工方法对需求进行检查和评审，不仅费时费力，而且容易忽略需求中存在的错误。利用Parnas提出的四变量模型作为指导框架确定驾驶舱显示系统的需求组成和关系，并用表格符号将需求进行表示，建立需求模型；运用形式化方法为需求模型定义精确的语义，并利用T-VEC工具进行检测。通过这一系列的工作，不仅可以准确地描述需求，而且找出了需求中存在的错误。

在将来的工作中，计划开发出一个支持T-VEC工具到符号化模型检测语言NuSMV的自动化工具，支持需求的安全性检测，找出需求中存在的安全错误，从而产生高质量的需求。这样的高质量需求，可以减少需求错误对系统的影响，提高系统的安全性。同时，自动化工具也减少了系统开发的成本。

[1] VERAS P C,VILLANI E,AMBROSIO A M,et al.Errors on space software requirements:a field study and application scenarios[C]//IEEE international symposium on software reliability engineering.[s.l.]:IEEE,2010.

[2] BOEHM B W. Software engineering economics[J].IEEE Transactions on Software Engineering,1984,10(1):4-21.

[3] ZHOU Y,ZHUANG D,ZHANG L,et al.Study on ergonomics evaluation method of the cockpit display system[C]//IEEE international conference on computer-aided industrial design & conceptual design.[s.l.]:IEEE,2010.

[4] GALLOWAY A,IWU F,MCDERMID J,et al.On the formal development of safety-critical software[M]//Verified software:theories,tools,experiments.Berlin:Springer-Verlag,2005:362-373.

[5] 陈 鑫，王 辉，牟 明.满足DO-178B要求的软件需求开发方法[J].计算机工程与设计,2012,33(7):2673-2677.

[6] 陈光颖，黄志球，陈 哲，等.面向DO-333的襟缝翼控制单元安全性分析[J].计算机科学，2016，43(5)：150-156.

[7] PARNAS D L,MADEY J.Functional documents for computer systems[J].Science of Computer Programming,1995,25(1):41-61.

[8] PARNAS D L.From requirements to architecture[C]//New

trends in software methodologies,tools and techniques.[s.l.]:IOS Press,2010:3-36.

[9] LEVESON N G,HEIMDAHL M P E,HILDRETH H,et al.Requirements specification for process-control systems[J].IEEE Transactions on Software Engineering,1994,20(9):684-707.

[10] MOIR I,SEABRIDGE A,JUKES M.Civil avionics systems[M].[s.l.]:John Wiley & Sons,2013.

[11] PARNAS D L.Tabular representation of relations[D].Canada:Telecommunications Research Institute of Ontario McMaster University,1997.

[12] HEITMEYER C L,JEFFORDS R D,LABAW B G.Automated consistency checking of requirements specifications[J].ACM Transactions on Software Engineering & Methodology,1996,5(3):231-261.

[13] 张 鹏，刘 磊，刘华虓，等.Tabular表达式的指称语义研究[J].软件学报,2014,25(6):1212-1224.

[14] HATTON L.What is a formal method (and what is an informal method)?[C]//Proceedings of the 12th annual conference on computer assurance 1997.[s.l.]:IEEE,1997:125-126.

[15] WELLS A T,RODRIGUES C C.Commercial aviation safety[M].[s.l.]:McGraw-Hill Professional,2011.