基于 SysML 的机载软件分层精化建模与验证方法

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.