This paper proposes an approach for the specification of the behavior of software components that implement data abstractions. By generalizing the approach of behavior models using graph transformation, we provide a concise specification for data abstractions that describes the relationship between the internal state, represented in a canonical form, and the observers of the component. Graph transformation also supports the generation of behavior models that are amenable to verification. To this end, we provide a translation approach into an LTL model on which we can express useful properties that can be model-checked with a SAT solver.
Using graph transformation systems to specify and verify data abstractions / L. Baresi, C. Ghezzi, A. Mocci, M. Monga. - In: ELECTRONIC COMMUNICATIONS OF THE EASST. - ISSN 1863-2122. - 10:(2008), pp. 1-14. ((Intervento presentato al 7. convegno International workshop on graph transformation and visual modeling techniques (GT-VMT 2008) tenutosi a Budapest nel 2008 [10.14279/tuj.eceasst.10.155.155].
Using graph transformation systems to specify and verify data abstractions
M. MongaUltimo
2008
Abstract
This paper proposes an approach for the specification of the behavior of software components that implement data abstractions. By generalizing the approach of behavior models using graph transformation, we provide a concise specification for data abstractions that describes the relationship between the internal state, represented in a canonical form, and the observers of the component. Graph transformation also supports the generation of behavior models that are amenable to verification. To this end, we provide a translation approach into an LTL model on which we can express useful properties that can be model-checked with a SAT solver.File | Dimensione | Formato | |
---|---|---|---|
gtapproach.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
420.62 kB
Formato
Adobe PDF
|
420.62 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.