College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Jiangsu, China.

---

Abstract—Safety verification of real-time embedded systems is a complex and hot issue. This paper proposes a SysML/MARTE activity diagram (SMAD), which is extended from SysML activity diagram (SAD) with non-functional MARTE semantics, for the describing of the real-time embedded systems behaviors. To carry out the safety verification, we transform the SMAD into timed automata. The processes of the model transformation and formal verification are as follows: first, building the meta-models of SMAD and timed automata, which are based on MDE; second, achieving the semantic and structures mapping, which can complete the model transformation; third, input the CTL specification into model checker UPPAAL for the verification. Finally, we construct an instance to illustrate the validity of the approach.

Index Terms—Safety verification, SysML activity diagram, MARTE, model transformation.

[PDF]

Cite: Chuanlin Huang, Zhiqiu Huang, Jun Hu, Zhipeng Wu, Siqi Wang, "A MDE-Based Approach to the Safety Verification of Extended SysML Activity Diagram," Journal of Software vol. 10, no. 1, pp. 56-70, 2015.