A value-oriented specification for weak sequencing validation

Weak sequencing is a UML2 concept which reduces to a parallel merge when the operands are on disjunct sets of participants. This semantics needs to be well defined based on a formal language that yields the fundamentals required for a rigorous validation of the specification. In this paper, we firstly provide this semantics through a new approach to translate the UML weak sequencing Combined Fragment 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. The analysis deals with the CPNs good construction as well as their faithfulness to the real-world system. To verify that the CPN models preserve the system properties, we use OCL invariants. This use motivates our second contribution based on the association ends specification on the behavioral models. Such a modeling allows a deep exploitation of the OCL expressivity while validating the models consistency. The verification is performed on a predicate/transition net explored by model checking.