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

doi:10.12305/j.issn.1001-506X.2024.01.24

摘要/Abstract

摘要：

针对民机安全关键系统在正向研发过程中, 系统级需求的正确性难以在设计早期全部完成确认的问题, 提出一种基于有限谓词追踪的功能需求一致性检查体系。首先, 引入一阶逻辑中的谓词追踪, 建立系统内部功能需求与交互功能需求形式化规约方法。其次, 针对单条、多条需求内容正确性以及需求关系一致性, 构建需求一致性检查形式化规约, 开展需求自冲突、集冲突与需求关系一致性检验, 并生成可解释的检查反例进行需求迭代。最后, 以机载平视显示(head-up display, HUD)系统飞行信息符号生成与显示功能为例, 验证该方法的正确性与有效性。研究结果表明, 基于有限谓词追踪的功能需求一致性检查方法能够提高需求一致性检查效率、降低研发成本, 为民机系统级需求确认提供支持。

关键词: 需求一致性, 定理证明, 功能需求正确性, 一阶逻辑, 需求冲突

Abstract:

To address the problem that it is difficult to confirm the correctness of system-level requirements in the forward development process of safety-critical systems for civil aircraft, a functional requirement consistency checking system based on limited predicate tracking is proposed. Firstly, the predicate tracking in first-order logic is introduced to establish a formal statute method for internal and interactive functional requirements of sytem. Secondly, a formal statute for requirement consistency checking for single and multiple requirement content correctness and requirement relationship consistency are constructed. The requirement self-conflict, set conflict and requirement relationship consistency checking are carried out. And the interpretable check counterexamples for requirement iteration is generated. Finally, the correctness and effectiveness of the method are verified by taking the head-up display (HUD) system flight information symbol generation and display function as an example. The conclusion shows that the finite predicate tracking-based functional requirement consistency checking method can improve the efficiency of requirement consistency checking, reduce the development cost, and provide support for system-level requirement validation of civil aircraft.

Key words: requirements consistency, theorem proving, correctness of functional requirements, first-order logic (FOL), requirements conflict

中图分类号:

王鹏, 岳舒婷, 张帆, 董磊. 基于有限谓词追踪的民机系统需求一致性检查方法[J]. 系统工程与电子技术, 2023, 46(1): 205-218.

Peng WANG, Shuting YUE, Fan ZHANG, Lei DONG. Requirement consistency checking method for civil aircraft systems based on finite predicate tracing[J]. Systems Engineering and Electronics, 2023, 46(1): 205-218.

图/表 15

图1

图2

图3

图4

图5

图6

图7

图8

表1

“飞行信息符号生成与显示”功能需求(部分)"

需求类型	需求编号	需求描述
内部功能需求	01	HUD系统在主画面模式下, 显示姿态、航向、高度、空速、航迹与飞行模式通告等符号信息
	02	HUD系统通告飞行模式信息时, 显示包括自动飞行模式通告、自动油门模式通告、飞行指引仪模式通告信息
	03	HUD系统通告飞行模式信息时, 显示包括自动飞行模式通告、自动油门模式通告、飞行指引仪水平模式通告、飞行指引仪垂直模式通告信息
	04	HUD系统显示的自动飞行模式通告符号信息发生改变时, 系统的即时模式与预期模式相应作出改变
	05	HUD系统显示的自动飞行模式通告符号信息可显示3个模式通告: ① 飞行指示仪开启且任一自动驾驶仪未激活; ② 任一自动监视仪接通; ③ 航向道截获且单通道接通(SINGLE CH)
	06	即时模式与预期模式都属于[1, 5]范围内的整数
	07	如果自动飞行系统模式通告FMA_FD符号闪烁显示, 那么DesiredMODE=CurrentMODE+1
	⋮	⋮
