Safety SysML: An Executable Safety-Critical Avionics Requirement Modeling Language

Establishing formal modeling and verification methods for requirements has become the key to enhancing avionics software's safety and development efficiency. As the mainstream modeling language used in Model-Based Software Engineering (MBSE), SysML is often applied to software requirements specifications. However, due to the lack of systematic and rigorous semantic definitions, SysML can cause problems in terms of accuracy and consistency in system development, threatening the correctness of safety-critical avionics software. To address the problem, this paper defines Safety SysML State Machine, an extended SysML state machine for safety control functions. Stepwise, the authors illustrate the formal specification and the refinement rules of the Safety SysML State Machine to construct the avionics integration model. Furthermore, a tool is implemented integrating the modeling and verification of the Safety SysML State Machine. Our contribution has a profound potential to broaden the use of MBSE and its well-known advantages in safety-critical applications. A specific case study on the aircraft roll angle control system demonstrates the effectiveness of our approach and the tool.