Statechart diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper, we present a branching-time model-checking approach to the automatic verification of the formal correctness of UML Statechart diagram specifications. We use a formal operational semantics for building a labelled transition system (automaton) which is then used as a model to be checked against correctness requirements expressed in Action-Based Temporal Logic (ACTL). Our reference verification environment is JACK, where automata are represented in a standard format, which facilitates the use of different tools for automatic verification
Model checking UML statechart diagrams using JACK
Gnesi S;Latella D;Massink M
1999
Abstract
Statechart diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper, we present a branching-time model-checking approach to the automatic verification of the formal correctness of UML Statechart diagram specifications. We use a formal operational semantics for building a labelled transition system (automaton) which is then used as a model to be checked against correctness requirements expressed in Action-Based Temporal Logic (ACTL). Our reference verification environment is JACK, where automata are represented in a standard format, which facilitates the use of different tools for automatic verificationFile | Dimensione | Formato | |
---|---|---|---|
prod_190553-doc_55688.pdf
solo utenti autorizzati
Descrizione: Model checking UML statechart diagrams using JACK
Tipologia:
Versione Editoriale (PDF)
Dimensione
2.35 MB
Formato
Adobe PDF
|
2.35 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.