SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems
Connection science(2021)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要