Model Checking UML State Machines and Collaborations

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.

Reference

Workshop on Software Model Checking, ENTCS 55(3), 2001 BibTeX reference

Download

Paper (PDF)

Further Information

Project homepage