Abstract
In this paper, we present the formal semantics of sequence diagrams. The semantics of a sequence diagram is interpreted as a consecutive execution of steps in UTP. The semantics clearly captures the consistency between the design class diagram and sequence diagrams. This may underpin development of model consistency checking functions in UML CASE tools. It may also be used to reason about the correctness of design model with respect to the requirement model.