基于形式化方法的DIMA动态重构仿真与验证

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

系统工程与电子技术 ›› 2022, Vol. 44 ›› Issue (4): 1282-1290.doi: 10.12305/j.issn.1001-506X.2022.04.26

基于形式化方法的DIMA动态重构仿真与验证

刘嘉琛^1,², 董磊^1,^2,^3,*, 赵长啸^1,^2,³, 陈泓兵^1,²

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

收稿日期:2021-02-17 出版日期:2022-04-01 发布日期:2022-04-01
通讯作者: 董磊
作者简介:刘嘉琛(1996—), 男, 博士研究生, 主要研究方向为航空电子综合研究、形式模型与安全性评估|董磊(1983—), 男, 副研究员, 博士, 主要研究方向为形式模型与安全性评估|赵长啸(1989—),男, 副研究员, 博士, 主要研究方向为民机航电系统设计与评估、航空电子综合研究|陈泓兵(1996—), 男, 硕士研究生, 主要研究方向为单一飞行员操作
基金资助:
国家自然科学基金-民航联合基金(U1933106);航空科学基金(20185167017);中央高校基本科研业务费(3122019167)

Simulation and verification of DIMA dynamic reconfiguration based on formal method

Jiachen LIU^1,², Lei DONG^1,^2,^3,*, Changxiao ZHAO^1,^2,³, Hongbing CHEN^1,²

1. College of Safety Science and Engineering, Civil Aviation University of China, Tianjin 300300, China
2. Key Laboratory of Civil Aircraft Airworthiness Technology, Civil Aviation University of China, Tianjin 300300, China
3. Civil Aircraft Airworthiness and Repair Key Laboratory of Tianjin, Tianjin 300300, China

Received:2021-02-17 Online:2022-04-01 Published:2022-04-01
Contact: Lei DONG

摘要/Abstract

摘要：

针对可重构分布式综合模块化航空电子(distributed integrated modular avionics, DIMA)系统在设计初期缺少仿真与验证手段的问题, 首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理(generic system management, GSM)的组件功能划分。然后, 使用架构分析与设计语言(architecture analysis and design language, AADL)及其相关附件对DIMA动态重构的架构基础、行为细节等要素进行建模。在此基础上, 设计了一种基于形式化定义的模型转换规则, 该规则将AADL动态重构模型转换成可执行的时间自动机模型。最后, 利用模型验证工具UPPAAL验证了可重构DIMA系统逻辑及时序的正确性和不安全控制行为的可达性。结果表明, 所提方法具有可行性和有效性, 并且能够为后续DIMA动态重构的形式化安全性评估提供模型基础。

关键词: 分布式综合模块化航空电子, 动态重构, 架构分析与设计语言, 形式化方法, 仿真验证

Abstract:

In view of the lack of simulation and verification means in the early design stage of reconfigurable distributed integrated modular avionics (DIMA) system, the architecture characteristics of reconfigurable DIMA software system and the component function division of hierarchical generic system management (GSM) supporting dynamic reconfiguration are analyzed firstly. Then, architecture analysis and design language (AADL) and its related accessories are used to model the architectural basis, behavior details and other elements of DIMA dynamic reconfiguration. On this basis, a model transformation rule based on formal definition is designed, which transforms AADL dynamic reconstruction model into executable timed automata model. Finally, the correctness of logic and timing of reconfigurable DIMA system and the accessibility of unsafe control behavior are verified by using model verification tool UPPAAL. The results show that the proposed method is feasible and effective, and can provide a model basis for the formal security evaluation of subsequent DIMA dynamic reconfiguration.

Key words: distributed integrated modular avionics (DIMA), dynamic reconfiguration, architecture analysis and design language (AADL), formal method, simulation verification

中图分类号:

V243

刘嘉琛, 董磊, 赵长啸, 陈泓兵. 基于形式化方法的DIMA动态重构仿真与验证[J]. 系统工程与电子技术, 2022, 44(4): 1282-1290.

Jiachen LIU, Lei DONG, Changxiao ZHAO, Hongbing CHEN. Simulation and verification of DIMA dynamic reconfiguration based on formal method[J]. Systems Engineering and Electronics, 2022, 44(4): 1282-1290.

图/表 13

图1

图2

表1

图3

表2

图4

图5

表3

图6

图7

表4

表5

表6

参考文献 31

