Research On Probabilistic Verification Of SysML Activity Diagram For Safety-critical Embedded System

Embedded systems are widely used in safety-critical areas such as aerospace, transportation, and nuclear energy. Catastrophic accidents caused by system failures always tend to be irreparable. Therefore, the safety and reliability of embedded systems has become a key problem both in industry and research. Sys ML is a system modeling language for embedded system based on UML 2.0. Sys ML activity diagram extended probability attribute is suitable for system behavior modeling. Probabilistic model checking is a probabilistic verification method based on model checking technology, which can give a comprehensive description and verification of the systems’ random feature, time feature and spatial feature.In this thesis, we integrate the Sys ML activity diagram into probabilistic model checking. In order to give a formal description and verification of system probabilistic event and environment uncertainty. We propose a probabilistic verification method based on Sys ML activity diagram. The main contents of this paper include:(1) We build the probabilistic model of the Sys ML activity diagram based on the Markov decision process(MDP). Firstly, we give a decomposition algorithm of the nested activity diagram. Then, MDP expressions, which can be used to express basic modeling elements are defined to describe the state transition of activity diagram. Finally, An algorithm is designed to transform activity diagram to MDP expressions, which realize the automatic construction of Sys ML activity diagram probabilistic model.(2) We use the model checker PRISM to analysis and verify the activity diagram probabilistic model. Firstly, we give the conversion rules from MDP expressions to PRISM codes, which transform the activity diagram probabilistic model to PRISM. Then, we use probabilistic tree logic(PCTL) to describe system safety properties. Finally, both of the model and properties are imported into PRISM for safety verification and analysis.(3) We design a model transformation tool SAD2 PRISM, and use the tool to give a case study of a safety-critical aircraft landing gear system. Firstly, we introduce the system design and implementation of SAD2 PRISM. Then, we use SAD2 PRISM to build probabilistic model of landing gear systems’ activity diagram. Finally, The PRISM is used to verify landing gear system model’s property specifications. We find problems and make improvements to ensure the reliability and safety of the system.