Abstract: UML 2.0 sequence diagrams are suitable for describing the interaction behavior among components and subcomponents of composite component, but the semantics of UML 2. 0 sequence diagram is notprecise, this makes the description of UML 20 sequence diagram c

Key words: Temporal logic, Formal semantics, UML 2. 0, Sequence diagram, XYZ/E