PUMA
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.
 
 
Abstract
(English)
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