基于SysML2NuSMV的民用飞机电传飞控系统安全性分析

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

Abstract

Abstract:

To solve the problem of excessive reliance on the experience of analysts in the safety analysis of traditional fly-by-wire （FBW） flight systems, a model-based safety analysis method by comprehensively using system modeling language （SysML） and new symbolic model verifier （NuSMV） to describe system behavior is proposed. Firstly, a nominal model and fault model of the FBW system are established using SysML, and a fault information extraction method based on SysML is proposed. Then, establish mapping rules between SysML and NuSMV models, and use the extracted fault information to automatically generate a NuSMV model that describes the system fault behavior. Finally, the security analysis of the FBW system is achieved through model checking. This method avoids reliance on personnel skills and experience, and the security analysis results are directly generated by the design model. When the design scheme is modified, the security analysis results can be automatically updated to avoid the tedious work caused by re conducting security analysis.

Key words: safety analysis, system modeling language （SysML）, new symbolic model verifier （NuSMV）, model-checking, fly-by-wire （FBW） system

CLC Number:

V 240.2

Kang LAI, Zhong LU, Dawei CHENG, Weirun MIAO. Safety analysis of civil aircraft fly-by-wire system based on SysML2NuSMV[J]. Systems Engineering and Electronics, 2025, 47(11): 3802-3815.

Figures/Tables 26

Fig.1

Fig.2

Fig.3

Table 1

Table 2

Fig.4

Fig.5

Fig.6

Fig.7

Fig.8

Fig.9

Fig.10

Fig.11

Fig.12

Table 3

Fig.13

Table 4

Fig.14

Fig.15

Fig.16

Table 5

Fig.17

Fig.18

Fig.19

Table 6

Fig.20

References 22

1	SAE ARP 4754B. Guidelines for development of civil aircraft and systems[S]. Warrendale: Society of Automotive Engineers, 2023.
2	SAE ARP 4761A. Guidelines and methods for conducting the safety assessment process on civil airborne system and equipment[S]. Warrendale: Society of Automotive Engineers, 2023.
3	JOSHI A, WHALEN M, HEIMDAHL M. Model based safety analysis final report, NASA contractor report[R]. Washington: NASA, 2006.
4	胡晓义, 王如平, 王鑫, 等. 基于模型的复杂系统安全性和可靠性分析技术发展综述[J]. 航空学报, 2020, 41 (6): 147- 158.
	HU X Y, WANG R P, WANG X, et al. Recent development of safety and reliability analysis technology for model-based complex systems[J]. Acta Aeronautica et Astronautica Sinica, 2020, 41 (6): 147- 158.
5	陈磊, 焦健, 赵廷弟. 基于模型的复杂系统安全分析综述[J]. 系统工程与电子技术, 2017, 39 (6): 1287- 1291.
	CHEN L, JIAO J, ZHAO T D. Review for model-based safety analysis of complex safety-critical system[J]. Systems Engineering and Electronics, 2017, 39 (6): 1287- 1291.
