FORMAL VERIFICATION OF DYNAMIC UML DIAGRAMS USING TLA+

摘要

Coping with the verification of dynamic UML diagrams implies use of the semantics of these diagrams. In this research domain, it possible to rest with the UML metamodel which is defined as text in natural language. Using natural language leads to some imprecisions in the semantics. To prevent this weakness, it is better to define the semantics formally. Our work has consisted in expressing a significant 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 specified 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.