Model Checking UML State Machines and Collaborations Export

@article{citeulike:578810, 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.}, author = {Sch\"{a}fer, Timm and Knapp, Alexander and Merz, Stephan}, booktitle = {Workshop on Software Model Checking (in connection with CAV '01)}, citeulike-article-id = {578810}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/S1571-0661(04)00262-2}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S1571066104002622}, citeulike-linkout-2 = {http://www.ingentaconnect.com/content/els/15710661/2004/00000055/00000003/art00262}, doi = {10.1016/S1571-0661(04)00262-2}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {2001, model\_checking, statecharts, uml}, month = {October}, number = {3}, pages = {357--369}, posted-at = {2008-12-13 12:02:16}, priority = {2}, title = {Model Checking UML State Machines and Collaborations}, url = {http://dx.doi.org/10.1016/S1571-0661(04)00262-2}, volume = {55}, year = {2001} }

TY - JOUR ID - citeulike:578810 L3 - citeulike-article-id:578810 N2 - 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. IS - 3 JF - Electronic Notes in Theoretical Computer Science EP - 369 TI - Model Checking UML State Machines and Collaborations VL - 55 T2 - Workshop on Software Model Checking (in connection with CAV '01) SP - 357 KW - 2001 KW - model_checking KW - statecharts KW - uml AU - Schäfer, Timm AU - Knapp, Alexander AU - Merz, Stephan PY - 2001/10// UR - http://dx.doi.org/10.1016/S1571-0661(04)00262-2 ER -