交互功能需求	01	HUDC通过处理传感器数据并生成图形及符号数据, 通过HPU的数据传输与投影, 使HCU组合仪显示飞行信息符号给飞行员
	02	HUDC应只允许设备方管理定义显示在HCU上的飞行信息符号
	03	HUDC应提供可自定义的HCU符号可见性策略
	04	如果HUDC接收的飞行模式数据发生改变, HUD系统应显示特定的飞行模式通告
	05	如果HUDC接收的飞行模式数据发生改变时, HUD系统应显示特定的自动飞行模式通告、自动油门模式通告、飞行指引仪模式通告信息
	06	如果HUDC数据接口传输特定的数据时, HUD系统应显示相应的自动飞行模式通告符号
	07	如果id_FDA=1(FD指示接通)且\|id_ComA-id_ComB\|=nill(Com指示不接通), 自动飞行系统模式通告显示为FMA_FD
	08	如果id_ComA与id_ComB的差值大于等于5时(Com指令位在右侧), 自动飞行系统模式通告显示“CMD”
	09	如果id_ComA与id_ComB的差值小于等于5时(Com指令位在左侧), 自动飞行系统模式通告显示“SINGE CH”
	⋮	⋮

表1

图9

图10

图11

图12

表2

表3

参考文献 32

1	XU W J , MA D F . A framework for model and verification of safety-critical operating system based on ARINC653[J]. Electronics, 2021, 10 (16): 1934. doi: 10.3390/electronics10161934
2	GUO X , LIU Y , ZHAO W , et al. Supporting resilient conceptual design using functional decomposition and conflict resolution[J]. Advanced Engineering Informatics, 2021, 48, 101262. doi: 10.1016/j.aei.2021.101262
3	廖万斌, 曹云峰, 王新尧. 面向复杂系统需求分析的DSL构建[J]. 系统工程与电子技术, 2022, 44 (11): 3443- 3454.
	LIAO W B , CAO Y F , WANG X Y , et al. DSL building for requirement analysis of complex system[J]. Systems Engineering and Electronics, 2022, 44 (11): 3443- 3454.
4	MOITRA A , SIU K , CRAPO A W , et al. Automating requirements analysis and test case generation[J]. Requirements Engineering, 2019, 24 (3): 341- 364. doi: 10.1007/s00766-019-00316-x
5	WANG Y , LUO L K , LIU H . Bridging the semantic gap between customer needs and design specifications using user-generated content[J]. IEEE Trans.on Engineering Management, 2020, 64 (4): 1622- 1634.
6	LI M, MENG B L, YU H, et al. Requirements-based automated test generation for safety critical software[C]//Proc. of the IEEE/AIAA 38th Digital Avionics Systems Conference, 2019.
7	MAVIN A, WILKSINSON P, GREGORY S, et al. Listens learned (8 lessons learned applying EARS)[C]//Proc. of the IEEE 24th International Requirements Engineering Conference, 2016: 276-282.
8	FRIEDENTHAL S , MOORE A , STEINER R . A practical guide to SysML: the systems modeling language[M]. San Francisco: Morgan Kaufmann, 2014.
9	FU C , LIU J H , WANG S D . Building SysML model graph to support the system model reuse[J]. IEEE Access, 2021, 9, 132374- 132389. doi: 10.1109/ACCESS.2021.3115165
10	OWL Working Group. OWL 2 Web ontology language document overview: W3C recommendation 27 October 2009[EB/OL]. [2022-07-01]. https://www.w3.org/TR/owl2-overview/.
11	PENG G Z , WANG H W , ZHANG H M , et al. A hypernetwork-based approach to collaborative retrieval and reasoning of engineering design knowledge[J]. Advanced Engineering Informatics, 2019, 42, 100956. doi: 10.1016/j.aei.2019.100956
12	QIN F W, XU H R, ZHANG W C, et al. Voice of the customer oriented new product synthesis over knowledge graphs[C]//Proc. of the International Design Engineering Technical Confe-rences and Computers and Information in Engineering Confe-rence, 2018.
13	DAPOIGNY R, BARLATIER P. Specifying well-formed part-whole relations in COQ[C]//Proc. of the International Confe-rence on Conceptual Structures, 2014: 159-173.
14	TAIT W W . First-order logic without bound variables: compositional semantics[M]. Cham: Springer, 2014: 359- 384.
15	SEMERÁTH O , BARTA Á , HORVÁTH Á , et al. Formal validation of domain-specific languages with derived features and well-formedness constraints[J]. Software & Systems Mo-deling, 2017, 16 (2): 357- 392.
16	LU J , OU C Y , LIAO C , et al. Formal modelling of a sheet metal smart manufacturing system by using Petri nets and first-order predicate logic[J]. Journal of Intelligent Manufacturing, 2021, 32 (4): 1043- 1063. doi: 10.1007/s10845-020-01602-0
17	LÚCIO L, RAHMAN S, CHENG C H, et al. Just formal enough? automated analysis of EARS requirements[C]//Proc. of the In NASA Formal Methods Symposium, 2017: 427-434.
18	王庆龙, 王智学, 何红悦, 等. 基于模糊-云模型的C4ISR系统效能需求建模与分析方法[J]. 系统工程与电子技术, 2016, 38 (9): 2065- 2071.
	WANG Q L , WANG Z X , HE H Y , et al. Modeling and analysis method to C4ISR system for efficiency requirements based on fuzzy cloud model[J]. Systems Engineering and Electronics, 2016, 38 (9): 2065- 2071.
