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.
%0 Journal Article
%1 schafer_01_model
%A Schäfer, Timm
%A Knapp, Alexander
%A Merz, Stephan
%B Workshop on Software Model Checking (in connection with CAV '01)
%D 2001
%J Electronic Notes in Theoretical Computer Science
%K statecharts model_checking uml 2001
%N 3
%P 357--369
%R 10.1016/S1571-0661(04)00262-2
%T Model Checking UML State Machines and Collaborations
%U http://dx.doi.org/10.1016/S1571-0661(04)00262-2
%V 55
%X 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.
@article{schafer_01_model,
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"{u}chi automata ("never claims"). The model checker SPIN is called upon to verify the model against the automata.},
added-at = {2009-02-12T11:44:04.000+0100},
author = {Sch"{a}fer, Timm and Knapp, Alexander and Merz, Stephan},
biburl = {https://www.bibsonomy.org/bibtex/2597d6a67a04bb17f236f8e7d6668bbe0/leonardo},
booktitle = {Workshop on Software Model Checking (in connection with CAV '01)},
citeulike-article-id = {578810},
doi = {10.1016/S1571-0661(04)00262-2},
interhash = {543b6066e404eec02f2ad251733b3726},
intrahash = {597d6a67a04bb17f236f8e7d6668bbe0},
journal = {Electronic Notes in Theoretical Computer Science},
keywords = {statecharts model_checking uml 2001},
month = {October},
number = 3,
pages = {357--369},
posted-at = {2008-12-13 12:02:16},
priority = {2},
timestamp = {2009-02-12T11:44:04.000+0100},
title = {Model Checking UML State Machines and Collaborations},
url = {http://dx.doi.org/10.1016/S1571-0661(04)00262-2},
volume = 55,
year = 2001
}