Formalization and Verification of Hierarchical Use of Interaction Overview Diagrams Using Timing Diagrams
This work addresses the need for formal verification in UML modeling for software designers, though it is incremental as it builds on existing formalization efforts.
The paper tackles the problem of UML2's informal semantics by formalizing the hierarchical use of Interaction Overview Diagrams and mapping them, along with Sequence and Timing Diagrams, into Hierarchical Colored Petri Nets using Timed colored Petri Nets, which reduces verification complexity by enabling abstraction and refinement at multiple hierarchical levels.
Thanks to its graphical notation and simplicity, Unified Modeling Language (UML) is a de facto standard and a widespread language used in both industry and academia, despite the fact that its semantics is still informal. The Interaction Overview Diagram (IOD) is introduced in UML2; it allows the specification of the behavior in the hierarchical way. This paper is a contribution towards a formal dynamic semantics of UML2. We start by formalizing the Hierarchical use of IOD. Afterward, we complete the mapping of IOD, Sequence Diagrams and Timing Diagrams into Hierarchical Colored Petri Nets (HCPNs) using the Timed colored Petri Nets (timed CP-net). Our approach helps designers to get benefits from abstraction as well as refinement at more than two levels of hierarchy which reduces verification complexity.