PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Majzik I., Massink M. Automatic verification of UML statechart diagrams using the SPIN model-checher. Internal note CNUCE-B4-99-008, 1999.
 
 
Abstract
(English)
Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modeling Language (UML]. In this paper we present a translation from UML Statechart Diagrams 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.
Subject Graphical modeling language
UML
C.3 Special-purpose and application based-systems


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