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

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

Abstract

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

CLC Number:

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.

Figures/Tables 15

Fig.1

Fig.2

Fig.3

Fig.4

Fig.5

Fig.6

Fig.7

Fig.8

Table 1

Functional requirements of "flight information symbol generation and display" (partial)"

需求类型	需求编号	需求描述
内部功能需求	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”
	⋮	⋮

Table 1

Fig.9

Fig.10

Fig.11

Fig.12

Table 2

Table 3

References 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]	Huayou WANG, Chengcheng ZHANG, Haihong XUE, Yifei LIU. Prediction of the number of accident symptoms in civil aviation based on "regression+Markov" combined model [J]. Systems Engineering and Electronics, 2023, 45(7): 2114-2120.
[2]	Xinze LI, Wenya ZHOU, Kai LIU, Bo WANG. Screening method for the optimal landing site in the reachable area [J]. Systems Engineering and Electronics, 2023, 45(6): 1712-1721.
[3]	Wei HAN, Zixuan LIU, Xichao SU, Kaikai CUI, Jie LIU. Deck path planning algorithm of carrier-based aircraft based on heuristic and optimal control [J]. Systems Engineering and Electronics, 2023, 45(4): 1098-1110.
[4]	Junsen LI, Yining FANG, Yun'an ZHANG, Guanghan BAI, Junyong TAO. Multi-agent modeling and evaluation method for mission-oriented equipment support SoS [J]. Systems Engineering and Electronics, 2023, 45(1): 279-290.
[5]	Wenqing SHI, Haifeng WANG, Haixin CHEN. Fighter-drone teaming system requirements elicitation and verification [J]. Systems Engineering and Electronics, 2023, 45(1): 108-118.
[6]	Peng WANG, Zijing SUN, Fan ZHANG, Guosong XIAO. Reliability analysis model for phased-mission system considering probabilistic common cause failures [J]. Systems Engineering and Electronics, 2022, 44(12): 3887-3898.
[7]	Yaohua LI, Yuan GAO. Safety analysis for civil aircraft system based on STPA-ANP model [J]. Systems Engineering and Electronics, 2022, 44(9): 2986-2994.
[8]	Feiran GUO, Jianqiao YU, Bao SONG. Optimal design of missile types in missile equipment system based on assignment model [J]. Systems Engineering and Electronics, 2022, 44(3): 850-862.
[9]	Qiucen FAN, Wenhao BI, An ZHANG, Wenhao WANG. MBSE modeling method of civil aircraft altitude control system [J]. Systems Engineering and Electronics, 2022, 44(1): 164-171.
[10]	Yunong WANG, Wenhao BI, An ZHANG, Chao ZHAN. DoDAF-based civil aircraft MBSE development method [J]. Systems Engineering and Electronics, 2021, 43(12): 3579-3585.
[11]	Yuhang KE, Yanjun LI, Yuyuan CAO, Xingcheng ZHANG. Research on model-based safety analysis of flight control system [J]. Systems Engineering and Electronics, 2021, 43(11): 3259-3265.
[12]	Wenwen KANG, Haomin LI. Multi-view representation method of aircraft system architecture based on model [J]. Systems Engineering and Electronics, 2021, 43(11): 3266-3277.
[13]	Wenhao WANG, Wenhao BI, An ZHANG, Qiucen FAN. Function modeling method of civil aircraft system based on MBSE [J]. Systems Engineering and Electronics, 2021, 43(10): 2884-2892.
[14]	Delin LI, Wenhao BI, An ZHANG, Qiucen FAN. MBSE-based process management in the development of civil aircraft [J]. Systems Engineering and Electronics, 2021, 43(8): 2209-2220.
[15]	Gaowei JIA, Jianfeng WANG. Research review of UAV swarm mission planning method [J]. Systems Engineering and Electronics, 2021, 43(1): 99-111.

Requirement consistency checking method for civil aircraft systems based on finite predicate tracing

RichHTML

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 15

References 32

Related Articles 15

Recommended Articles

Metrics

Comments