Formal Analysis of Sequence Diagram with Combined Fragments
Hui Shen, Mark Robinson, Jianwei Niu · 2012
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. To alleviate this problem, we introduce an approach to formally describe Sequence Diagrams with Combined Fragments in terms of the input language of the model checker NuSMV. This approach permits the verification of desired properties against Sequence Diagrams.