基于有限谓词追踪的民机系统需求一致性检查方法

王 鹏, 岳舒婷, 张 帆,*, 董 磊

(1. 中国民航大学民航航空器适航审定技术重点实验室, 天津 300300;2. 中国民航大学安全科学与工程学院, 天津 300300)

0 引 言

随着整机设计要求的不断提升与相关技术的发展,以平视显示(head-up display, HUD)系统为代表涉及多领域的高复杂性安全关键系统,呈现综合集成度高、研发周期长、管理复杂等特点[1]。为保证安全关键系统基于需求的正向研发水平,在设计早期确认功能需求的正确性具有重要意义。在国产安全关键系统研发工程中,系统功能需求确认主要通过人工评审来实现,效率低且难以排除需求文档中所有冲突与不一致,无法满足机载系统功能需求的严格确认要求[2-3]。同时,此类安全关键系统通常由多部门、多专业协同研发,而不同的开发人员、设计阶段使得整体项目的需求细节无法被全面、准确地理解[4],从而导致需求冲突与不一致的问题通常在系统设计后期的集成测试阶段涌现,而引入错误和发现错误之间的间隔越长,会造成系统研发迭代成本越高[5-6]。解决上述问题,亟需研究形式化的需求一致性检查方法,以严格的数学逻辑进行规约,在系统研发初期能够捕获需求冲突与需求不一致,从而迅速进行需求迭代,在降低系统设计返工或性能不足风险的同时减少系统研发成本。

采用形式化方法开展需求一致性检查,主要包含两部分内容:需求形式化规约与需求冲突检测。近年来,已有多位学者开展相关研究,研究成果涉及系统需求形式化规范、软件需求冲突检查等领域。

在早期的需求形式化规约研究中,文献[7]开发了简单需求语法模板(easy approach to requirement syntax, EARS),包括5类模板规范自然语言需求。随后多项研究基于架构模型建立需求规约,包括系统建模语言(system modeling language, SysML)[8-9]的建模语言提供了易于理解、使用的图形语法,但缺乏正式的语义。基于描述逻辑的Web本体语言[10]为需求语言提供精确的语义,文献[11-12]开发了多种本体构建方法以及工程设计领域需求的本体,但其表达性具有一定局限。文献[13]基于一阶逻辑(first-order logic, FOL)谓词的形式化规约则通过增加谓词、量词等进一步分析语句成分,成为更具表达力的基于逻辑的语言。文献[14]提出了直观表示FOL的显式方法,利用此方法构造了智能计算机辅助诊断/计算机辅助制造系统逻辑架构。由于FOL表达能力广泛,对特定复杂领域知识的描述需要对其进行一定的约束或扩展,使其适用于特定的形式化规约。文献[15]提出了基于派生特征约束FOL的特定领域语言形式化规约方法。文献[16]结合Petri网使用FOL对智能制造系统进行形式化建模,并推导出用于表示工艺方案的有限一阶谓词。

基于上述需求形式化规约的研究,需求冲突检测技术相应发展。基于EARS的EARS-CTRL (control)工具[17]可进行需求冲突检查,但检查效率较低且只针对简单类型的冲突。SysML、架构描述语言[18-19]多用于需求冲突检测,但缺乏形式语义。文献[20]提出了将逻辑嵌入SysML并将验证问题转化为逻辑问题的方法。文献[21]使用FOL构建需求模型,并进行跟踪关系的语义一致性检验,但其范围仅限于确认通用需求关系一致性,并未针对特定对象检查内容一致性,因此,后续研究更多针对需求内容进行推理规则的处理。文献[22]提出了一种基于独立FOL规则的方法,检测领域工程过程中的不一致特征,以提高软件产品的质量。文献[23-24]基于FOL的规范表示和一致性推理进行自动化合规性检查,但其推理规则较为复杂。文献[25]利用扩展谓词逻辑进行形式化规约并推导出用于验证的语义、语法和推理规则的定理。文献[26]利用基于有限谓词规则的软件特征模型分析其模型中的不一致性,但并未针对软件需求进行一致性分析。

对以上研究工作进行总结,上述方法存在以下两点问题:① 在需求形式化规约方面,未形成紧密贴合民机系统研发流程的系统级功能需求形式化规约方案,导致形式化方法和实际系统研发有一定偏差;② 在需求冲突方面,结合需求内容正确性、关系一致性的冲突检测技术在民机系统级需求领域尚无应用。

