Computer Science ›› 2019, Vol. 46 ›› Issue (11): 100-108.doi: 10.11896/jsjkx.181001850

• Information Security • Previous Articles     Next Articles

Method of System Safety Analysis and Verification for SysML Models

LI Wan-qian, HU Jun, CHEN Song, ZHANG Wei-jun   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)
  • Received:2018-10-07 Online:2019-11-15 Published:2019-11-14

Abstract: In recent years,with the increasing scale and complexity of safety-critical systems such as aviation,transportation and medical treatment,model-based system safety analysis and verification has become an important research direction in the field of safety-critical system engineering.How to analyze and verify the safety of SysML as a typical system model is a very important issue.Based on the framework of model-based safety analysis,this paper designed a safety analysis and verification method for the SysML models,which realizes the complete process from model construction to safety analysis and attribute verification.Firstly,this paper introduced SysML system architecture design model and the latest system safety modeling language AltaRica3.0 from requirement level and design level,constructed the semantic equivalence transformation rules from the core model elements of SysML to AltaRica 3.0,gave the formal description of transformation rules,analyzed and proved the transformation rules.Then,this paper designed a prototype tool platform based on the model-driven method to complete the process of automatic transformation and safety analysis of the model.The prototype tool combines the functions of transformation,compilation and generation of fault tree,fault tree analysis,stepwise simulation and dynamic demonstration of fault path.The synchronization of system design and safety analy-sis was realized.On the basis of this,the key points of transformation from AltaRica 3.0 to Promela model were given,and the attributes of the model were verified by the exhaustive model verification tool SPIN.Finally,the SysML model was established according to the architecture design description and safety requirements of the wheel brake system in 4761 standard,and the automatic conversion,safety analysis and verification of the model were realized based on the prototype tool platform and attribute verification tool,which further illustrates the effectiveness of the conversion method.

Key words: AltaRica3.0, Promela, Safety-critical system, SysML, Wheel brake system

CLC Number: 

  • TP311
[1]GOMES A,MOTA A,SAMPAIO A,et al.Systematic ModelBased Safety Assessment Via Probabilistic Model Checking[J].Lecture Notes in Computer Science,2010,6415:625-639.
[2]FRIEDENTHAL S,MOORE A,STEINER R.A practical guideto SysML:the systems modeling language[M].San Francisco:Morgan Kaufmann,2014.
[3]FRIEDENTHAL S,MOORE A,STEINER R.OMG SystemsModeling Language (OMG SysML?) Tutorial[C]∥INCOSE International Symposium.INCOSE,2008:1731-1862.
[4]MICHEL B,TATIANA P,ANTOINE R.AltaRica3.0 Language Specification[M/OL].https://www.openaltarica.fr/docs-downloads/.
[5]BIEBER P,BOUGNOL C,CASTEL C,et al.Safety Assessment with Altarica[M]∥Building the Information Society.US:Springer,2004:505-510.
[6]ERICSON C A.Fault tree analysis[C]∥System Safety Conference.Orlando,Florida,1999:1-9.
[7]INVERARDI P,MUCCINI H,PELLICCIONE P.Automatedcheck of architectural models consistency using SPIN[C]∥Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001).IEEE,2001:346-349.
[8]PROSVIRNOVA T,BATTEUX M,BRAMERET P A,et al.The altarica 3.0 project for model-based safety assessment[J].IFAC Proceedings Volumes,2013,46(22):127-132.
[9]PROSVIRNOVA T,RAUZY A.AltaRica 3.0 project:compileGuarded Transition Systems into Fault Trees[C]∥European Safety and Reliability Conference.2013.
[10]CLARKE E M,GRUMBERG O,PELED D.Model checking[M].Massachu-setts MIT Press,1999.
[11]KOVSE J,HARDER T.Generic XMI-based UML model transformations[C]∥International Conference on Object-Oriented Information Systems.Springer,Berlin,Heidelberg,2002:192-198.
[12]WANG J,HU L,CHEN S,et al.Verification of RiskA calculation engine based on Open-PSA platform[C]∥2013 International Conference on Quality,Reliability,Risk,Maintenance,and Safety Engineering (QR2MSE).IEEE,2013:32-35.
[13]INVERARDI P,MUCCINI H,PELLICCIONE P.Automatedcheck of architectural models consistency using SPIN[C]∥16th Annual International Conference on Automated Software Engineering,2001.(ASE 2001).IEEE,2001:346-349.
[14]HU J,CHEN S,WANG M M.Method oftransformation and verification from AltaRica3.0 to Promela[J].Computer Engineering &Science,2017,39(4):708-716.(in Chinese)
胡军,陈松,王明明.AltaRica3.0模型到Promela模型转换与验证方法研究[J].计算机工程与科学,2017,39(4):708-716.
[15]LUO W L,WEI O,HUANG M Y.Computing minimal cut sets of fault tree using SAT solver[J].Computer Engineering & Scien-ce,2017,39(4):725-733.(in Chinese)
罗炜麟,魏欧,黄鸣宇.基于SAT求解器的故障树最小割集求解算法[J].计算机工程与科学,2017,39(4):725-733.
[16]SAE International.Guidelines and methods for conducting thesafety assessment process on civil airborne systems and equipment[M].SAE International,1996.
[17]BOZZANO M,CIMATTI A,PIRES A F,et al.Formal design and safety analysis of AIR6110 wheel brake system[C]∥Internatio-nal Conference on Computer Aided Verification.Springer,Cham,2015:518-535.
[18]DAVID P,IDASIAK V,KRATZ F.Automating the synthesis of AltaRica Data-Flow models from SysML[C]∥Proceedings of European Safety and Reliability Conference (ESREL09).2009:105-112.
[19]BOZZANO M,CIMATTI A,LISAGOR O,et al.Safety assessment of AltaRica models via symbolic model checking[J].Science of Computer Programming,2015,98(4):464-483.
[1] WANG Wen-xuan, HU Jun, HU Jian-cheng, KANG Jie-xiang, WANG Hui, GAO Zhong-jie. Test Case Generation Method Oriented to Tabular Form Formal Requirement Model [J]. Computer Science, 2021, 48(5): 16-24.
[2] TANG Hong-ying, HU Jun, CHEN Shuo, SHI Meng-ye. System Safety Analysis Tool for SysML and Case Study [J]. Computer Science, 2020, 47(5): 284-294.
[3] XUE Yan, WU Shu-hong, WANG Yao-li. Verification of G Language System Model Based on SPIN [J]. Computer Science, 2018, 45(6A): 536-540.
[4] XU Wen-hua and ZHANG Yu-ping. Design and Implementation of Safety Analysis Tool Based on Avionics System Architecture Model [J]. Computer Science, 2016, 43(Z11): 536-541.
[5] WU Zhi-peng HUANG Zhi-qiu WANG Shan-shan CAO De-jian. Research on Framework of Safety Verification Based on Fault-extended SysML Activity Diagram [J]. Computer Science, 2015, 42(7): 222-228.
[6] WANG Fei, SHEN Guo-hua, HUANG Zhi-qiu, MA Lin, LIU Chang, LI Hai-feng and LIAO Li-li. Method Combining Linear Temporal Logic and Fault Tree for Software Safety Verification [J]. Computer Science, 2015, 42(12): 71-75.
[7] . Method for Generating Formal System Model Based on Scenarios Analysis [J]. Computer Science, 2012, 39(8): 136-140.
[8] DUAN Feng-Qin ,LI Xiang (Institute of Computer Seienee,Guizhou University,Guiyang 550025). [J]. Computer Science, 2006, 33(5): 287-289.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!