PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Latella D., Massink M. Model checking UML statechart diagrams using Jack. In: 4th IEEE International Symposium on High-Assurance Systems Engineering. Proceedings (Washington, USA, November 17-19, 1999), 46-55. IEEE Computer Society, 1999.. 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 branching time model-checking approach to the automatic verification of formal correctness of UML Statechart Diagrams specifications. We use a formal operational semantics for building a labeled transition system (automaton) which is then used as a model to be checked against correctness requirements expressed in the action based temporal logics 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.
Subject UML statechart diagrams


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