Eingang zum Volltext in OPUS
Lizenz
Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:kobv:83-opus-20012
URL: http://opus.kobv.de/tuberlin/volltexte/2008/2001/
Baresi, Luciano ; Ghezzi, Carlo ; Mocci, Andrea ; Monga, Mattia
Using Graph Transformation Systems to Specify and Verify Data Abstractions
| pdf-Format: |
| |
| Print-on-Demand: |
Kurzfassung auf Englisch
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.
| Freie Schlagwörter (Englisch): | Graph Transformation Systems , Specifications , Data Abstractions , Model Checking , SAT Solving | |
| Collection: | TU Berlin / Zeitschriften / Fakultät IV - Elektrotechnik und Informatik / Electronic Communications of the EASST- ECEASST / Volume 10 (2008): Graph Transformation and Visual Modeling Techniques 2008 | |
| Institut: | Institut für Softwaretechnik und Theoretische Informatik | |
| DDC-Sachgruppe: | Informatik | |
| Dokumentart: | Aufsatz | |
| Schriftenreihe: | Electronic Communications of the EASST- ECEASST | |
| Bandnummer: | 10/21 | |
| ISBN/ISSN: | 1863-2122 | |
| Quelle: | http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/19 | |
| Sprache: | Englisch | |
| Erstellungsjahr: | 2008 | |
| Publikationsdatum: | 28.08.2008 | |
| Lizenz: | Standardlizenz: Typ CC by-nc-sa - Namensnennung erforderlich | Kommerziell nein | Weiterbearbeitung nur unter gleichen Bedingungen erlaubt | PoD ja |