Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach

Fayçal Guerrouf; Samir Tigane

doi:10.35377/saucis...1872608

Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach

Abstract

The Unified Modeling Language (UML) is a widely adopted standard for visualizing, specifying, constructing, and documenting software system artifacts. It enables developers to design diagrams that effectively represent complex relationships and processes. Despite its versatility, UML lacks the formal notation necessary for rigorous analysis and verification. % To address this limitation, we propose an approach for transforming Statechart Diagrams (STD), a type of UML behavioral diagram, into Generalized Stochastic Petri Nets (GSPN). GSPNs provide a well-established framework for representing and analyzing concurrency, timing, synchronization, precedence, and priority in processes. Using the meta-modeling tool AToM3, we create meta-models for both STDs and GSPNs. Additionally, a graph grammar is developed to facilitate automatic transformation. This approach enables the creation of a tool for modeling and verifying Statechart diagrams. The proposed method is validated through a case study involving an automatic gearbox system with six states and multiple transitions. The transformation successfully handled models of moderate complexity (up to 20 states and 30 transitions). It enabled verification in under 5 seconds using the PIPE tool, detecting potential design flaws such as deadlocks and unsafe states.

Keywords

References

B. Rumpe, Modeling with UML. Springer, 2016, vol. 98. [Online]. Available: https://doi.org/10.1007/978-3-319-33933-7
O. Group et al., “Unified modeling language,” http://www.uml.org, 2001.
T. Murata, “Petri nets: Properties, analysis and applications,” Proceedings of the IEEE, vol. 77, no. 4, pp. 541–580, 1989. [Online]. Available: https://doi.org/10.1109/5.24143
M. A. Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, “Modeling with generalized stochastic petri nets,” ACM SIGMETRICS Performance Evaluation Review, vol. 26, no. 2, p. 2, 1998. [Online]. Available: https://doi.org/10.1145/288197.581193
E. Guerra and J. de Lara, “A framework for the verification of UML models: examples using petri nets,” in JISBD, vol. 2003, 2003, pp. 325–334.
N. J. Dingle, W. J. Knottenbelt, and T. Suto, “Pipe2: a tool for the performance evaluation of generalized stochastic petri nets,” ACM SIGMETRICS Performance Evaluation Review, vol. 36, no. 4, pp. 34–39, 2009. [Online]. Available: https://doi.org/10.1145/1530873.1530881
E. André, S. Liu, Y. Liu, C. Choppy, J. Sun, and J. S. Dong, “Formalizing UML state machines for automated verification – a survey,” ACM Comput. Surv., vol. 55, no. 13s, Jul. 2023. [Online]. Available: https://doi.org/10.1145/3579821
C. Choppy, K. Klai, and H. Zidani, “Formal verification of UML state diagrams: a petri net based approach,” ACM SIGSOFT Software Engineering Notes, vol. 36, no. 1, pp. 1–8, 2011. [Online]. Available: https://doi.org/10.1145/1921532.1921561

