Abstract
The UML 2.0 integrates a dialect of High-Level Message Sequence Charts (HMSCs) for interaction modelling. We describe a translation of UML 2.0 interactions into automata for model checking whether an interaction can be satisfied by a given set of message exchanging UML state machines. The translation supports basic interactions, state invariants, strict and weak sequencing, alternatives, ignores, and loops as well as forbidden interaction fragments. The translation is integrated into the UML model checking tool HUGO/RT. © Springer-Verlag Berlin Heidelberg 2007.
Author supplied keywords
Cite
CITATION STYLE
Knapp, A., & Wuttke, J. (2007). Model checking of UML 2.0 interactions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4364 LNCS, pp. 42–51). Springer Verlag. https://doi.org/10.1007/978-3-540-69489-2_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