1	ROBATI T , GHERBI A , MULLINS J . A modeling and verification approach to the design of distributed IMA architectures using TTEthernet[J]. Procedia Computer Science, 2016, 83, 229- 236. doi: 10.1016/j.procs.2016.04.120
2	WOLFIG R, JAKOVLJEVIC M. Distributed IMA and DO-297: architectural, communication and certification attributes[C]//Proc. of the IEEE/AIAA 27th Digital Avionics Systems Confe-rence, 2008.
3	FUCHSEN R . IMA NextGen: a new technology for the Scarlett program[J]. IEEE Aerospace and Electronic Systems Magazine, 2010, 25 (10): 10- 16. doi: 10.1109/MAES.2010.5631720
4	郭阳明, 米琪, 张双, 等. 基于故障预测与健康管理的DIMA动态重构技术综述[J]. 计算机测量与控制, 2019, 27 (10): 101- 104.
	GUO Y M , MI Q , ZHANG S , et al. Review of DIMA dynamic reconstruction technology based on prognostic and health mana-gement[J]. Computer Measurement &Control, 2019, 27 (10): 101- 104.
5	阎芳, 邢培培, 赵长啸, 等. 基于联合k/n(G)模型的DIMA系统可靠性建模与分析[J]. 航空学报, 2018, 39 (6): 190- 198.
	YAN F , XING P P , ZHAO C X , et al. Reliability modeling and analysis of DIMA system based on joint k/n(G) model[J]. Aeronautica et Astronautica Sinica, 2018, 39 (6): 190- 198.
6	JIANG Z T , ZHAO T , WANG S , et al. New model-based analysis method with multiple constraints for integrated modular avionics dynamic reconfiguration process[J]. Processes, 2020, 8 (5): 574- 596. doi: 10.3390/pr8050574
7	WEI X M, DONG Y W, XIAO M R. Safety-based software reconfiguration method for integrated modular avionics systems in AADL Model[C]//Proc. of the IEEE International Conference on Software Quality, Reliability and Security Companion, 2018.
8	DA F A A , DO N F A M , NADJM-TEHRANI S , et al. Timing assurance of avionic reconfiguration schemes using formal analysis[J]. IEEE Trans.on Aerospace and Electronic Systems, 2019, 56 (1): 95- 106.
9	GU Q B, WANG G, WU J J, et al. Dynamic reconfiguration mechanism for distributed integrated modular avionics system[C]//Proc. of the AIAA Aviation Technology, Integration, and Operations Confe-rence, 2015.
10	杨威, 张晓红. 机载分布式系统管理中消息交互机制探究[J]. 计算机测量与控制, 2015, 23 (10): 3430- 3433.
	YANG W , ZHANG X H . Study of message interaction mechanism of the airborne distributed management system[J]. Computer Measurement & Control, 2015, 23 (10): 3430- 3433.
11	王震, 朱剑锋, 洪沛. 基于分布式IMA平台的系统健康管理的设计与实现[J]. 航空电子技术, 2016, 47 (2): 11- 15. doi: 10.3969/j.issn.1006-141X.2016.02.03
	WANG Z , ZHU J F , HONGN P . Design and implementation of system health management based on distributed IMA platform[J]. Avionics Technology, 2016, 47 (2): 11- 15. doi: 10.3969/j.issn.1006-141X.2016.02.03
12	HASKINS C, FORSBERG K, KRUEGER M, et al. Systems engineering handbook[C]//Proc. of the International Council on Systems Engineering, 2006.
13	JOLLIFFE G , NICHOLSON M . Exploring the possibilities towards a preliminary safety case for IMA blueprints[M]. London: Springer, 2005: 163- 81.
14	STANAG 4626. Modular and open avionics architecture (Part I: Architecture)[S]. Brussels: North Atlantic Organization, 2005: 24-34.
15	ARINC653. Avionics application software standard interface[S]. Maryland: Aeronautical Radio Incorporation, 2003.
16	何锋. 航空电子系统综合调度理论与方法[M]. 北京: 清华大学出版社, 2017.
	HE F . Theory and approach to avionics system integrated scheduling[M]. Beijing: Tsinghua University Press, 2017.
17	杨军祥, 田泽, 湛文韬, 等. 新一代分布式IMA核心系统技术研究[J]. 微电子学与计算机, 2019, 36 (12): 36- 41.
	YANG J X , TIAN Z , ZHAN W T , et al. Research on new generation of distributed IMA core system technology[J]. Microeletronics & Computer, 2019, 36 (12): 36- 41.
18	AEROSPACE S. SAE AS5506C: architecture analysis and design language (AADL)[EB/OL]. [2021-02-10]. https://www.sae.org/standards/content/as5506c/, 2017.
19	凌冬怡, 王世海, 刘斌. 基于AADL体系结构模型的构件系统可靠性评估[J]. 系统工程与电子技术, 2017, 39 (4): 947- 952.
	LING D Y , WANG S H , LIU B . Reliability assessment method for component system based on AADL architecture model[J]. Systems Engineering and Electronics, 2017, 39 (4): 947- 952.
