Formal validation with OCL

System validation allows to check whether the modeled system complies with the customer requirements. For UML modeling, these requirements can be specified by the designer as invariants using the Object Constraint Language (OCL). To validate the OCL invariants, we first propose to derive the UML dynamic models to Petri nets. The OCL invariants are after, translated to temporal logic properties in order to be checked on the derived Petri nets. To efficiently exploit all OCL capabilities in expressing invariants, we also propose an object flow specification on the dynamic models and introduce an adequate technique to translate them to Petri nets. A case study is given throughout the paper to illustrate the approach.