Modular design

Model checking

Formal verification

Aerospace engineering

Consistency (knowledge bases)

Correctness

Software engineering

Engineering

Visual arts

Avionics

Unified Modeling Language

Artificial intelligence

Life-critical system

Systems Modeling Language

Modeling language

Integrated modular avionics

Programming language

Viewpoints

Software

Model transformation

Computer science

Complex system

Formal methods

IEEE Access

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.

Integrating Model Checking With SysML in Complex System Safety Analysis