Model Checking Combined Fragments of Sequence Diagrams

Abstract

Graphical representations of scenarios using the Combined Fragments of UML Sequence Diagrams, serve as a well-accepted means for expressing an aggregation of multiple traces encompassing complex and concurrent behaviors. However, Combined Fragments increase the difficulty of analysis of scenarios. This paper introduces an approach to formally verify all the Combined Fragments, and nested Combined Fragments using model checking. © Springer-Verlag Berlin Heidelberg 2013.