@article {325, title = {Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker}, journal = {FORMAL ASPECTS OF COMPUTING}, volume = {11}, year = {1999}, month = {1999}, pages = {637 - 664}, isbn = {0934-5043}, url = {http://mycite.omikk.bme.hu/doc/16328.pdf}, author = {Diego Latella and Istv{\'a}n Majzik and Mieke Massink} }