K. Lano , J. Bicarregui , A. Evans
January 2000
Rigorous Object-Oriented Methods 2000 (ROOM)
Rigorous Object-Oriented Methods
17 January 2000
In this paper we provide a systematic formal interpretation for most elements of the UML notation. This interpretation, in a structured temporal logic, enables precise analysis of the properties of these models, and the verification of one model against another. We extend previous work by providing a structured logical interpretation for sequence diagrams, in which object communication is represented using theory morphisms. As an application of the formalisation, we show how the introduction of particular design patterns can be proved to be refinement transformations.
This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/