针对上述问题,提出基于有限谓词追踪的系统功能需求一致性检查方法体系,开展包含属性分配、变量分配的系统级功能需求形式化规约分析,在此基础上运用定理证明器ACL2(a computational logic for application common lisp)[27]实现需求自冲突、集冲突与需求关系一致性检查,基于可解释的检查反例进行需求迭代。最后通过实例分析,验证该方法的合理性与适用性。

1 基于有限谓词追踪的需求一致性检查结构框架

1.1 基于有限谓词追踪的需求一致性检查方法概述

文献[28]中需求确认为确定产品需求的正确性与完整性。一致性为已确定的相对于标准、技术规范或图纸的(产品)正确性,属于正确性检查的重要组成部分。功能需求指在具体条件下为了获得系统预期性能所需的需求,是系统功能架构研制的基础[29],包括系统级功能自顶向下的功能需求分配,并针对系统级、子系统级进行确认,以此支持系统功能需求的更新与迭代,过程如图1所示。

图1 基于4754A的需求分配及其确认流程图Fig.1 Requirement allocation and verification flow based on 4754A

系统自顶向下的功能需求分配基于系统实现,其系统过程与子系统过程之间的信息流形成系统功能需求,以此向下分配至:① 子系统设计阶段,形成内部功能需求;② 子系统综合阶段,形成交互功能需求。系统需求的规范化描述为需求规约,针对目前未形成紧密贴合民机系统研发流程的系统级功能需求形式化规约方案的问题,结合上述分配过程提出基于变量分配、属性分配的形式化需求及其分配规约,共同输入至系统级功能需求文档。

系统级功能需求一致性检查过程基于4754A中建议的正确性检查指南,从3个检查纬度评估需求的正确性,包括:① 需求包含事实的错误吗?——需求自冲突检查;② 需求与其他需求冲突吗?——需求集冲突检查;③ 需求追踪具有一致性吗?——需求关系一致性检查。由于目前在需求冲突方面,结合需求内容正确性、关系一致性的冲突检测技术在民机系统级需求领域尚无应用,提出系统单条需求的自冲突、多条需求的集冲突以及需求关系一致性的检查方法,建立基于有限谓词追踪的系统功能需求一致性检查体系,总体框架如图2所示。

图2 基于有限谓词追踪的需求一致性检查方法Fig.2 Requirement consistency checking method based on finite predicate tracing

(1) 需求形式化规约

传统的需求文档为基于工程经验、利益攸关者意愿、运行限制、规章约束以及设计实现等编写的自然语言文本,易于表达但缺乏精准,因此结合图1系统研发流程将功能需求分为内部功能需求与交互功能需求。将上述两类功能需求进一步细分,提出功能需求形式化分配方法:① 完成顶层期望功能的需求——完全/部分属性分配,例如,HUD系统具备姿态信息显示功能;② 完成设计实现所需功能的需求——监控/受控变量分配,例如,如果机体俯仰角大于35°,则HUD系统进入异常姿态模式。采用形式化规约描述需求以进行自动化定理证明或推理,从而检查需求冲突或不一致。

(2) 需求一致性检查

① 单条需求检查:单条需求冲突常为数值、范围、语义等类型冲突。因此,基于形式化需求提取可变类型及其变量,采用自冲突属性进行单条需求内容确认。② 多条需求内容检查:多条需求冲突常存在于拥有相同可变类型及变量的多个需求之间。因此,基于形式化需求提取涉及同一变量的所有需求,采用集冲突属性进行多条需求内容确认。③ 多条需求关系一致性检查:系统需求间的不一致关系常存在于系统向下分配需求时多个分配关系的矛盾。因此,基于形式化需求分配链提取需求关系并映射至属性关系,采用一致性推理公理进行需求关系一致性检查。

1.2 基本概念定义

需求、属性和变量是系统需求规约的3个基本概念:需求是功能规范的可识别要素;属性是描述系统拥有的静态特性;变量是系统输入/输出的事件和数据。后续使用FOL将需求及需求关系形式化为精准语义描述,其遵循以下基本定义。

定义 1需求R。需求R定义为一个元组〈P,S〉,其中P为包含两个参数的属性,P可以用由谓词组成的合取范式(conjunctive normal form, CNF)表示如下:

