UPPAAL-Based Model Structure Transformation Algorithm from STM to TA
Zhanjun Huang, Yiming Wang, Wenzhuo Shang, Jianing Yan, An Zhang · 2023
Transforming semi-formal models with intuitive features into formal models with strict system behavior descriptions can effectively improve system development efficiency. This paper analyzes the characteristics and differences of the SysML state machine diagram (STM) model and the Timed Automata (TA) model. A corresponding conversion algorithm is proposed for the typical composite state structure of the SysML STM. Firstly, the internal structure of the composite state is represented by constructing a new TA template. Secondly, composite state self-transfers and internal transfers are added to represent the dynamic system behavior. Lastly, additional triggering conditions, enabling transfer conditions, and correspondences are added. An example is analyzed to realize structural conversion to the TA model. Finally, based on Bi-simulation, the correctness of the model before and after conversion is analyzed.