A formal semantics of UML sequence diagram

We present a formal semantics of UML sequence diagram. In abstract syntax form, a well-formed sequence diagram corresponds to an ordered hierarchical structure tree. The static semantics of a sequence diagram is to check whether it is consistent with the class diagram declaration as well as with its well-formed tree structure. Meanwhile, the dynamic semantics is defined in terms of the state transitions that are carried out by the method invocations in the diagram. When a message is executed, it must be consistent with system state, i.e., object diagram and the state diagrams of its related objects. The semantics clearly captures the consistency between sequence diagram with class diagram and state diagram. Therefore, it is useful to develop the model consistent checking functions in UML CASE tools. And it also can be used to reason about the correctness of a design model with respect to a requirement model.