T. Jussila, J. Dubrovin, T. Junttila, T. Latvala, I. Porres, and J. K. U. Linz, “Model checking dynamic and hierarchical UML state machines,” Proc. MoDeV2a: Model Development, Validation and Verification, pp. 94–110, 2006.
A. Lyazidi and S. Mouline, “Formal verification of UML state machine diagrams using petri nets,” in International Conference on Networked Systems. Springer, 2019, pp. 67–74. [Online]. Available: https://doi.org/10.1007/978-3-030-31277-0_5
L. B. R. d. Santos, V. A. d. S. Júnior, and N. L. Vijaykumar, “Transformation of UML behavioral diagrams to support software model checking,” arXiv preprint arXiv:1404.0855, 2014. [Online]. Available: https://doi.org/10.48550/arXiv.1404.0855
N. Markjan, N. Tuaycharoen, and W. Vatanawood, “Formal modeling of concurrent state machine diagrams using NuSMV,” in Proceedings of the 2025 17th International Conference on Computer Modeling and Simulation, ser. ICCMS ’25. New York, NY, USA: Association for Computing Machinery, 2025, pp. 100–106. [Online]. Available: https://doi.org/10.1145/3761668.3761685
F. Peres and M. Ghazel, “A proven translation from a UML state machine subset to timed automata,” ACM Trans. Embed. Comput. Syst., vol. 23, no. 5, Aug. 2024. [Online]. Available: https://doi.org/10.1145/3581771
S. Doostali, S. M. Babamir, and M. Javani, “Using a process algebra interface for verification and validation of UML statecharts,” Computer Standards & Interfaces, vol. 86, p. 103739, 2023. [Online]. Available: https://doi.org/10.1016/j.csi.2023.103739
G. Bazydło, “Designing reconfigurable cyber-physical systems using unified modeling language,” Energies, vol. 16, no. 3, 2023. [Online]. Available: https://doi.org/10.3390/en16031273
Y. Zhao, Y. Fan, X. Bai, Y. Wang, H. Cai, and W. Ding, “Towards formal verification of UML diagrams based on graph transformation,” in IEEE International Conference on E-Commerce Technology for Dynamic E-Business. IEEE, 2004, pp. 180–187. [Online]. Available: https://doi.org/10.1109/CEC-EAST.2004.70
F. Guerrouf, A. Chaoui, and A. Aldahoud, “A graph transformation approach of mobile activity diagram to nested petri nets,” International Journal of Computer Aided Engineering and Technology, vol. 5, no. 1, pp. 44–57, 2012. [Online]. Available: https://doi.org/10.1504/IJCAET.2013.050549
P. Baldan, A. Corradini, and F. Gadducci, “Specifying and verifying UML activity diagrams via graph transformation,” in Global Computing: IST/FET International Workshop, GC 2004 Rovereto, Italy, March 9–12, 2004 Revised Selected Papers. Springer, 2005, pp. 18–33. [Online]. Available: https://doi.org/10.1007/978-3-540-31794-4_2
S. Tigane, F. Guerrouf, and L. Kahloul, “A GSPN-based formalism under infinite-server semantics for reconfigurable WANETs,” Computing, vol. 105, no. 10, pp. 2263–2291, 2023. [Online]. Available: https://doi.org/10.1007/s00607-023-01183-9
J. de Lara and H. Vangheluwe, “AToM3: A tool for multi-formalism and meta-modelling,” in Fundamental Approaches to Software Engineering: 5th International Conference, FASE 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8–12, 2002 Proceedings 5. Springer, 2002, pp. 174–188. [Online]. Available: https://doi.org/10.1007/3-540-45923-5_12
M. Andries, G. Engels, A. Habel, B. Hoffmann, H.-J. Kreowski, S. Kuske, D. Plump, A. Schürr, and G. Taentzer, “Graph transformation for specification and programming,” Science of Computer Programming, vol. 34, no. 1, pp. 1–54, 1999. [Online]. Available: https://doi.org/10.1016/S0167-6423(98)00023-9

Details

Primary Language

English

Subjects

Computer Software, Software Testing, Verification and Validation

Journal Section

Research Article

Authors

Fayçal Guerrouf ^*
0000-0001-6917-8032
Algeria

Samir Tigane
0000-0001-9093-1180
Algeria

Early Pub Date

June 22, 2026

Publication Date

June 30, 2026

Submission Date

January 27, 2026

Acceptance Date

April 24, 2026

Published in Issue

Year 2026 Volume: 9 Number: 3

DOI

https://doi.org/10.35377/saucis...1872608

IZ

https://izlik.org/JA49DA94KR

Cite

RIS / Bibtex

APA

Guerrouf, F., & Tigane, S. (2026). Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach. Sakarya University Journal of Computer and Information Sciences, 9(3), 790-805. https://doi.org/10.35377/saucis...1872608

AMA

1.Guerrouf F, Tigane S. Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach. SAUCIS. 2026;9(3):790-805. doi:10.35377/saucis.1872608

Chicago

Guerrouf, Fayçal, and Samir Tigane. 2026. “Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach”. Sakarya University Journal of Computer and Information Sciences 9 (3): 790-805. https://doi.org/10.35377/saucis. 1872608.

EndNote

Guerrouf F, Tigane S (June 1, 2026) Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach. Sakarya University Journal of Computer and Information Sciences 9 3 790–805.

IEEE

[1]F. Guerrouf and S. Tigane, “Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach”, SAUCIS, vol. 9, no. 3, pp. 790–805, June 2026, doi: 10.35377/saucis...1872608.

ISNAD

Guerrouf, Fayçal - Tigane, Samir. “Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach”. Sakarya University Journal of Computer and Information Sciences 9/3 (June 1, 2026): 790-805. https://doi.org/10.35377/saucis. 1872608.

JAMA

1.Guerrouf F, Tigane S. Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach. SAUCIS. 2026;9:790–805.

MLA

Guerrouf, Fayçal, and Samir Tigane. “Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach”. Sakarya University Journal of Computer and Information Sciences, vol. 9, no. 3, June 2026, pp. 790-05, doi:10.35377/saucis. 1872608.

Vancouver

1.Fayçal Guerrouf, Samir Tigane. Formal Verification of UML Statechart Diagrams via Graph Transformation to Generalized Stochastic Petri Nets: A Meta-Modeling Approach. SAUCIS. 2026 Jun. 1;9(3):790-805. doi:10.35377/saucis. 1872608