A MDE-Based Approach to the Safety Verification of Extended SysML Activity Diagram
Chuanlin Huang, Zhiqiu Huang, Jun Hu, WU Zhi-peng, Siqi Wang · Journal of Software · 2015
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.