The association ends at the basis of a formal validation

The object constraint language OCL is an extension of the UML notation for the expression of restrictions over the static and dynamic diagrams. We propose to take advantage of its formal capabilities for validating whether the UML model matches with the system properties. For this purpose, we develop an approach based on Petri nets and temporal logics. This approach allows the non trivial integration of the temporal logic properties translated from the OCL invariants with the Petri nets obtained from the UML modeling. A case study is given throughout the paper to illustrate the approach