定义 2属性P。属性P是由条件与结论组成的陈述句。其中,条件为系统展现出规定特性的假设;结论为陈述系统在假设成立时真实存在的特征。

定义 3监控变量C。属性P的条件中使用的变量是系统输入的事件和数据。

定义 4受控变量H。属性P满足C条件下的结论中设置的变量,是系统输出的事件和数据。

例如,R1:如果动机转速百分比小于30%(条件),那么系统应将通道Px设置为开启(结论)。

此条功能需求语句中,条件中的“转速百分比”为监控变量,结论中的“通道Px”为受控变量。

将属性P定义为一个元组〈C,H〉,即∀h∈H:C(h)。根据FOL的语义模型理论,将C形式化表达为

需求自冲突、集冲突、关系不一致是系统需求检查的基本概念。

定义 5需求冲突。如果需求R1的实现排除了需求R2的实现,那么需求R1和需求R2就会冲突,反之亦然。

定义 6需求自冲突。如果监控变量的某个输入值不能满足需求,即使存在受控变量满足,该需求为自冲突。

定义 7需求集冲突。任一受控变量的输入值,都有一个或几个监控变量的输入值不能满足需求集,则该需求为集冲突。

定义 8需求关系不一致。指需求之间某些关系的共存导致了已定义语义上下文中的矛盾。

定义 9ACL2逻辑。ACL2逻辑中用宏defun来定义函数,用添加定理defthm的方法来证明系统的属性。函数定义包括函数名、参数名以及函数体,示例如下:

① (defun (xy)

② (if (conspx)

③ (cons (carx) (app (cdrx)y))y))

④ (defthmtest-app (equal (app (appab)c)

(appa(appbc)))

第①行定义了“连接x和y”的函数;第②行通过谓词函数检查参数类型;第③行以可终止的递归形式定义,表示如果x不为空,则复制x的第一个节点并重复到下一个节点,直到x为空则回到y;第④行为验证app函数的ACL定理,证明过程中,ACL2包含大量的决策制定程序和强大的简化机制。

基于FOL精准语义形式化系统功能需求,进行需求一致性检查需要用到相应的定理证明推理规范[30],因此做出如下假设。

假设 1使用规范语言L

① 多类别一阶逻辑

② 可扩展

③ 可执行

假设 2属性P定义形式为

① 无嵌套量词

② 隐式普遍量化

假设 3一个交互定理证明器(interactive theorem prover assistant, ITP),可以对L中的规范进行推理。

① 分解:将一个目标(一个用L写的公式)作为输入,并返回一个相等有效的子目标列表。

② 简化:将使用语言L编写的公式和组公式作为输入,并返回一个与语言L编写公式等价的简化公式(假设组公式为真)。

2 系统需求形式化描述规约

2.1 系统内部功能需求形式化方法

基于需求捕获环境必须允许需求工程师在高层级需求描述中不给出低层级需求的全部细节[4],系统需求形式化描述规约通过谓词追踪完成分配。分配允许识别未完全描述的某些组件具体行为,形式上可以理解为未解释的函数。因此,可以将顶层需求直接向下分配,不进行分配的需求也可直接形式化属性及变量,进行需求一致性检查。

系统内部功能需求向下形式化分配包含属性分配与变量分配两种方式,分配过程如图3所示。

图3 内部功能需求的形式化Fig.3 Formalization of internal functional requirements

2.1.1 属性分配

(1) 属性完全分配

设R1=〈P1,S1〉,R2=〈P2,S2〉是需求。P1和P2为由CNF组成的需求属性,P2的CNF为

∃s∈S2:s∉S1

结论:如果P1对于给定的系统s成立,那么P2对于s也成立(∀s∈S1:s∈S2)。在∃s∈S2:s∉S1和∀s∈S1:s∈S2的基础之上,即可得S1⊂S2。Refines关系具有非自反性、非对称性和传递性。

例:需求R1向下完全分配了需求R2

P1=FMA_pattern_1(x)

P2=CMD_msg(x)

x∈{CMD,NO_CMD,SINGE_CH,和NO_SINGE_CH}

设:FMA_pattern_1Mdef{CMD,NO_CMD,SINGE_CH,NO_SINGE_CH}

则CMD_msgMdef{CMD,NO_CMD}

属性完全分配后形式化为

R2refinesR1:[CMD_msg(x)→FMA_pattern_1(x),S2⊂S1]

即HUD系统显示飞行模式通告(FMA_pattern_1)功能向下完全分配至自动监视仪(CMD_msg)启动功能。

(2) 属性部分分配

设R1=〈P1,S1〉,R2=〈P2,S2〉是需求,P1和P2为公式,P2的CNF为

例:需求R1向下部分分配了需求R2

P1=interface(x,y)

P2=datainterface(x,y,z)

式中:x是功能需求的变量;y是接口需求的变量;z是数据接口的变量;P2细化了P1接口部分,并增加了数据接口的具体内容。因此,属性部分分配后形式化为表示为

R2partially_refinesR1:[datainterface(x,y,z)→

interface(x,y),∃s∈S1:s∉S2,∃s∈S2:s∉S1]

即HUD系统符号显示功能中的功能接口需求部分分配至数据接口,但分配后的数据接口功能并不完全服务于符号显示功能。

2.1.2 变量分配

(1) 受控变量分配

设P1=〈C1,H1〉P2=〈C2,H2〉是需求。

该定义可得出结论H1⊂H2。集合H1和H2之间的子集关系将control_refines关系定义为非自反、非对称和传递的,也可以称作R2为R1的先决条件,且R1与R2不允许相等。

例:需求R1受控变量向下分配了需求R2

H1=FMA_pattern∈{CMD,NO_CMD,SINGE_CH,NO_SINGE_CH}

H2=SINGE_CH_msg

受控变量向下分配后形式化表示为

R2control_refinesR1:[C(x),H2⊂H1]

(2) 监控变量分配

设R1=〈C1,H1〉,R2=〈C2,H2〉,…,Rk=〈Ck,Hk〉是需求,其中k≥2,C2,C3,…,Ck为公式,其CNF为

式中:C′表示为C2,C3,…,Ck未捕获的需求。此定义对于分解的完整性不做假设。从定义可以得出结论,如果C1成立,那么C2…Ck也保持,如果C2…Ck成立则C1不一定成立。因此,H1⊂H2,H1⊂H3,…,H1⊂Hk。其中,monitor_refines关系是非自反的,非对称的,传递的。

例:需求R1监控变量向下分配了需求R2

C1=provide (FMA_FD_ONf)

监控变量向下分配后形式化为表示为

ON_flash),H2⊂H1]

