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.
Automatic verification of UML statechart diagrams using the SPIN model-checher
Latella D;Massink M
1999
Abstract
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_407907-doc_143041.pdf
accesso aperto
Descrizione: Automatic verification of UML statechart diagrams using the SPIN model-checher
Dimensione
1.39 MB
Formato
Adobe PDF
|
1.39 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
