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,