Semantics of the interaction overview diagram

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to illustrate the approach.