20	张博林, 杨志斌, 周勇, 等. 一种面向安全关键软件的AADL模型组合验证方法[J]. 计算机学报, 2020, 43 (11): 2134- 2151. doi: 10.11897/SP.J.1016.2020.02134
	ZHANG B L , YANG Z B , ZHOU Y , et al. A compositional verification method for AADL models of safety-critical software[J]. Chinese Journal of Computers, 2020, 43 (11): 2134- 2151. doi: 10.11897/SP.J.1016.2020.02134
21	AEROSPACE S. SAE AS5506/1A: architecture analysis and design language (AADL)[EB/OL]. [2021-02-12]. https://www.sae.org/standards/content/as5506/1a/, 2015.
22	AEROSPACE S. SAE AS5506/2: architecture analysis and design language (AADL)[EB/OL]. [2021-02-12]. https://www.sae.org/standards/content/as5506/2/, 2019.
23	LEVESON N G , THOMAS J P . STPA handbook[M]. Massachusetts: Cambridge, 2018.
24	LEVESON N G . Engineering a safer world: systems thinking applied to safety[M]. Massachusetts: The MIT Press, 2016.
25	赵长啸, 李浩, 董磊, 等. 基于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.
26	HU K , ZHANG T , YANG Z B , et al. Exploring AADL verification tool through model transformation[J]. Journal of Systems Architecture, 2015, 61 (4): 141- 56.
27	ALUR R , DILL D L . A theory of timed automata[J]. Theoretical Computer Science, 1994, 126 (2): 183- 235. doi: 10.1016/0304-3975(94)90010-8
28	HESSEL A , LARSEN K G , MIKUCIONIS M , et al. Testing real-time systems using UPPAAL[M]. Berlin: Springer, 2008: 77- 117.
29	DAKWAT A L , VILLANI E . System safety assessment based on STPA and model checking[J]. Safety Science, 2018, 109, 130- 143. doi: 10.1016/j.ssci.2018.05.009
30	朱智, 雷森, 雷永林. 基于模型驱动工程的形式化模型转换技术[J]. 系统仿真学报, 2021, 33 (9): 2119- 2127.
	ZHU Z , LEI S , LEI Y L . Exploring formal model transformation techniques within model driven engineering[J]. Journal of System Simulation, 2021, 33 (9): 2119- 2127.
31	NIGRO L, SCIAMMARELLA P F. Statistical model checking of distributed real-time actor systems[C]//Proc. of the IEEE/ACM 21st International Symposium on Distributed Simulation and Real Time Applications, 2017.

功能性组件	组件功能
HM	心跳消息采集, 心跳消息报错
FM	故障过滤, 故障处理, 故障上报
CM	容错方案调配, 配置状态切换
SM	身份认证, 消息加解密

动态重构元素	AADL实体
模块	以虚拟处理器为子组件的处理器
分区	虚拟处理器
分区	绑定到虚拟处理器和内存的进程
分区间通信(排队端口)	事件数据端口
健康监控	线程
故障管理
配置管理
功能应用
配置状态	模式

AADL数据	UPPAAL数据	数据类型映射描述
boolean	bool	将boolean映射为bool
integer	int	将integer映射为int
自定义数组	数组类型array	将自定义数组映射为数组类型array
自定义结构型	结构型数据struct	将自定义结构体映射为结构型数据struct

语句类型	含义
E◇p	若给定性质p在某个状态转移序列中的某个状态下为真, 则E◇p为真
A□p	等价于not E◇not p, 即所有状态转移序列中, 每一个状态均满足给定性质p
E□p	若给定性质p在某个状态转移序列中的所有状态下都为真, 则E□p为真
A◇p	等价于not E□not p, 即每个状态转移序列中, 至少有一个状态满足给定性质p

