DOI: 10.35377/saucis...1872608 ISSN: 2636-8129

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

Fayçal Guerrouf, Samir Tigane
Show PDF Cite
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.

More from our Archive