SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems
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 us...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Taylor & Francis Group
2022-12-01
|
| Series: | Connection Science |
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1080/09540091.2021.2017853 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850215314409652224 |
|---|---|
| author | Jian Xie Wenan Tan Zhibin Yang Shuming Li Linquan Xing Zhiqiu Huang |
| author_facet | Jian Xie Wenan Tan Zhibin Yang Shuming Li Linquan Xing Zhiqiu Huang |
| author_sort | Jian Xie |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-8520c1749acc4e34825ccea994bf118a |
| institution | OA Journals |
| issn | 0954-0091 1360-0494 |
| language | English |
| publishDate | 2022-12-01 |
| publisher | Taylor & Francis Group |
| record_format | Article |
| series | Connection Science |
| spelling | doaj-art-8520c1749acc4e34825ccea994bf118a2025-08-20T02:08:39ZengTaylor & Francis GroupConnection Science0954-00911360-04942022-12-0134191194110.1080/09540091.2021.20178532017853SysML-based compositional verification and safety analysis for safety-critical cyber-physical systemsJian Xie0Wenan Tan1Zhibin Yang2Shuming Li3Linquan Xing4Zhiqiu Huang5College of Computer Science of Technology, Nanjing University of Aeronautics and Astronautics, NanjingCollege of Computer Science of Technology, Nanjing University of Aeronautics and Astronautics, NanjingCollege of Computer Science of Technology, Nanjing University of Aeronautics and Astronautics, NanjingCollege of Computer Science of Technology, Nanjing University of Aeronautics and Astronautics, NanjingCollege of Computer Science of Technology, Nanjing University of Aeronautics and Astronautics, NanjingCollege of Computer Science of Technology, Nanjing University of Aeronautics and Astronautics, NanjingSafety-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.http://dx.doi.org/10.1080/09540091.2021.2017853cyber-physical systemssysmlcompositional verificationsafety analysisocra |
| spellingShingle | Jian Xie Wenan Tan Zhibin Yang Shuming Li Linquan Xing Zhiqiu Huang SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems Connection Science cyber-physical systems sysml compositional verification safety analysis ocra |
| title | SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems |
| title_full | SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems |
| title_fullStr | SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems |
| title_full_unstemmed | SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems |
| title_short | SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems |
| title_sort | sysml based compositional verification and safety analysis for safety critical cyber physical systems |
| topic | cyber-physical systems sysml compositional verification safety analysis ocra |
| url | http://dx.doi.org/10.1080/09540091.2021.2017853 |
| work_keys_str_mv | AT jianxie sysmlbasedcompositionalverificationandsafetyanalysisforsafetycriticalcyberphysicalsystems AT wenantan sysmlbasedcompositionalverificationandsafetyanalysisforsafetycriticalcyberphysicalsystems AT zhibinyang sysmlbasedcompositionalverificationandsafetyanalysisforsafetycriticalcyberphysicalsystems AT shumingli sysmlbasedcompositionalverificationandsafetyanalysisforsafetycriticalcyberphysicalsystems AT linquanxing sysmlbasedcompositionalverificationandsafetyanalysisforsafetycriticalcyberphysicalsystems AT zhiqiuhuang sysmlbasedcompositionalverificationandsafetyanalysisforsafetycriticalcyberphysicalsystems |