Language integration for model validation

System validation allows to check whether the modeled system complies with the customer requirements. For UML modeling, these requirements can be specified as invariants using the object constraint language (OCL). OCL is an extension of the UML notation for the expression of restrictions over the diagrams. To validate OCL invariants, 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 derived from the UML 2.0 activity partitions. A case study is given throughout the paper to illustrate the approach.