即HUD系统自动驾驶仪未接通符号闪烁显示的条件分配为3个监控变量。

2.2 系统交互功能需求形式化方法

与前述内部需求类似,交互功能需求的形式化需要考虑多个系统的交互关系下属性分配与多系统子集关系,形式化过程如图4所示。

图4 交互功能需求的形式化Fig.4 Formalization of interactive functional requirements

(1) 属性完全分配

交互需求属性完全分配后形式化表示为

(2) 属性部分分配

∃s∈S1-S2:s∉S1-S2,∃s∈(S1-S2∩S1-S2)

P2=datainterface(x,y,z)

R2partially_refinesR1:[datainterface(x,y,z)→

(3) 变量分配

交互功能需求的变量分配与内部功能需求相同,即:

3 基于有限谓词追踪的一致性检查

3.1 系统功能需求自冲突检查

本文通过提取关键冲突属性并采用ACL2定理证明器对需求一致性进行验证。基于第2节系统功能需求形式化描述规约,由需求自冲突的定义可得自冲突的检查形式[31]为

(1)

式中:c1,c2,…,cn为需求的n个监控变量(monitor_variable);T1,T2,…,Tn为监控变量的n个类型(monitor_type);h1,h2,…,hk为需求的k个受控变量(control_variable);Z1,Z2,…,Zk为受控变量的k个类型(control_type);fr为需求主体。

式(1)表明,对于监控变量的任何可行赋值(监控变量的类型对应其可行值),受控变量至少有一个可行赋值,使得需求R成立。基于式(1)的检查形式构建显示自冲突的确认:

(2)

式(2)则表明需求自冲突的类型,如果提取变量及其可行值与自冲突类型相同,则需求R显示为自冲突,即存在监控变量的可行赋值不满足需求R。因此,自冲突检查过程如图5所示。

图5 需求自冲突检查Fig.5 Requirements self-conflict checking

待检查的单条形式化需求Ri作为输入,提取属性以及变量进行冲突识别,判断其是否属于需求自冲突类型,若属于自冲突类型则检查结果为需求自冲突,并输出反例;否则进入下一条需求的检查。其中,自冲突类型:① 存在监控变量及其可行值,但不存在相应受控变量;② 存在监控变量及其可行值、相应受控变量,但该受控变量不存在可行值;③ 存在监控变量但不存在该监控变量可行值。

例,R1:如果机体俯仰角超过35°,则HUD系统进入异常姿态模式;R2:姿态数据传感器可识别角度范围[-30,33]。此案例中的自冲突类型为第③种,即R1监控变量的赋值大于33时无可行赋值,R1发生自冲突。

自冲突属性系统功能需求检查为自冲突,ACL2实现策略如下:

DEFUN self-conflict

(AND (∀monitor_variable∈monitor_type)

(eqlfr(Monitor_variable, control_variable)T))

#监控变量存在可行赋值且输出受控变量与监控变量的关系

DEFTHM self-conflict-test

(OR (∀control_variable∈control_type)

(eqlfr(Monitor_variable, control_variable)T))

#受控变量存在可行赋值

3.2 系统功能需求集冲突检查

根据需求集冲突的定义,将式(1)与式(2)中的R替换为需求R的集合,作为集冲突的检查形式,集冲突的检查过程如图6所示。

由于多数存在集冲突的需求集往往共享一个受控变量,因此待检查的多条形式化需求Ri作为输入,需要提取相关属性及其相同受控变量进行冲突识别,判断其是否属于需求集冲突类型,若属于集冲突类型则检查结果为需求集冲突,并输出反例;否则进入下一条需求的检查。其中,集冲突类型:① 存在一个监控变量及其可行值对应多个监控变量及可行值;② 存在多个监控变量及其可行值同时成立时无相应受控变量及可行值。

例,R1:如果TO/GA状态数据指令开启,则自动油门模式通告显示为“GA”;R2:如果自动油门模式N1数据指令开启时,则自动油门模式通告显示为“N1”。此案例中的冲突类型为第②种,即如果TO/GA状态数据指令开启且自动油门模式N1数据指令开启两个条件同时成立时,受控变量——“自动油门模式通告”不存在可行赋值,即两个需求发生集冲突。

集冲突属性系统功能需求检查为集冲突,ACL2实现策略如下:

DEFUN set-conflict

(COND (c1∈T1(AND (eqlfr(c1,h1)T)h1∈Z1))

(c2∈T2(AND (eqlfr(c2,h2)T)h2∈Z2))

⋮

(cn∈Tn(AND (eqlfr(cn,hk)T)hk∈Zk)))

#如果c1/c2/…/cn成立则对应输出h1/h2/…/hk

DEFTHM set-conflict-test

(IMPLIES (AND (eqlfr(c,h)T)(∃cn∈Tn))

(AND (eqlfr(c1,h)T)(eqlfr(c2,h)T)))

#监控变量找不到可行值或多个同时满足输出一个受控变量。

3.3 系统功能需求关系一致性检查

基于第2节需求分配关系定义,需求分配f(R1,R2)共存在4种关系:① 属性完全分配WR;② 属性部分分配PR;③ 监控变量分配MR;④ 受控变量分配CR。需求关系的一致性通过将需求关系进一步细分为属性关系g(P1,P2)进行检查,根据文献[21]给定的需求属性,存在的5种关系分别为:① 整体-整体——all-in-whole(P1,P2);② 整体-局部——all-in-part(P1,P2);③ 局部蕴含——some-implies-in(P1,P2);④ 整体蕴含——all-implies-in(P1,P2);⑤ 全等——all-equals-in(P1,P2),基于以上5种关系分别定义需求的属性分配与变量分配关系:

具体映射如下:

对于上述公式之间的关系,具有以下一致性公理,如果推导出的新关系包含以下矛盾关系,则被判定为不一致。具体检查过程如图7所示。

图7 需求一致性检查Fig.7 Requirement consistency checking

(1) 全等与蕴含矛盾

例:all-equals-in∩all-implies-in=Ø

(2) 整体与局部矛盾

例:all-in-whole∩all-in-part=Ø

需求R进行属性/变量分配过程得到分配后的需求R′,即将R与R′之间的关系fn(R1,R2)作为输入,存在多种关系的两条需求,使其需求关系映射至属性关系gn(P1,P2),判断细化后的属性关系是否存在矛盾关系,如果存在则判定为不一致关系;否则进入下一对需求关系检查。

例:①R1可以通过属性完全分配得到R2;②R1可以通过受控变量分配得到R2。此案例中的不一致类型为第①种,即两个需求的属性关系all-equals-in, some-implies-in矛盾即R1与R2存在不一致。

关系冲突属性系统功能需求关系检查为不一致,ACL2实现策略如下:

DEFUN consistency

(COND (ralation1(P1,P2)(OR{00}{11}{01}{10}))

(ralation2(P1,P2)(OR{00}{11}{01}{10}))

⋮

(ralation5(P1,P2)(OR{00}{11}{01}{10})))

#如果ralation1/…/ralation5成立则输出对应的{00}/{11}/{01}/{10}

DEFTHM consistency-test

(IF (output(consistency)∈(OR{0011}{1100}{0110}{1001}))′(non-consistency)′(consistency))

#如果给定的两需求关系代码组合属于不一致组合,则该两需求关系之间存在不一致。

4 实例分析

4.1 HUD系统飞行信息符号生成与显示功能概述

HUD系统能够将机上传感器信息处理计算后,利用光学反射和成像设备将必要飞行状态信息,以及提示、告警、故障等方式投射至飞行员前方的成像板上,实现飞行关键信息符号生成与显示[32]。HUD系统的基本架构由HUD计算机(HUD computer, HUDC)、HUD投影装置(HUD projector unit, HPU)、HUD组合仪(HUD combiner unit, HCU)组成。以典型功能“飞行信息符号生成与显示”为例,系统功能架构如图8所示。 HUDC接收并解析机载传感器数据,将其转换为内部应用程序编程接口;符号生成软件根据传感器数据计算符号逻辑,生成绘制指令。HUDC根据绘制指令生成飞行信息符号画面发送给HPU,HPU对显示画面进行畸变校正,并经过光学结构进行投影。HCU接收投射的显示画面并显示规定的符号信息。

图8 HUD系统飞行信息符号生成与显示功能架构Fig.8 HUD system flight information symbol generation and display function architecture

4.2 基于形式化规约的系统功能需求描述

4.2.1 功能需求分类

飞行信息符号生成与显示功能需求(部分)分类如表1所示。

表1 “飞行信息符号生成与显示”功能需求(部分)Table 1 Functional requirements of “flight information symbol generation and display” (partial)

4.2.2 功能需求形式化描述

基于第2节形式化需求分配,HUD系统内部、交互功能需求的分配关系如图9所示,其中WR为属性完全分配,PR为属性部分分配,CR为受控变量分配,MR为监控变量分配。

图9 功能需求分配关系图Fig.9 Functional requirement allocation relationship diagram

(1) 内部功能需求形式化

分配①:R02partially_refinesR01:[FMA(x,y)→Display(x),∃s∈S01:s∉S02,∃s∈S02:s∉S01]

∥R02部分细化了R01的飞行模式通告具体内容。

分配②:R03refinesR02:[FDM(y)→ FMA(x),S03⊂S02]

∥R03在R02原有内容的基础上细化了飞行指引仪模式通告信息具体内容。

分配③:R04control_refinesR03:[AFM(x),H04⊂H03]

∥R04细化了R03结论中自动飞行模式通告改变时系统模式的改变。

分配④:R07partially_refinesR04:[MODE_Change _body→AFM-MODE(x),∃s∈S04:s∉S07,∃s∈S07:s∉S04]

∥R07部分细化了R04两个模式之间的关系。

分配⑤:R05monitor_refinesR04:[C04=C05∧C′,H05⊂H04]

∥R05细化了R04条件中自动飞行模式通告符号信息可显示的3个模式通告。

分配⑥:R06control_refinesR04:[AFM(x),H06⊂H04]

∥R06细化了R04结论中两个模式的类型。

(2) 交互功能需求形式化

∥R09细化了R08中符号定义的具体管理内容

R10control_refinesR09:[Defined(x),H10⊂H09]

∥R10细化了R09结论中符号定义的条件。

∥R14、R15、R16细化了R13条件中的受控变量及其可行值,以及相应的结论。

4.3 需求一致性检查

(1) 需求自冲突检查

自冲突适用于单条需求的类型检查、赋值检查以及范围检查,以R06和R07作为典型案例,使用ACL2定理证明器开展系统自冲突检查。

基于自冲突属性进行HUD功能需求自冲突检查,ACL2实现如下:

DEFUN self-conflict1 (xy)

(declare (type integerxy))

(if (AND (INTEGERPx)

(<=1x)(<=x5)

(INTEGERPy)

(<=1y)(<=y5))

(+x1) 0)

DEFTHM self-conflict-test

(and (INTEGERP (self-conflict1xy))

(<=0 (self-conflict1xy))

(<=(self-conflict1xy) 5))

上述代码首先定义monitor_variable存在的可行赋值,并构建control_variable与monitor_variable在属性中的映射关系,通过ACL2定理证明器,验证该control_variable不存在满足需求的可行赋值,检查结果为自冲突。代码中第二行要对需求变量的可行值类型进行约束,且需要给出监控变量及其赋值的可行范围,证明过程如下:

Cgen/test

图10 自冲突检查结果及反例Fig.10 Self-conflict examination results and counterexamples

因此,检查结果表明R07存在自冲突,即如果自动飞行系统模式通告FMA_FD闪烁显示,那么DesiredMODE应该根据CurrentMODE设置为CurrentMODE+1的值,此时CurrentMODE为监控变量,DesiredMODE为受控变量。但是CurrentMODE和DesiredMODE是相同的类型,是[1,5]范围内的整数,如果CurrentMODE=5,那么就没有办法为受控变量DesiredMODE赋值以满足需求,所以存在需求自冲突。

(2) 需求集冲突检查

集冲突适用于具有相同受控变量的需求集,以R15和R16作为典型案例,使用ACL2定理证明器开展HUD系统功能需求集冲突检查。

基于集冲突属性进行HUD功能需求集冲突检查,ACL2实现如下:

DEFUN set-conflict1(coma comb)

(declare (type integer coma comb))

(if (>=(-coma comb) 5) 1 0)

DEFUN set-conflict2(coma comb)

(declare (type integer coma comb))

(if (<=(-coma comb) 5) 0 1)

DEFTHM set-conflict-test

(=((-(set-conflict coma comb) (set-conflict coma comb))0)

上述代码表示根据需求属性定义当monitor_variable存在可行值T1时,可使对应的control_variable成立且输出可行值Z1,或将(c1,h1)的映射关系传递至(cn,hk)成立,及其对应输出可行赋值(Tn,Zk);验证monitor_variable找不到可行值,或多个monitor_variable同时满足输出一个control_variable,则检查结果为集冲突。代码中第7行用到的函数必须存在多个需求使用同一受控变量及其可行值的条件限制,证明过程如下:

#将字符串与正则表达式进行匹配,正则表达式在宏扩展时进行分析。

#获取和设置Cgen中各种参数的默认值

#存储简化的定义主体

#简化规则

Cgen/test

若存在反例,则ACL2输出如图11(a)所示,反例给出需求显示自冲突时监控变量赋值为5时受控变量存在两相异可行值,即集冲突类型①如图11(b)所示。

图11 集冲突检查结果及反例Fig.11 Set-conflict examination results and counterexamples

因此,检查结果表示R15和R16存在集冲突,即|id_ComA-id_ComB|需要严格大于5还是大于或等于5存在冲突。ACL2给出的反例捕获了两个数据的差值正好为5的系统状态,在这种情况下,两个需求都适用,并将FMA_pattern置为不同的值,所以存在需求集冲突。

(3) 需求关系一致性检查

一致性冲突适用于分配过程的关系一致性,以R09和R10作为典型案例,使用ACL2定理证明器开展HUD系统功能需求关系一致性检查。

基于关系冲突属性进行HUD功能需求关系一致性检查,ACL2实现如下:

DEFUN refines (all-in-whole some-implies-in)

(declare (type integer all-in-whole some-implies-in))

(cond((=all-in-whole some-implies-in)(print′(0 0)))

((

(endp))

DEFUN control-refines (all-in-part all-equals-in)

(declare (type integer all-in-part all-equals-in))

(cond((

((=all-in-part (fx all-in-part)) (print′(1 0)))

(endp))

DEFUN consistency-check (xy)

(declare (type integerxy))

(cond((or (=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 0 1 0))

(=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 1 1 1)))x)

((or (=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 0 1 1))

(=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 1 1 0)))y)(x))

DEFTHM consistency-test

(equal (consistency-checkxy)

(consistency-checkyy))

上述代码表示根据属性之间的关系对应输出集合{00}/{11}/{01}/{10},再将需求之间的关系以属性关系的对应数组按顺序相连,形成相应的需求关系代码组合属于规定的不一致组合{0011}{1100}{0110}{1001},则检查结果为需求关系不一致。代码中DEFTHM定义函数必须为可终止函数,ACL2证明过程如下:

Cgen/test

若存在不一致则ACL2输出如图12(a)所示,反例给出需求关系显示不一致时同时存在的属性关系交集为空,即不一致类型①和②如图12(b)所示。

图12 一致性检查结果及反例Fig.12 Consistency check results and counterexamples

因此,检查结果为R10refinesR09与R10control _refinesR09关系存在不一致,ACL2给出的反例表示不存在有相应关系的两条需求,即WR(R10,R09)=all-in-whole(P10,P09)∧some-implies-in(P10,P09),CR(R10,R09)=all-in-part(P10,P09)∧ all-equals-in(P10,P09),整体(all-in-whole)与局部关系(all-in-part)相矛盾、全等关系(all-equals-in)与蕴含关系(some-implies-in)相矛盾。因此WR(R10,R09)和CR(R10,R09)存在不一致。

检查结果汇总如表2所示。基于第4.2节中的形式化需求,开展HUD系统16条功能需求自冲突检查、16条功能需求集冲突检查、14种分配关系进行一致性检查,共完成46次一致性检查共遍历13 026次,生成15条反例对结果进行评审,确认结果正确,从而证明了方法的有效性。

表2 “飞行信息符号显示与生成功能”需求一致性检查结果Table 2 Results of “flight information symbol display and generation function” requirement consistency check

本文提出的基于有限谓词追踪的HUD系统功能需求一致性检查方法与EARS-CTRL、根系统标记语言(root system markup language, RSML)、规范工具和需求方法(specification toolsand requirements methodology, SpecTRM),统一建模语言(unified modeling language, UML)、 SysML、美国国防部架构框架(Department of Defense Architecture Framework, DoDAF),TRIC/FOL的对比结果如表3所示。通过对比,本文方法主要具有以下3个方面的优势:① 综合需求内容正确性与需求关系一致性的体系化检查方案;② 生成可解释冲突反例,实现部分隐性需求显性化,有助于安全关键系统研发需求的更新迭代;③ 基于4754A系统功能需求形式化分配完成逻辑事实推理,将需求冲突检查转化为基于一阶逻辑的精准语义推理,优化以往形式化方法语义推理不足。

表3 方法对比Table 3 Methods comparison

5 结 论

本文提出基于有限谓词追踪的民机系统需求一致性检查方法,能够在系统研发初期捕获功能需求冲突与不一致,并综合考虑了需求内容正确性与需求关系一致性的体系化检查方案。① 针对系统功能需求包含的内部功能需求、交互功能需求构建基于谓词追踪的形式化规约,形成属性追踪、变量追踪的系统级功能需求分配机制;② 基于需求形式化规约,在有限谓词追踪路径内定义需求冲突属性,开展需求自冲突、集冲突的单、多条需求内容的一致性检查;③ 基于需求追踪关系制定关系冲突属性,通过ACL2完成需求关系一致性检查。同时,检查结果为冲突时即可生成可解释反例实现隐性需求显性化,助于需求迭代,以HUD系统飞行信息符号生成与显示功能为例验证该方法的正确性与有效性。

基于有限谓词追踪的民机系统需求一致性检查方法是一阶逻辑形式化与定理证明推理的综合,应用谓词追踪形式化需求分配过程,通过ACL2实现检查策略从而识别冲突与不一致。在需求形式化规约方面,形成紧密贴合民机系统研发流程的系统级功能需求形式化规约方案,优化形式化方法使用效果;在需求冲突方面,实现结合需求内容正确性、关系一致性的冲突检测技术在民机系统级需求领域的应用,降低系统研发成本。