Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-124
Main Title: Integration of Graph transformation and temporal logic for the specification of distributed systems
Translated Title: Integration von Graphtransformation und temporaler Logik zur Spezifikation verteilter Systeme
Author(s): Koch, Manuel
Advisor(s): Ehrig, Hartmut
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Die vorliegende Arbeit stellt eine formale Spezifikationsmethode für verteilte Systeme vor. Ziele der Arbeit sind die komponentenweise Modellierung des Verhaltens verteilter Systeme, die Spezifikation von Eigenschaften verteilter Systeme und die Unterstützung zum (automatischen) Überprüfen dieser Eigenschaften. Um diese Ziele zu erreichen, schlage ich einen integrierten Ansatz zweier formaler Methoden vor: verteilte Graphtransformation und temporale Logik. Verteilte Graphtransformation wird zur Modellierung des Verhaltens verteilter Systeme eingesetzt, Eigenschaften werden mit temporaler Logik spezifiziert. Der kombinierte Ansatz profitiert von den Stärken der einzelnen Ansätze und stellt eine geeignete Methode zur Verfügung, Aspekte verteilter Systeme formal und graphisch zu modellieren. Ich habe einen Single-Pushout (SPO) Ansatz für verteilte Graphtransformation entwickelt, der sowohl die Topologie als auch die lokalen Datenzustände spezifiziert. Dieser Ansatz läßt eine Vielzahl von Spezifikationstechniken für die lokalen Zustände zu. Ein Hauptbeitrag meines Ansatzes ist die kompositionale operationale Semantik, welche auf den von Martin Große-Rhode entwickelten Transformationssystemen basiert. Ich integriere den SPO Ansatz für verteilte Graphtransformation und eine aussagenlogische temporale Logik. Die Integration vollzieht sich über eine Pre-Ordnung (eine reflexive und transitive Relation) über verteilten Graphen und resultiert in graphinterpretierten temporalen Formeln und temporalen Graphmodellen. Graphinterpretierte Formeln erlauben die graphische Spezifikation temporaler Eigenschaften, so dass die Spezifikation des verteilten Systems und die Spezifikation der Systemeigenschaften im selben Formalismus geschieht. Dank der Integration verteilter Graphtransformation und temporaler Logik können vorhandene Konzepte im Bereich der temporalen Logik zum Nachweis graphinterpretierter Formeln bzgl. eines mit verteilter Graphtransformation modellierten Systems genutzt werden. Insbesondere das Konzept des Model-Checkens wird in dieser Arbeit zur automatischen Verifikation von graphinterpretierten Formeln betrachtet. Ich stelle die Konstruktion eines typischen Modells vor, welche ein möglicherweise unendliches temporales Graphmodell (d.h. ein Modell mit unendlich vielen Zuständen) zu einem endlichen Graphmodell zusammenfaßt. Das typische Modell hilft, von lokaler Erfüllbarkeit lokaler Formeln in einem Teilsystem des verteilten Systems auf die globale Erfüllbarkeit globaler Formeln im gesamten verteilten System zu schließen.
This work provides a methodology for the specification of distributed systems based on formal methods. Major aims are the compositional modeling of the behavior of distributed systems, the specification of distributed system properties and the support of their (automatic) verification. To reach this goal, I propose an integrated approach of two formal methods, namely distributed graph transformation and temporal logic. Distributed graph transformation is intended for modeling the behavior of distributed systems, whereas distributed system properties are specified by temporal logic. The combined approach benefits from the strength of each single approach and provides a suitable methodology to model formally the aspects of distributed systems. I develop a single-pushout approach to distributed graph transformation that specifies the topology of the distributed system as well as its local data states. My approach permits a variety of specification techniques for local data states, where I investigate the requirements for the specification techniques that can be used for the local data. A main contribution of my approach to distributed graph transformation is the compositional operational semantics. This semantic is based on transformation systems introduced by Große-Rhode. I integrate the single-pushout approach to distributed graph transformation and a propositional temporal logic. The integration takes place over a pre-order relation over distributed graphs and results in graph-interpreted temporal formulas and temporal graph models. Graph-interpreted formulas provide a methodology to specify temporal properties graphically, in the same way as the distributed system itself is specified. The integration of distributed graph transformation and temporal logic allows to make use of the variety of verification concepts in the area of temporal logic to check graph-interpreted temporal formulas with respect to a temporal graph model. I focus in this work especially on the concept of model-checking for the automatic verification of graph-interpreted temporal formulas. I provide the construction of a typical graph model that collapses a possibly infinite temporal model to a finite one and that supports the reasoning from the local satisfaction of local formulas in a sub-system of the distributed system to global satisfaction of global formulas in the complete distributed system.
URI: urn:nbn:de:kobv:83-opus-284
http://depositonce.tu-berlin.de/handle/11303/421
http://dx.doi.org/10.14279/depositonce-124
Exam Date: 30-Sep-1999
Issue Date: 2-Jun-2000
Date Available: 2-Jun-2000
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Graphtransformation
Softwarespezifikation
Temporale Logik
Verteilte Konfigurationsverwaltung
Verteilte Systeme
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_32.pdf4,62 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.