Flexible Modular Formalization of UML Sequence Diagrams

UML Sequence Diagrams are one of the most commonly used type of UML diagrams in practice. Their semantics is often considered to be straightforward, but a more detailed analysis reveals diverse interpretations. These different choices must be properly supported by verification tools. This paper describes a formal framework for capturing semantic choices in a precise and modular way. The user is then able to select the semantics of interest, mix different interpretations, and analyze diagrams according to the chosen solution. This solution is supported by Corretto, our UML verification environment, to allow the user to play with different semantics and prove properties on Sequence Diagrams, accordingly.