UPPAAL-Based Model Structure Transformation Algorithm from STM to TA

Zhanjun Huang, Yiming Wang, Wenzhuo Shang, Jianing Yan, An Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2023 IEEE International Conference on Energy Internet, ICEI 2023
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages346-350
Number of pages5
ISBN (Electronic)9798350386684
DOIs
StatePublished - 2023
Event7th IEEE International Conference on Energy Internet, ICEI 2023 - Shenyang, China
Duration: 20 Oct 202322 Oct 2023

Publication series

NameProceedings - 2023 IEEE International Conference on Energy Internet, ICEI 2023

Conference

Conference7th IEEE International Conference on Energy Internet, ICEI 2023
Country/TerritoryChina
CityShenyang
Period20/10/2322/10/23

Keywords

  • Bi-simulation
  • Model Transformation
  • Model Validation
  • SysML
  • TA

Fingerprint

Dive into the research topics of 'UPPAAL-Based Model Structure Transformation Algorithm from STM to TA'. Together they form a unique fingerprint.

Cite this