Formal Analysis of Scenario Aggregation

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 UML Sequence Diagram permit various types of control flow among messages (e.g., interleaving and iteration) to express an aggregation of multiple scenarios encompassing very complex and concurrent behaviors. Understanding the behavior of such Sequence Diagrams can be difficult, particularly if the Combined Fragments have semi-formal semantics. We introduce an approach to formalize the semantics of Sequence Diagrams with Combined Fragments in terms of both NuSMV models and Linear Temporal Logic formulas. These two formalizations enable us to leverage the analytical powers of model checking to automatically determine if a collection of Sequence Diagrams is consistent, safe, and adheres to user-supplied properties. Our work increases the accessibility of formal verification techniques to practitioners, allowing them to remain focused in the realm of scenario-based, intuitive specifications.