%0 Journal Article %1 Latella1999 %A Latella, Diego %A Majzik, Istvan %A Massink, Mieke %D 1999 %I Springer London %J Formal Aspects of Computing %K model\_checking statecharts uml %N 6 %P 637--664 %R 10.1007/s001659970003 %T Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker %U http://dx.doi.org/10.1007/s001659970003 %V 11 %X Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.

@article{Latella1999, abstract = {{Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.}}, added-at = {2012-04-20T17:51:17.000+0200}, author = {Latella, Diego and Majzik, Istvan and Massink, Mieke}, biburl = {https://www.bibsonomy.org/bibtex/2095660597c3cf6bcd736f0bf69627899/georghackenberg}, citeulike-article-id = {887462}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/s001659970003}, citeulike-linkout-1 = {http://www.springerlink.com/content/r0hp11xyl6lc7w3l}, day = 21, doi = {10.1007/s001659970003}, file = {Latella1999.pdf:Latella1999.pdf:PDF}, groups = {public}, interhash = {4816c7cf46c22f88576402361592f695}, intrahash = {095660597c3cf6bcd736f0bf69627899}, issn = {0934-5043}, journal = {Formal Aspects of Computing}, keywords = {model\_checking statecharts uml}, month = {#dec#}, number = 6, pages = {637--664}, posted-at = {2010-12-14 23:55:11}, priority = {2}, publisher = {Springer London}, timestamp = {2012-04-20T17:51:17.000+0200}, title = {Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker}, url = {http://dx.doi.org/10.1007/s001659970003}, username = {georghackenberg}, volume = 11, year = 1999 }