6	LIU J T, WANG H W, ZHENG W. A safety modelling method for high-speed train control systems based on UML extension[C]// Proc.of the Chinese Automation Congress, 2020: 317−321.
7	SHAO N, ZHANG S G, LIANG H. Model-based safety analysis of a control system using Simulink and Simscape extended models[C]//Proc.of the 3rd International Conference on Mechanical, Electronic and Information Technology Engineering, 2017, 139: 00219.
8	KIRAN R, JEPPU Y. Autopilot mode transitions and voter logic validation using model checking: a design study of formal methods[C]//Proc.of the Smart Sensors Measurements and Instrumentation, 2021: 263−281.
9	PECIAK M, SKARKA W. Assessment of the potential of electric propulsion for general a viation using model-based system engineering（MBSE）methodology[J]. Aerospace, 2022, 9 (2): 74- 96. doi: 10.3390/aerospace9020074
10	PING M L, ZHANG X B, GAO Z H, et al. Simulation model development of three-stage synchronous generator for aircraft power systems based on modelica[C]//Proc.of the 19th International Conference on Electrical Machines and Systems, 2016.
11	SANNES P S, APVRILLE L, VINGERHOEDS R. Checking SysML models against safety and security properties[J]. Journal of Aerospace Information Systems, 2021, 18 (12): 906- 918. doi: 10.2514/1.I010950
12	WOLNY S, MAZAK A, CARPELLA C, et al. Thirteen years of SysML: a systematic mapping study[J]. Software and Systems Modeling, 2020, 19 (1): 111- 169. doi: 10.1007/s10270-019-00735-y
13	STEWART D, LIU J, COFER D, et al. AADL-based safety analysis using formal methods applied to aircraft digital systems[J]. Reliability Engineering & System Safety, 2021, 213, 107649.
14	WEI X M, DONG Y W, LI X L, et al. Architecture-level hazard analysis using AADL[J]. Journal of Systems and Software, 2018, 137, 580- 604. doi: 10.1016/j.jss.2017.06.018
15	BOZZANO M, CIMATTI A, LISAGOR O, et al. Safety assessment of AltaRica models via symbolic model checking[J]. Science of Computer Programming, 2015, 98 (4): 464- 483.
16	祁健, 胡军, 谷青范, 等. 一种AltaRica 3.0模型中类的平展化方法[J]. 计算机科学, 2021, 48 (5): 51- 59. doi: 10.11896/jsjkx.200700184
	QI J, HU J, GU Q F, et al. Class flattening method for AltaRica 3.0 model[J]. Computer Science, 2021, 48 (5): 51- 59. doi: 10.11896/jsjkx.200700184
17	王少鹏. 基于时间自动机方法的SysML状态机图形式化建模与验证[D]. 上海: 华东师范大学, 2023.
	WANG S P. Formal verification of SysML state machine: time automata approach[D]. Shanghai: East China Normal University, 2023.
18	KAISER B, SODEN M, HEUERMANN N. A UAV case study on an MBSE workflow with integrated modular safety and reliability analysis[C]//Proc.of the Annual Reliability and Maintainability Symposium, 2024.
19	WANG Y P, WANG T T, LI X L, et al. Fault tree generation and analysis based on extended SysML model[C]//Proc.of the International Conference on High Performance Computing and Communication Engineering, 2024: 130730.
20	荘露, 陆中, 张子文. 基于随机Petri网的机载系统动态可靠性建模[J]. 西北工业大学学报, 2020, 38 (4): 846- 854. doi: 10.3969/j.issn.1000-2758.2020.04.020
	ZHUANG L, LU Z, ZHANG Z W. Dynamic reliability model for airborne systems based on stochastic Petri net[J]. Journal of Northwestern Polytechnical University, 2020, 38 (4): 846- 854. doi: 10.3969/j.issn.1000-2758.2020.04.020
21	张金辉, 赵滟, 毛寅轩, 等. 基于模型的可靠性、安全性分析方法[J]. 科技导报, 2024, 42 (8): 101- 110.
	ZHANG J H, ZHAO Y, MAO Y X, et al. A survey of model-based reliability and safety analysis methods[J]. Science & Technology Review, 2024, 42 (8): 101- 110.
22	ALMERAZ C N, LOPEZ-TERRAZAS R J, TSENG T L. A model-based systems engineering approach to obtain fault trees for failure analysis using SysML[C]//Proc.of the IEEE International Conference on Recent Advances in Systems Science and Engineering, 2021.

FBW子系统或部件	SysML模块
主飞控计算机	System
作动器控制电子	System
备份计算机	System
传感器	System
远程控制电子	System
作动器	Component
舵面	Component
其他	Component

模块名称	模块含义
PFC	主飞行控制计算机子系统模块
CommandChannel	监控支路模块
MonitorChannel	指令支路模块
Voter	信号表决模块
PFCMode	工作模式判断模块

构件	故障类型	故障描述	故障率/FH
PFC	F_stuck	输出卡滞	1E-7
	F_random	随机输出	1E-7
	F_omission	无响应	2E-7
ACE	A_stuck	输出卡滞	4E-7
	A_random	随机输出	1E-7
	A_omission	无响应	2E-7
REU	R_stuck	输出卡滞	1E-8
REU	R_omission	无响应	1E-8
PCU	P_jam	机械卡阻	1E-6
PCU	P_omission	无响应	1E-6
传感器	S_omission	无响应	4E-7
	S_stuck	输出卡滞	4E-7
	S_random	随机输出	4E-7
