Research On System Safety Design Verification Methodology Based On Alta Rica Model

As the size of aviation,transportation,medical and other safety-critical system increasing,how to increase the safety of complex safety-critical systems to prevent crippling casualties,became an urgent problem.There is a big difference of between models of traditional modeling methods and actual system.The model can be used throughout the whole design process.Very small changes can result in the specification to loop through all the safety model,prone to consume resources.High-level modeling language AltaRica proposed solving this problem.The model of AltaRica is a component reusable hierarchy.It is an MBSA modeling language specifically designed for industrial systems safety by France industrial and academic associations.With the update of AltaRica3.0,ARC and other traditional AltaRica modeling tools are no longer supported,and SPIN as a thorough model validation tool is widely used.Due to SPIN cannot be used directly for AltaRica3.0 model analysis and validation.So,need to transform an AltaRica3.0 model into a Promela model.To solve these problems,the main work of this paper is proposing an analysis and validation method of using Simfia to create a model based on graphical modeling,converting to an AltaRica3.0 model,then converting to a Promela model,using SPIN tool to verify.Concrete works as showed below:(1)Proposed a modeling method of AltaRica3.0 based on Simfia,then created a model of display control system to analyze its fault tree.First introducd basic knowledge of AltaRica3.0 and Simfia,analyzed features between model of AltaRica3.0 and Simfia;proposed a modeling method of AltaRica3.0 based on Simfia,pointed out mapping relationship of Simfia model elements and AltaRica3.0 model elements;created a model of display control system to analyze its fault tree at last.(2)Analyzed flatting method from an AltaRica3.0 model to a GTS model,and proposed a method of transforming an AltaRica3.0 model into a Promela model.First analyzed detailed rules of flatting from an AltaRica3.0 model to a GTS model;analyzed semantics model of AltaRica3.0 and Promela;created a transition rules of AltaRica3.0 and Promela according to flatting rules and verifyied its feasibilit;Finally,illustrated the transition process using simple water system as an example.(3)Created an AltaRica3.0 model of wheel braking system and transformed it into a Promela model for analysis and validation.Created an AltaRica3.0 model of wheel braking system,and used Arbre Analyste for fault tree analysis;transformed it into a Promela model for analysis and verification by SPIN;evaluated the model by comparing the two conclusion.