Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Majzik I., Massink M. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. In: Formal Aspects of Computing, vol. 11 (6) pp. 637 - 664. Springer, 1999.
Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Uni ed 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 re nement - into PROMELA, the speci cation language of the SPIN model checker. SPIN is one of the most advanced analysis and veri cation tools available nowadays. Our translation allows for the automatic veri cation of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.
Subject UML
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional