A Tool for Transforming SysML State Machine into Uppaal Automatically

Shaopeng Wang, Jianqi Shi*, Yanhong Huang, Yang Yang

*Corresponding author for this work

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

2 Scopus citations

Abstract

SysML state machine (SysML-STM) is a modeling tool used in the Systems Modeling Language (SysML) to describe the behavior of a system. It is widely used in model-driven development (MDD). Formal methods are mathematical techniques to ensure the correctness, reliability and safety of software systems and hardware designs. In this paper, we introduce formal methods into MDD by transforming a SysML-STM model into a Uppaal timed automata. By formally verifying the system at an early stage of the development life-cycle, we aim to enhance the system's robustness. We design the mapping rules between the two models and have developed a tool, STMTU, to transform them directly. Our tool effectively leverage the benefits of formal verification techniques to ensure the correctness and reliability of the system. And the direct transformation of these models not only reduces the learning cost for developers but also helps to promote the wider adoption of formal methods.

Original languageEnglish
Title of host publication2023 IEEE International Conference on Systems, Man, and Cybernetics
Subtitle of host publicationImproving the Quality of Life, SMC 2023 - Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages2471-2476
Number of pages6
ISBN (Electronic)9798350337020
DOIs
StatePublished - 2023
Event2023 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2023 - Hybrid, Honolulu, United States
Duration: 1 Oct 20234 Oct 2023

Publication series

NameConference Proceedings - IEEE International Conference on Systems, Man and Cybernetics
ISSN (Print)1062-922X

Conference

Conference2023 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2023
Country/TerritoryUnited States
CityHybrid, Honolulu
Period1/10/234/10/23

Keywords

  • ATL
  • Formal Methods
  • Model Transformation
  • State Machine
  • SysML
  • Timed Automata
  • Uppaal

Fingerprint

Dive into the research topics of 'A Tool for Transforming SysML State Machine into Uppaal Automatically'. Together they form a unique fingerprint.

Cite this