Research On Model-driven System Safety Modeling And Verification Method

With the increasingly complex structure and interaction of embedded systems and the increasing proportion of software in embedded systems,how to ensure the high safety and reliability of complex embedded systems has gradually become a challenge today.At present,traditional system safety analysis methods such as Failure Mode and Effects Analysis(FMEA),Fault Tree Analysis(FTA),and Reliability Block Diagram(RBD)have been widely used in academia and industry.However,in the face of the development trend of highly integrated,complex,and software-intensive systems,the traditional system safety analysis process is often difficult to deal with.In the conventional safety analysis process,safety engineers usually use independent tools to manually extract information from the system model.The whole process is timeconsuming and error-prone,which affects the efficiency and accuracy of safety analysis.Safety model and system model are independent of each other,making it difficult to maintain consistency and continuity.In terms of the current problems,this paper proposes a model driven system safety modeling and verification method to complete the modeling of system safety and the automatic generation and verification of safety analysis files.The main research process of this article is as follows:(1)Safety modeling.Aiming at the problem that the SysML system modeling language can not express safety,this paper proposes a safety extension safe profile based on SysML language,which can describe the safety requirements,hazards,module fault status and fault propagation information,and then use the extension of safe profile to model the system.(2)Generation and verification of model.In order to improve the efficiency and accuracy of safety analysis,this paper proposes a transformation algorithm from extended model to fault tree,and then inputs the fault tree into XFTA tool for qualitative and quantitative analysis.The results are used to optimize the system architecture or component composition;In addition,a transformation algorithm from SysML state machine model to UPPAAL timed automata model is proposed,and then the timed automata model is input into UPPAAL tool for formal verification to verify whether the system behavior meets the safety requirements.(3)Tool integration and case analysis.A model transformation tool is designed and implemented to realize the automatic generation of fault tree and the automatic transformation from SysML state machine model to timed automata model.Taking automobile adaptive cruise system as an example,the tool is used for case analysis to prove the feasibility of the method.