验证性质	性质验证语句	验证结果	消耗时间/s	消耗空间/KB
HM正常运行	E◇ HM.idle or HM.collect_hreatbeat or HM.inspect_hreatbeat or HM.send_message	满足该性质	0.063	31 500
FM正常运行	E◇ FM.filter_fault or FM.send_data	满足该性质	0.012	31 536
CM正常运行	E◇ CM.deploy_configuration_scheme or CM.stop_configuration or CM.load_configuration	满足该性质	0.015	31 468
FA1正常运行	E◇ FA1.idleorFA1.work or FA1.processing	满足该性质	0.012	31 488
FA2正常运行	E◇ FA2.idle or FA2.work or FA2.processing	满足该性质	0.012	31 488
RTBP正常运行	E◇ RTBP.idle or RTBP.work or RTBP.processing	满足该性质	0.012	31 488
FM在收到HM发送的心跳信息后才能进行过滤	A□ FM.filter_faultimply (HMsm_o!=3)	满足该性质	7.547	281 880
FA1在收到停止指令或收集心跳信息的指令后才会进入处理状态	A□ FA1.processing imply (CMsc_o!=3 or HM.collect_hreatbeat)	满足该性质	6.594	281 880
FA2在收到加载指令后才会进入处理状态	A□ FA2.processing imply (CMlc_o!=3)	满足该性质	6.781	281 880

基于形式化方法的DIMA动态重构仿真与验证

Simulation and verification of DIMA dynamic reconfiguration based on formal method

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 13

参考文献 31

相关文章 11

编辑推荐

Metrics

本文评价

UCA描述	UCA可达性验证语句	验证结果	消耗时间/s	消耗空间/KB
UCA-1:在已经获取行动列表的情况下, 控制指令无法加载到目标资源单元	E◇(HM_o+FM_o+RTBP_o+FA1_o+FA2_o+CMdcs_o==1) and (CM_o==3)	满足该性质	0.129	281 880
UCA-2:在已经获取行动列表的情况下, 加载错误的控制指令	E◇(HM_o+FM_o+FA1_o+FA2_o+CMdcs_o==1&&RTBP_o==2) and (CM_o==2)	满足该性质	6.328	281 884
UCA-3:在已经获取行动列表的情况下, 控制指令加载到错误的资源单元	E◇(HM_o+FM_o+RTBP_o+FA1_o+FA2_o+CMdcs_o==1) and (CM_o==2)	满足该性质	0.183	281 884
UCA-4:在没有获取行动列表的情况下, 控制指令就开始加载	E◇(HM_o+FM_o+FA2_o+CMdcs_o!=3&&RTBP_o==3) and (CM_o==1)	满足该性质	0.013	281 884
UCA-5:在已经获取行动列表的情况下, 未能及时加载控制指令	E◇(HM_o+FM_o+RTBP_o+FA1_o+FA2_o+CMdcs_o==1) and (CM_o==1 and z>8*t)	不满足该性质	9.753	290 876

[1]	陈志伟, 王靖, 谷长超, 章健淳, 钟季龙. 考虑动态重构的装备体系可用性及弹性分析[J]. 系统工程与电子技术, 2021, 43(8): 2347-2354.
[2]	王鹏, 刘嘉琛, 董磊, 赵长啸. 面向任务的民机DIMA动态重构策略[J]. 系统工程与电子技术, 2021, 43(6): 1618-1627.
[3]	范新峰, 谭志良. 基于数字对消的跟踪干扰抑制方法[J]. 系统工程与电子技术, 2020, 42(6): 1235-1240.
[4]	柯文俊, 陈静, 江山. 基于Petri网模型的系统仿真验证方法[J]. 系统工程与电子技术, 2017, 39(4): 924-930.
[5]	李友毅, 张志春, 熊壮, 肖景新, 李国辉. 舰载直升机着舰碰撞建模方法[J]. 系统工程与电子技术, 2015, 37(7): 1691-1696.
[6]	裴福俊, 程雨航, 李昊洋, 居鹤华. 基于空间域划分的分布式SLAM算法[J]. 系统工程与电子技术, 2015, 37(3): 639-645.
[7]	赵诺，赵廷弟，冯畅. 基于多状态空间的动态重构系统安全分析技术[J]. 系统工程与电子技术, 2014, 36(2): 317-325.
[8]	夏青元，徐锦法，张梁. 倾转旋翼飞行器无模型自适应姿态控制[J]. Journal of Systems Engineering and Electronics, 2013, 35(1): 146-151.
[9]	王亮, 康凤举, 邓红德, 陈怀民. 基于视觉的无人机着陆半物理仿真系统的应用[J]. Journal of Systems Engineering and Electronics, 2012, 34(7): 1511-1517.
[10]	杜湘瑜，梁甸农. 分布式卫星SAR柔性仿真系统设计与实现[J]. Journal of Systems Engineering and Electronics, 2012, 34(5): 915-919.
[11]	李震, 刘斌, 李小勋, 殷永峰. 基于Petri网模型检验的安全关键软件需求验证[J]. Journal of Systems Engineering and Electronics, 2011, 33(2): 458-463.