19	ATOUM I , BAKLIZI M , ALSMADI I , et al. Challenges of software requirements quality assurance and validation: a systematic literature review[J]. IEEE Access, 2021, 9, 137613- 137634. doi: 10.1109/ACCESS.2021.3117989
20	LIMA L , MIYAZAWA A , CAVALCANTI A , et al. An integrated semantics for reasoning about SysML design models using refinement[J]. Software & Systems Modeling, 2017, 16, 875- 902.
21	GOKNIL A , KURTEV I , VAN D B K , et al. Semantics of trace relations in requirements models for consistency checking and inferencing[J]. Software & Systems Modeling, 2011, 10 (1): 31- 54.
22	ELFAKI A O . A rule-based approach to detect and prevent inconsistency in the domain-engineering process[J]. Expert Systems, 2016, 33 (1): 3- 13. doi: 10.1111/exsy.12116
23	ZHANG J S , EL-GOHARY N M . Semantic-based logic representation and reasoning for automated regulatory compliance checking[J]. Journal of Computing in Civil Engineering, 2017, 31 (1): 04016037. doi: 10.1061/(ASCE)CP.1943-5487.0000583
24	XUE X R , ZHANG J S . Regulatory information transformation ruleset expansion to support automated building code compliance checking[J]. Automation in Construction, 2022, 138, 104230. doi: 10.1016/j.autcon.2022.104230
25	VIRIYASITAVAT W , XU L D , BI Z , et al. Extension of specification language for soundness and completeness of service workflow[J]. Enterprise Information Systems, 2018, 12 (5): 638- 657. doi: 10.1080/17517575.2018.1432769
26	BHUSHAN M , GOEL S , KUMAR A . Improving quality of software product line by analysing inconsistencies in feature models using an ontological rule-based approach[J]. Expert Systems, 2018, 35 (3): e12256. doi: 10.1111/exsy.12256
27	KAUFMANN M, MOORE J S. An ACL2 tutorial[C]//Proc. of the International Conference on Theorem Proving in Higher Order Logics, 2008: 17-21.
28	ARP4754A. Guidelines for development of civil aircraft and systems[S]. Warrendale: SAE International, Warrendale, 2010.
29	王文浩, 毕文豪, 张安, 等. 基于MBSE的民机系统功能建模方法[J]. 系统工程与电子技术, 2021, 43 (10): 2884- 2892.
	WANG W H , BI W H , ZHANG A , et al. Function modeling method of civil aircraft system based on MBSE[J]. Systems Engineering and Electronics, 2021, 43 (10): 2884- 2892.
30	RYBAKOV M , SHKATOV D . Algorithmic properties of first-order superintuitionistic logics of finite Kripke frames in restricted languages[J]. Journal of Logic and Computation, 2021, 31 (2): 494- 522. doi: 10.1093/logcom/exaa091
31	MANOLIOS P. Scalable methods for analyzing formalized requirements and localizing errors[P]. U.S. : Patent 9639450, 2017-05-02.
32	赵长啸, 李浩, 董磊, 等. 基于STPA-Bayes模型的机载平视显示系统安全性分析与评价[J]. 系统工程与电子技术, 2020, 42 (5): 1083- 1092.
	ZHAO C X , LI H , DONG L , et al. Safety analysis and evaluation of airborne HUD system based on STPA-Bayes model[J]. Systems Engineering and Electronics, 2020, 42 (5): 1083- 1092.

