On CPN-based verification of hierarchical formalization of UML 2 Interaction Overview Diagrams

Unified Modeling Language (UML) is a graphical modeling language based on diagrams is widely used both in industry and academia although its semantics is yet informal. In this work, we aim to give a formal semantics description of Interaction Overview Diagram (IOD) semantics. IOD as new diagram introduced by UML2 allows a hierarchical specification of system´s behavior at more than one level. We establish a mapping of the hierarchical use of IODs and of timing diagrams into respectively hierarchical colored Petri nets (HCPNs) and timed colored Petri nets (TCPNs). The objective of this formal description is to assist designers in the use of abstraction as well as refinement while keeping verification possible. Finally, we compare our approach with others similar existing in the literature.