An interleaving semantics for UML 2 interactions using Petri nets

Weak sequencing is the implicit composition operator for interactions defined by the OMG specification. Accordingly, most semantics retain this operator to compose a CombinedFragment with the rest of the interactions. But all of them use only formalisms based on trace or interleaving semantics. True-concurrency-based formalisms ignore the standard interpretation and introduce synchronization on entering and exiting fragments. In this paper, we propose to revise the formal semantics of the CombinedFragments using a formalism that offers a high expressivity power to describe execution traces with regard to true concurrency as well as interleaving. We define an appropriate semantics, which is in accordance with the UML 2.4 specification regarding the event ordering over the operands and the constraints evaluation. For this purpose, we propose an approach to translate the CombinedFragments into Colored Petri Nets, or CPNs. The derived specification is value-oriented, composed of identified objects and events, thus allowing a more precise analysis of the model behavior. It is verified by model checking. A case study is given to illustrate the approach throughout the paper.