案例名称	一致性检查类型	检查数量	冲突数据
案例名称	一致性检查类型	检查数量	冲突类型	数量	反例生成
HUD系统“飞行信息符号生成与显示”功能需求	需求自冲突检查	16	存在监控变量及其可行值, 但不存在相应受控变量	2	2
	需求自冲突检查	16	存在监控变量及其可行值、相应受控变量, 但该受控变量不存在可行值	2	3
	需求集冲突检查	16	存在监控变量但不存在该监控变量可行值	2	2
			存在一个监控变量及其可行值对应多个监控变量及可行值	2	3
			存在多个监控变量及其可行值同时成立时无相应受控变量及可行值	3	3
	需求关系一致性检查	14	全等与蕴含矛盾	1	1
	需求关系一致性检查	14	整体与局部矛盾	1	1

不同方法	是否支持功能需求细化	是否支持需求追踪	是否支持单条需求一致性检查	是否支持多条需求一致性检查	是否支持一致性检查	是否支持集合推理	是否支持反例生成
本文方法	✔	✔	✔	✔	✔	✔	✔
EARS-CTRL	✔		✔	✔
RSML		✔	✔
SpecTRM		✔	✔
UML	✔	✔	✔	✔	✔
SysML	✔	✔	✔	✔	✔
DoDAF/ 描述逻辑	✔				✔	✔
TRIC/FOL	✔	✔			✔	✔

[1]	王华友, 张诚诚, 薛海红, 刘轶斐. 基于“回归+马尔可夫”组合模型的民用航空事故症候数预测[J]. 系统工程与电子技术, 2023, 45(7): 2114-2120.
[2]	李昕泽, 周文雅, 刘凯, 王博. 可达区域内最佳着陆场的筛选方法[J]. 系统工程与电子技术, 2023, 45(6): 1712-1721.
[3]	韩维, 刘子玄, 苏析超, 崔凯凯, 刘洁. 结合启发式与最优控制的舰载机甲板路径规划算法[J]. 系统工程与电子技术, 2023, 45(4): 1098-1110.
[4]	李峻森, 方依宁, 张云安, 白光晗, 陶俊勇. 面向任务的装备保障体系多Agent建模与评估方法[J]. 系统工程与电子技术, 2023, 45(1): 279-290.
[5]	史文卿, 王海峰, 陈海昕. 战斗机无人机编组协同系统需求捕获与验证[J]. 系统工程与电子技术, 2023, 45(1): 108-118.
[6]	王鹏, 孙紫荆, 张帆, 肖国松. 考虑概率型共因失效的多阶段任务系统可靠性分析模型[J]. 系统工程与电子技术, 2022, 44(12): 3887-3898.
[7]	李耀华, 高源. 基于STPA-ANP模型的民机系统安全性分析[J]. 系统工程与电子技术, 2022, 44(9): 2986-2994.
[8]	郭斐然, 于剑桥, 宋豹. 基于指派模型的导弹装备体系弹种优化设计[J]. 系统工程与电子技术, 2022, 44(3): 850-862.
[9]	范秋岑, 毕文豪, 张安, 王文浩. 民用飞机高度控制系统MBSE建模方法[J]. 系统工程与电子技术, 2022, 44(1): 164-171.
[10]	王雨农, 毕文豪, 张安, 詹超. 基于DoDAF的民机MBSE研制方法[J]. 系统工程与电子技术, 2021, 43(12): 3579-3585.
[11]	柯宇航, 李艳军, 曹愈远, 张兴成. 基于模型的飞控系统安全性分析研究[J]. 系统工程与电子技术, 2021, 43(11): 3259-3265.
[12]	康文文, 李浩敏. 基于模型的飞机系统架构多视图表达方法[J]. 系统工程与电子技术, 2021, 43(11): 3266-3277.
[13]	王文浩, 毕文豪, 张安, 范秋岑. 基于MBSE的民机系统功能建模方法[J]. 系统工程与电子技术, 2021, 43(10): 2884-2892.
[14]	李德林, 毕文豪, 张安, 范秋岑. 基于MBSE的民机研制过程管理[J]. 系统工程与电子技术, 2021, 43(8): 2209-2220.
[15]	贾高伟, 王建峰. 无人机集群任务规划方法研究综述[J]. 系统工程与电子技术, 2021, 43(1): 99-111.