A Logical Framework for Sequence Diagram with Combined Fragments

Graphical representations of scenarios, such as UML Sequence Diagrams and Message Sequence Charts, serve as a well-accepted means for modeling the interactions among software systems and their environment through the exchange of messages. The Combined Fragments of UML Sequence Diagram permit various types of control flow among messages (e.g., interleaving and branching) to express an aggregation of multiple traces encompassing complex and concurrent behaviors. However, Combined Fragments increase the difficulty of Sequence Diagram comprehension and analysis. This paper introduces an approach to formalizing the semantics of Sequence Diagrams with Combined Fragments in terms of Linear Temporal Logic (LTL) templates. In all the templates, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the semantics of basic Sequence Diagram, all the Combined Fragments, and nested Combined Fragments. Moreover, the formalization enables us to leverage the analytical powers of automated decision procedures for LTL formulas to determine if a collection of Sequence Diagrams is consistent, safe, and deadlock-free.