Integration of the Association Ends within
UML State Diagrams
Thouraya Bouabana-Tebibel1 and Mounira Belmesk2
1National Institute of Computer Science, INI BP 68 M Oued-Smar 16309, Algiers
2Edouard Monpetit College, longueuil, Canada
Abstract: UML currently still lacks a rigorously defined semantics for its models, which makes formally analyzing a model and verifying its properties extremely difficult. To remedy that, we first present a technique for transforming the UML statechart diagrams into Petri nets. Then we develop an approach based on the class association ends. This approach shows how to validate the system invariants, expressed in the Object Constraint Language, on the Petri nets derived from the UML models. System property validation starts with an initialization of the model, extracted from the object and sequence diagrams. A case study is given throughout the paper to illustrate the methodology.
Keywords: UML, OCL, Petri nets, temporal logics, verification.
Received March 19, 2006; accepted September 7, 2006
