Abstract:

In recent years the model based safety analysis and verification method for embedded systems is an important research hotspot in the field of safety critical systems engineering. We put forward a system safety verification method based on the model driven architecture, which is SysML/MARTE state machine oriented, including the construction of both the state machine metamodel which has SysML/MARTE extension semantics, and the GTS metamodel which is the semantic model of AltaRica (ie.safety modeling and analysis language). We then establish semantic mapping model transformation rules from a SysML/MARTE state machine model to the timed automata model and to the AltaRica model respectively. Thirdly, based on the platform of the AMMA and the timed automata verification tools UPPAAL we design and realize the model transformation of the SysML/MARTE state machine and the framework for system safety formal verification. Finally a safety verification example about aircraft landing control system design model is analyzed.

Key words: system safety analysis；model-driven engineering；SysML/MARTE；state machine model；embedded system