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 条

[1]

Huang ZQ, Xu BF, Kan SL, Et al., Survey on embedded software safety analysis standards, methods and tools for airborne system, Ruan Jian Xue Bao/Journal of Software, 25, 2, (2014)

[2]

DO-331: Model-based Development and Verification Supplement to DO-178C and DO-278A, (2011)

[3]

Formal Methods Supplement to DO-178C and DO-278A, (2011)

[4]

Lenny D., SysML Distilled: A Brief Guide to the Systems Modeling Language, (2013)

[5]

Unified modeling language: Superstructure version 2.0, (2005)

[6]

McKelvin ML, Jimenez A., Specification and design of electrical flight system architectures with SysML, Proc. of the AIAA Infotech at Aerospace Conf. and Exhibit, (2012)

[7]

Yang H, Zhan C, Wu H, Et al., Research on modeling of aircraft-level high-lift system architecture based on SysML, Journal of Physics. Conf. Series, 1827, (2021)

[8]

Kim Y, Gomez M, Goppert J, Et al., Model checking of a training system using NuSMV for humanoid robot soccer, pp. 531-540, (2015)

[9]

Ratiu D, Ulrich A., An integrated environment for Spin-based C code checking: Towards bringing model-driven code checking closer to practitioners, Int’l Journal on Software Tools for Technology Transfer, 21, pp. 267-286, (2019)

[10]

Ahn SJ, Hwang DY, Kang M, Et al., Hierarchical system schedulability analysis framework using UPPAAL, IEICE Trans. on Information and Systems, pp. 2172-2176, (2016)

← 1 2 3 4 →