Systems Engineering and Electronics ›› 2022, Vol. 44 ›› Issue (4): 1282-1290.doi: 10.12305/j.issn.1001-506X.2022.04.26
• Systems Engineering • Previous Articles Next Articles
Jiachen LIU1,2, Lei DONG1,2,3,*, Changxiao ZHAO1,2,3, Hongbing CHEN1,2
Received:
2021-02-17
Online:
2022-04-01
Published:
2022-04-01
Contact:
Lei DONG
CLC Number:
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.
Table 5
Verification of system logic and time sequence correctness"
验证性质 | 性质验证语句 | 验证结果 | 消耗时间/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 |
Table 6
Reachability verification of dynamic reconfiguration behavior"
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 |
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. |
[1] | Zhiwei CHEN, Jing WANG, Changchao GU, Jianchun ZHANG, Jilong ZHONG. Performance availability and resilience analysis of weapon system of systems considering dynamic reconfiguration [J]. Systems Engineering and Electronics, 2021, 43(8): 2347-2354. |
[2] | Peng WANG, Jiachen LIU, Lei DOND, Changxiao ZHAO. Task oriented DIMA dynamic reconfiguration strategy for civil aircraft [J]. Systems Engineering and Electronics, 2021, 43(6): 1618-1627. |
[3] | Xinfeng FAN, Zhiliang TAN. Follower jamming suppression method via digital cancellation [J]. Systems Engineering and Electronics, 2020, 42(6): 1235-1240. |
[4] | LING Dongyi, WANG Shihai, LIU Bin. Reliability assessment method for component system based on AADL architecture model [J]. Systems Engineering and Electronics, 2017, 39(4): 947-952. |
[5] | 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. |
[6] | LI You-yi, ZHANG Zhi-chun, XIONG Zhuang, XIAO Jing-xin, LI Guo-hui. Collision modeling method of ship-board helicopter landing [J]. Systems Engineering and Electronics, 2015, 37(7): 1691-1696. |
[7] | PEI Fu-jun, CHENG Yu-hang, LI Hao-yang, JU He-hua. Distributed simultaneous localization and mapping algorithm based on partition of space-region [J]. Systems Engineering and Electronics, 2015, 37(3): 639-645. |
[8] | HAO Nuo, ZHAO Ting-di, FENG Chang. Dynamic reconfiguration system safety analysis method based on multi-state space [J]. Systems Engineering and Electronics, 2014, 36(2): 317-325. |
[9] | XIA Qing-yuan, XU Jin-fa, ZHANG Liang. Modelfree adaptive attitude controller for a tilt-rotor aircraft [J]. Journal of Systems Engineering and Electronics, 2013, 35(1): 146-151. |
[10] | LI Zhen, LIU Bin, LI Xiao-xun, YIN Yong-feng. Verification of safetycritical software requirement based on Petri-net model checking [J]. Journal of Systems Engineering and Electronics, 2011, 33(2): 458-463. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||