Hierarchical Refined Modeling and Verification Method of Airborne Software Using SysML

被引：0

作者：

Xiao S.-H. ^{[1
,2
]}

Liu Q. ^{[1
,2
]}

Huang Y.-H. ^{[1
,2
]}

Shi J.-Q. ^{[1
,2
]}

Guo X. ^{[1
,2
]}

机构：

[1] Software Engineering Institute, East China Normal University, Shanghai

[2] National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai

来源：

Ruan Jian Xue Bao/Journal of Software | 2022年 / 33卷 / 08期

关键词：

airborne software; model checking; model refinement; model transformation;

D O I：

10.13328/j.cnki.jos.006602

中图分类号：

学科分类号：

摘要：

Airborne software is widely used in aerospace, which dramatically improves the performance of airborne equipment. Nevertheless, with airborne software's increasing scale and function, it is challenging to develop airborne software. How to ensure the correctness and safety of airborne software has become a difficult problem to be solved. Model-based development can effectively improve development efficiency, and formal methods can effectively guarantee the correctness of software. To reduce the difficulty of development and ensure airborne software’s correctness and safety, this study proposes a hierarchical refinement modeling and verification method of airborne software using the SysML state machine diagram subset. Firstly, the SysML state machine diagram is used to model the dynamic behavior of airborne software. According to the proposed refinement rules, the initial model is refined to obtain the refined design model step by step manually. Then, according to the dynamic characteristics of the software model, the SysML state machine model is automatically converted to a network of timed automata, and the formal TCTL properties are manually extracted from the software requirements for model checking. Secondly, to realize coding automation, the SysML model is automatically converted to Simulink, and Simulink Coder generates the source code. Finally, an automatic flight control software is developed and verified based on the proposed method, and the experimental results show the effectiveness of the method. © 2022 Chinese Academy of Sciences. All rights reserved.

引用

页码：2851 / 2874

页数：23

共 32 条

[11]

Miotto P, Breger L, Sargent R., Simulation and flight software development using model-based design with MATLAB and UML tools, Proc. of the AIAA Modeling and Simulation Technologies Conf. 2012, (2012)

[12]

David A, Larsen KG, Legay A, Mikucionis M, Poulsen DB., Uppaal SMC tutorial, Int’l Journal on Software Tools for Technology Transfer, 17, pp. 397-415, (2015)

[13]

Chen X, Gu Q, Liu WS, Et al., Survey of static software defect prediction, Ruan Jian Xue Bao/Journal of Software, 27, 1, (2016)

[14]

Hao JF, Ye H, Ren XR., Research on formal methods of DO-333 supplement, Aeronautical Computing Technique, 50, 1, pp. 124-129, (2020)

[15]

Meta object facility core specification v2.0, (2006)

[16]

Liu ZZ., The study of consistency issues in model transformations based on graph theory, (2010)

[17]

van Benthem, Johan FAK, ter Meulen A., Handbook of Logic and Language, (2011)

[18]

Xu J., Aircraft Automatic Flight Control System, (2020)

[19]

Gao S, Cao W, Fan L, Et al., MBSE for satellite communication system architecting, IEEE Access, 7, pp. 164051-164067, (2019)

[20]

Dmitriev K, Zafar SA, Schmiechen K, Et al., A lean and highly-automated model-based software development process based on DO-178C/DO-331, Proc. of the 39th AIAA/IEEE Digital Avionics Systems Conf. (DASC), pp. 1-10, (2020)

← 1 2 3 4 →