Specifying and Verifying UML Activity Diagrams via Graph Transformation"

Paolo Baldan ⁽¹⁾ - Andrea Corradini⁽²⁾ - Fabio Gadducci⁽²⁾

⁽¹⁾ Dipartimento di Informatica, Università Ca' Foscari di Venezia, Italia.
⁽²⁾ Dipartimento di Informatica, Università di Pisa, Italia.

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.