We propose a methodology for system specification and verification based on UML diagrams and interpreted in terms of graphs and graph transformations. Once a system is modeled in this framework, a temporal graph logic can be used to express some of its relevant behavioral properties. Then, under certain constraints, such properties can be checked automatically. The approach is illustrated over a simple case study, the so-called Airport Case Study, which has been widely used along the first two years of the AGILE GC project.

Specifying and verifying UML activity diagrams via graph transformations

CORRADINI, ANDREA;GADDUCCI, FABIO
2004-01-01

Abstract

We propose a methodology for system specification and verification based on UML diagrams and interpreted in terms of graphs and graph transformations. Once a system is modeled in this framework, a temporal graph logic can be used to express some of its relevant behavioral properties. Then, under certain constraints, such properties can be checked automatically. The approach is illustrated over a simple case study, the so-called Airport Case Study, which has been widely used along the first two years of the AGILE GC project.
2004
Baldan, Paolo; Corradini, Andrea; Gadducci, Fabio
File in questo prodotto:
File Dimensione Formato  
gc2004.pdf

solo utenti autorizzati

Tipologia: Versione finale editoriale
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 218.37 kB
Formato Adobe PDF
218.37 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/84930
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 11
social impact