Integrating Model Checking With SysML in Complex System Safety Analysis

Abstract

Modern complex systems are characterized by numerous complex interactions and high levels of integration of functions, which present new challenges from the viewpoints of system safety analysis and design. Model checking can be employed to perform safety analysis, identify potential hazards, and prove the correctness of complex systems. However, many types of construction models are expressed in different ways, and there exists no unified model. Thus, the integration of model checking with system modeling language is proposed herein to analyze the safety of complex systems. System modeling language (SysML) is introduced to establish a unified system model that can describe a hybrid system of hardware and software but cannot be applied directly to safety analysis. Therefore, the semi-formal model SysML is transformed into the formal model new symbolic model checker/verifier, and the transformation rules are defined. The proposed unified model can not only help designers and safety and software engineers to execute various tasks but also efficiently, completely, and accurately analyze and verify the safety of complex systems. Finally, an integrated modular avionics case is presented to illustrate how to analyze the safety of complex systems. The results of the case study show that the proposed method can help increase the efficiency of safety analysis work and improve system safety.

Keywords

• Complex system
• safety analysis
• model checking
• system modeling language (SysML)
• integrated modular avionics (IMA)
• potential hazard