Table of contents:

UML, the de-facto standard for object-oriented modeling, currently still lacks a rigorously defined semantics for its models. This makes formal analysis and verification of model properties extremely difficult. OCL, the Object Constraint Language is part of UML for the expression of system properties. To validate formally these properties, we first present a technique for transforming a UML object life cycle model into Object Petri nets. We are especially interested in the modeling of communicating systems and for this purpose we use the state machines as models of the object behaviour. Secondly, we resort to the object and sequence diagrams which provide respectively identified objects and events for initializing the Petri nets derived from the state machines. Thirdly, validation of OCL invariants which are translated into temporal logic properties to be checked on the Petri nets derived from the UML models, requires integration of object flows within the state machines. These object flows express the dynamic creation and deletion of objects in the class association ends. Our interest in the association ends is motivated by the fact that they constitute the most important constructs of OCL expressions. A case study is provided throughout the paper to illustrate the methodology.

[ download PDF ]