A formal framework for analyzing sequence diagram

Graphical representations of scenarios, such as UML Sequence Diagrams, 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 Sequence Diagram permit different types of control flows, including interleaving, alternative, and loop, for representing complex and concurrent behaviors. These fragments increase a Sequence Diagram's expressiveness, yet introduce a challenge to comprehend what behavior is possible in the traces that express system executions. Furthermore, software practitioners tend to use a collection of Sequence Diagrams to express multiple usages of a software system. It can be extremely difficult to determine manually that multiple Sequence Diagrams constitute a consistent, correct specification. This dissertation introduces an approach to codify the semantics of Sequence Diagrams with Combined Fragments in terms of Linear Temporal Logic (LTL) templates. In each template, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the semantics of all the Combined Fragments. In addition, we develop an approach to transform Sequence Diagrams with Combined Fragments into the input language of model checker NuSMV. The analytical powers of model checking can be leveraged to automatically determine if a collection of Sequence Diagrams is consistent. Another benefit of this approach is the ability to specify certain safety properties of a system as intuitive Sequence Diagrams. We have developed tools to translate Sequence Diagrams to both LTL and NuSMV's input language to demonstrate that they can be automatically verified. We validate our techniques by analyzing two design examples taken from an insurance industry software application. We also model Health Insurance Portability and Accountability Act of 1996 (HIPAA) Privacy Rule using Sequence Diagrams to show that high-level policies can be described using Sequence Diagrams.