Using Graph Transformation Systems to Specify and Verify Data Abstractions

  • 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 thisThis 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.show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author: Luciano Baresi, Carlo Ghezzi, Andrea Mocci, Mattia Monga
URN:urn:nbn:de:kobv:83-opus-20012
ISBN:1863-2122
Series (Serial Number):Electronic Communications of the EASST- ECEASST (10/21)
Document Type:Arbeitspapier/Research Paper
Language:English
Date of Publication (online):2008/08/28
Publishing Institution:Technische Universität Berlin
Release Date:2008/08/28
Tag:Data Abstractions; Graph Transformation Systems; Model Checking; SAT Solving; Specifications
Note:
http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/19
Institutes:Institut für Softwaretechnik und Theoretische Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Collection:Volume 10 (2008): Graph Transformation and Visual Modeling Techniques 2008
Licence (German):License LogoCC BY-NC-SA 2.0 DE: Creative Commons-Lizenz: Namensnennung, nicht kommerziell, Weitergabe unter gleichen Bedingungen 2.0 Deutschland