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.
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
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