BCM	B_stuck	输出卡滞	4E-7
	B_random	随机输出	1E-7
	B_omission	无响应	2E-7

SysML模型	SysML模型在XML文档中的表达
系统模块	<UML：Class name="…" xmi.id="…"> <UML：Stereotype name="System"/> </UML：Class>
组件模块	<UML：Class name="…" xmi.id="…"> <UML：Stereotype name="Component"/> </UML：Class>
组成部分属性	<UML：ClassifierRole name="…" xmi.id="…"> <UML：TaggedValue tag="owner" value="…"/> <UML：TaggedValue tag="propertyType" value="…"/> </UML：ClassifierRole>
端口	<UML：Class name="…" xmi.id="…"> <UML：TaggedValue tag="ea_stype" value="Port"/> <UML：TaggedValue tag="owner" value="…"/> </UML：Class>
连接器	<UML：Association xmi.id="…"> <UML：TaggedValue tag="ea_type" value="Connector"/> <UML：Association.connection>  </UML：Association.connection> </UML：Association>
状态	<UML：SimpleState name="…" xmi.id="…"> <UML：Stereotype name="…"/> <UML：TaggedValue tag="owner" value="…"/> <UML：TaggedValue tag="behavior" value="…"/> </UML：SimpleState>
故障模式	<UML：Class name="…" xmi.id="…"> <UML：Stereotype name="Failure Mode"/> </UML：Class>
转换	<UML：Transition xmi.id="…" source="…" target="…"> <UML：Event name="…"/> <UML：BooleanExpression body="…"/> <UML：TaggedValue tag="$ea_xref_property" value="…"/> </UML：Transition>

序号	模块及交互关系	序号	模块及交互关系
1	IRU	8	LOE_REU（ACE3.output）
2	AD	9	LIE_REU（ACE1.output，BCM.output）
3	AOA	10	ROE_REU（ACE4.output）
4	DMRS	11	RIE_REU（ACE2.output，BCM.output）
5	SDS	12	UPR_REU（ACE3.output）
6	Attitude	13	MDR_REU（ACE1.output，BCM.output）
7	FSECU	14	LWR_REU（ACE4.output）
15	LIA_REU（ACE1.output，BCM.output）	30	PFC1（IRU.output，AoA.output，AD.output， FSECU.output，Attitude.output）
16	LOA_REU（ACE3.output）	30
17	RIA_REU（ACE2.output，BCM.output）	31	PFC2（IRU.output，AoA.output，AD.output， FSECU.output，Attitude.output）
18	ROA_REU（ACE4.output）	31
19	LOE_PCU（LOE_REU.output）	32	PFC3（IRU.output，AoA.output，AD.output， FSECU.output，Attitude.output）
20	LIE_PCU（LIE_REU.output）	32
21	ROE_PCU（ROE_REU.output）	33	ACE1（PFC1.output，PFC2.output，PFC3.output， SDS.output，DMRS.output）
22	RIE_PCU（RIE_REU.output）	33
23	UPR_PCU（UPR_REU.output）	34	ACE2（PFC1.output，PFC2.output，PFC3.output， SDS.output，DMRS.output）
24	MDR_PCU（MDR_REU.output）	34
25	LWR_PCU（LWR_REU.output）	35	ACE3（PFC1.output，PFC2.output，PFC3.output， SDS.output，DMRS.output）
26	LIA_PCU（LIA_REU.output）	35
27	LOA_PCU（LOA_REU.output）	36	ACE4（PFC1.output，PFC2.output，PFC3.output， SDS.output，DMRS.output）
28	RIA_PCU（RIA_REU.output）	36
29	ROA_PCU（ROA_REU.output）	37	BCM（ACE1.Mode，ACE2.Mode，ACE3.Mode，ACE4.Mode， ACE1.output，ACE2.output，ACE3.output. ACE4.output）

Safety analysis of civil aircraft fly-by-wire system based on SysML2NuSMV

RichHTML

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 26

References 22

Related Articles 14

Recommended Articles

Metrics

Comments

