M. Couzinier and L. Féraud (France)
Object Oriented Analysis, Modeling Languages, UML, Verification
Coping with the verification of dynamic UML diagrams implies use of the semantics of these diagrams. In this re search domain, it possible to rest with the UML metamodel which is defined as text in natural language. Using natu ral language leads to some imprecisions in the semantics. To prevent this weakness, it is better to define the seman tics formally. Our work has consisted in expressing a sig nificant part of the semantics of dynamic diagrams first in Object-Z then in TLA+. In this paper, we present a formal approach of dynamic UML diagrams based on the TLA+ formal language of Lamport. This language is an extension of the linear time logic of actions, it allows the expression of safety, liveness, and fairness properties over the speci fied diagrams. The main advantage of this language is its Model Checker, TLC, that enables us to check the temporal properties which specify the system behavior.
Important Links:
Go Back
