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

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

摘要/Abstract

摘要：

为解决传统电传飞控系统安全性分析过度依赖分析人员经验的问题，综合利用系统建模语言（system modeling language，SysML）和新符号模型验证器（new symbolic model verifier，NuSMV）描述系统行为，提出一种基于模型的安全性分析方法。首先，利用SysML建立电传飞控系统的名义模型和故障模型，提出面向SysML的故障信息提取方法。然后，建立SysML和NuSMV模型的映射规则，利用提取的故障信息自动生成描述系统故障行为的NuSMV模型。最后，通过模型检测实现电传飞控系统的安全性分析。该方法避免了对人员技术和经验的依赖，并且安全性分析结果由设计模型直接生成。当设计方案修改时能自动更新安全分析结果，避免重新开展安全性分析带来的繁琐工作。

关键词: 安全性分析, 系统建模语言, 新符号模型验证器, 模型检测, 电传飞控系统

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

中图分类号:

V 240.2

赖康, 陆中, 程大炜, 缪炜润. 基于SysML2NuSMV的民用飞机电传飞控系统安全性分析[J]. 系统工程与电子技术, 2025, 47(11): 3802-3815.

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.

图/表 26

图1

图2

图3

表1

表2

图4

图5

图6

图7

图8

图9

图10

图11

图12

表3

图13

表4

图14

图15

图16

表5

图17

图18

图19

表6

图20

参考文献 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）