TY - GEN
T1 - UPPAAL-Based Model Structure Transformation Algorithm from STM to TA
AU - Huang, Zhanjun
AU - Wang, Yiming
AU - Shang, Wenzhuo
AU - Yan, Jianing
AU - Zhang, An
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - Bi-simulation
KW - Model Transformation
KW - Model Validation
KW - SysML
KW - TA
UR - http://www.scopus.com/inward/record.url?scp=85187961895&partnerID=8YFLogxK
U2 - 10.1109/ICEI60179.2023.00072
DO - 10.1109/ICEI60179.2023.00072
M3 - 会议稿件
AN - SCOPUS:85187961895
T3 - Proceedings - 2023 IEEE International Conference on Energy Internet, ICEI 2023
SP - 346
EP - 350
BT - Proceedings - 2023 IEEE International Conference on Energy Internet, ICEI 2023
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 7th IEEE International Conference on Energy Internet, ICEI 2023
Y2 - 20 October 2023 through 22 October 2023
ER -