Object Petri nets marking using UML

UML semantics formalisation has aroused much interest these two last decades. Among the numerous proposed works many undertake the formalisation by translation into statetransition languages. The verification is afterwards performed by model-checking. However, one important issue raised by model checking is the state space explosion. The purpose of this paper will mainly address this issue. It is threefold. We first propose an approach to mark the derived formalisms starting from any time of the system lifecycle. The marking is drawn from the object and sequence diagrams. We secondly exploit the association ends modelled on the object diagram to retrieve the first action of each object behaviour. This contribution ensures a strong consistency when handling the object and sequence diagrams. We finally propose a method based on the association end formalisation in order to deal with the models validation. The whole of the solution is analysed by model checking.