Formalization of UML object dynamics and behavior

UML has emerged as the industry standard for object-oriented modeling. However, it still lacks a well-defined semantic base enabling it to perform formal verification tasks. Our goal is to provide system designers a life cycle of software development integrating the UML user-friendliness and the Petri nets rigor and reliability. For this purpose, we propose a methodology to specify using UML and then to systematically verify and validate by way of the Petri nets. This methodology is based on a technique which derives colored Petri nets from UML object, statechart, collaboration and sequence diagrams. The proposed approach associates the formalization of the dynamics and the behavior of objects identified by identities and attribute values. A case study is provided to illustrate this technique.