@leonardo

Model Checking UML State Machines and Collaborations

, , and . Electronic Notes in Theoretical Computer Science, 55 (3): 357--369 (October 2001)
DOI: 10.1016/S1571-0661(04)00262-2

Abstract

The Unified Modeling Language provides two complementary notations, state machines and collaborations, for the specification of dynamic system behavior. We describe a prototype tool, HUGO, that is designed to automatically verify whether the interactions expressed by a collaboration can indeed be realized by a set of state machines. We compile state machines into a PROMELA model and collaborations into sets of Büchi automata ("never claims"). The model checker SPIN is called upon to verify the model against the automata.

Links and resources

Tags