SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems

Abstract

Safety-critical cyber-physical systems (SC-CPS) have the characteristics of distributed, heterogeneous, strong coupling of computing resources and physical resources. With the increased acceptance of Model-Driven Development (MDD) in the safety-critical domain, the SysML language has been broadly used. Increasing complexity results in the formal verification of the SysML models of SC-CPS often faces the so-called state-explosion problem. Moreover, safety analysis is also an important step to ensure the quality of SC-CPS. Thus, this article proposes an integrated SysML modelling and verification approach to cover specification of nominal behaviour and safety. First, an extension of SysML is presented, in which the contract information (i.e. Assume and Guarantee) is extended for SysML block diagrams and a Safety Profile is proposed to describe safety-related concepts. Second, the transformation from SysML to the compositional verification tool OCRA is given. Third, the safety analysis is achieved by translating the Safety Profile model into FTA (Fault Tree Analysis). Finally, the prototype tools including SysML2OCRA and SafetyProfile2FTA are represented, and the effectiveness of the method proposed in this paper is verified through actual industrial cases.

Keywords:

• Cyber-physical systems
• SysML
• compositional verification
• safety analysis
• OCRA

Disclosure statement

No potential conflict of interest was reported by the author(s).

Notes

1 The i is the number of flat roots at the orbit angle, Ω is the number of flat roots at the ascending node equinox, and μ denotes the orbit amplitude angle.

Additional information

Funding

This work was supported by the National Natural Science Foundation of China [grant number 62072233 and 61772270], Aeronautical Science Foundation of China [grant number 201919052002] and National Key Research and Development Program [grant number 2018YFB1003900] .