A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams

Runfang Wu, Ye Du () and Meihong Li
Additional contact information
Runfang Wu: Cyberspace Security Department, School of Cyberspace Science and Technology, Beijing Jiaotong University, No. 3 Shangyuancun Haidian District, Beijing 100044, China
Ye Du: Cyberspace Security Department, School of Cyberspace Science and Technology, Beijing Jiaotong University, No. 3 Shangyuancun Haidian District, Beijing 100044, China
Meihong Li: Cyberspace Security Department, School of Cyberspace Science and Technology, Beijing Jiaotong University, No. 3 Shangyuancun Haidian District, Beijing 100044, China

Mathematics, 2025, vol. 13, issue 5, 1-31

Abstract: A model transformation method based on state refinement and semantic mapping is proposed to address the challenges of high modeling complexity and resource consumption in symbolic validation of industrial software requirements. First, a rule-based semantic mapping system is constructed through the explicit definition of element correspondence between statechart components and verification models, coupled with a composite state-level refinement strategy to structurally optimize model hierarchy. Second, an automated transformation algorithm is developed to bridge graphical modeling tools with formal verification environments, supported by quantitative evaluation metrics for mapping validity. To demonstrate its practical applicability, the methodology is systematically applied to railway infrastructure safety—specifically the railroad turnout control system—as a critical case study. The experimental implementation converts operational statecharts of turnout control logic into optimized NuSMV models. Not only did the models remain intact, but the state space was also effectively reduced through the optimization of the hierarchical structure. In the validation phase, the converted model is tested for robustness using the fault injection method, and boundary condition anomalies that are not explicitly stated in the requirement specification are successfully detected. The experimental results show that the validation model generated by this method has improved validation efficiency in the NuSMV tool, which is significantly better than the traditional conversion method.

Keywords: software model checking; formal verification; UML state diagram; model transformation (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2025
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/13/5/724/pdf (application/pdf)
https://www.mdpi.com/2227-7390/13/5/724/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:13:y:2025:i:5:p:724-:d:1598255

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().