序号	阶数	割集元素
1	2	LOE_PCU_jam，LIE_PCU_jam
2	2	LOE_PCU_omission，LIE_PCU_jam
3	2	LOE_PCU_omission，LIE_PCU_omission
4	2	LOE_PCU_jam，LIE_PCU_omission
5	2	LOE_REU_stuck，LIE_REU_stuck
6	2	LOE_REU_omission，LIE_REU_stuck
7	2	ACE1_stuck，ACE3_stuck
8	2	ACE1_random，LOE_PCU_jam
9	2	ACE1_omission，LOE_PCU_omission
10	2	ACE1_random，LOE_REU_stuck
11	2	ACE1_stuck，LOE_REU_omission
12	2	ACE3_omission，LIE_REU_stuck
13	3	AoA_omisson，PFC1_mon_lane_stuck， LOE_PCU_jam
14	3	AoA_omission，PFC1_com_lane_random， LOE_PCU_jam
15	3	IRU_omission，PFC1_mon_lane_random， LOE_PCU_jam
16	4	ACE1_omission，ACE2_omission， ACE4_omission，BCM_stuck
17	4	ACE1_omission，ACE2_omission， ACE4_omission，BCM_random
18	4	ACE1_omission，ACE2_omission， ACE4_omission，BCM_omission
19	5	PFC1_com_lane_stuck，PFC2_com_lane_stuck， PFC3_com_lane_stuck，DMRS_omisson， FSECU_omisson
20	5	PFC1_com_lane_random，PFC2_mon_lane_stuck， PFC3_com_lane_stuck，DMRS_omisson， FSECU_omission

[1]	Yaqun QI, Ping JIN, Qibo PENG, Hailian ZHANG, Guobiao CAI. Model-based fault identification and modeling method for space propulsion system [J]. Systems Engineering and Electronics, 2024, 46(12): 4062-4073.
[2]	Xin JIN, Yufeng HE. Method for automatic generation of space effective payload test paths based on SysML [J]. Systems Engineering and Electronics, 2024, 46(10): 3416-3426.
[3]	Haoliang REN, Jianchao ZHANG, Huichuan CHENG. Modeling and analysis method of weapon equipment system capability requirements based on SysML [J]. Systems Engineering and Electronics, 2023, 45(9): 2843-2851.
[4]	Ran HUANG, Qibo PENG, Xinfeng WU, Qing NI. Architecture modeling for manned lunar landing based on DoDAF [J]. Systems Engineering and Electronics, 2023, 45(7): 2131-2137.
[5]	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.
[6]	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.
[7]	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.
[8]	Changxiao ZHAO, Hao LI, Lei DONG, Peng WANG. Safety analysis and evaluation of airborne HUD system based on STPA-Bayes model [J]. Systems Engineering and Electronics, 2020, 42(5): 1083-1092.
[9]	Sen QIAO, Zhiqiu HUANG, Jinyong WANG, Weijian WAN. DFT quantitative analysis method based on statistical model checking [J]. Systems Engineering and Electronics, 2020, 42(2): 480-488.
[10]	CHEN Lu, JIAO Jian, WEI Qianxin. Model-checking oriented unified modeling method based on NuSMV [J]. Systems Engineering and Electronics, 2018, 40(7): 1654-1659.
[11]	CHEN Lei, JIAO Jian, ZHAO Tingdi. Review for model-based safety analysis of complex safety-critical system [J]. Systems Engineering and Electronics, 2017, 39(6): 1287-1291.
[12]	KE Wenjun, CHEN Jing, JIANG Shan. System simulation and verification method based on Petri net model [J]. Systems Engineering and Electronics, 2017, 39(4): 924-930.
[13]	HE Deyu1,2, HU Niaoqing1,2, HU Lei1,2, CHEN Ling1,2, GUO Yiping3. Design of demonstration platform of fault safety analysis -based on virtual prototyping [J]. Systems Engineering and Electronics, 2017, 39(3): 681-686.
[14]	JIANG Jiang,LI Xuan,CHEN Ying-wu,YANG Ke-wei. Evidential network and its application in safety analysis of aerospace systems [J]. Journal of Systems Engineering and Electronics, 2011, 33(6): 1270-1275.