Diploma Thesis DIP-1980

BibliographySchneider, Sören: Evaluation von Systemen zur Korrektheitsuntersuchung am Beispiel von Konsistenzerhaltungsprotokollen.
University of Stuttgart, Faculty of Computer Science, Diploma Thesis No. 1980 (2002).
128 pages, german.
CR-SchemaC.2.1 (Network Architecture and Design)
C.2.2 (Network Protocols)
D.2.2 (Software Engineering Design Tools and Techniques)
D.2.4 (Software Engineering Software/Program Verification)
D.3.1 (Programming Languages Formal Definitions and Theory)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
I.6.3 (Simulation and Modeling Applications)
I.6.4 (Model Validation and Analysis)
J.6 (Computer-Aided Engineering)
Abstract

Ein großes Problem bei der gemeinsamen Erstellung von Dokumenten durch mehrere Personen betrifft die Konsistenz der Daten, denn jeder sollte beliebige Änderungen vornehmen können. Dies gilt in besonderem Maß, wenn Benutzer mit mobilen Endgeräten beteiligt sind, welche nicht permanent mit den Datenservern verbunden sind und somit die meiste Zeit Offline arbeiten. D.h. die Daten werden lokal bearbeitet und Änderungen eher abschnittsweise, auf einmal in das gemeinsame Dokument eingebracht. Um die dabei nicht zwangsweise entstehenden Inkonsistenzen zu kontrollieren und zu beheben, wurden bereits eine Reihe von Protokollen zur Konsistenzerhaltung (z.B. Grove, 2-Phasen-Sperren) vorgeschlagen.

Diese, mit zunehmender Komplexität, verwendeten Protokolle bestimmen in großem Maß den reibungslosen Ablauf bei der gemeinsamen Erstellung/Bearbeitung von Dokumenten. Deren Zuverlässigkeit scheint eine unabdingbare Forderung zu sein. Der Nachweis der "fehlerfreien Funktion"(Verifikation) ist jedoch ein sehr schwieriges Unterfangen.

Die am häufigsten verwendeten Verifikationstechniken sind Test (z.B. Blackbox- und Glasboxtest) und Simulation. Diese Verfahren sind jedoch sehr aufwändig und garantieren keine 100%ige Fehlerfreiheit.

Anfang der 80er Jahre wurde eine Methode entwickelt, welche es erlaubt, die logische Struktur komplexer Systeme/Protokolle vollautomatisch zu analysieren und den Nachweis der gestellten Anforderungen zu erbringen. Diese Technik wird Model Checking genannt und ist Grundbaustein moderner Verifikationswerkzeuge (z.B. Spin, Verisoft, UPPAAL, ...). Diese Werkzeuge erlauben die Modellierung und Verifikation von parallelen Systemen, Kommunikationsprotokollen und u.v.m.

Dabei werden die unterschiedlichsten Methoden verwendet. Beispielsweise besitzt Spin eine eigene Spezifikationssprache, mit welcher z.B. Kommunikationsprotokolle nachgebildet werden können, wogegen Verisoft auf dem Sourcecode arbeitet und die gestellten Forderungen direkt im zu überprüfenden System/Protokoll definiert werden können.

Um die an ein zu verifizierendes System gestellten Forderungen präzise formulieren und überprüfen (z.B. Finden von Deadlocks (Verklemmungen) und "unerreichbaren" Unterroutinen) zu können, verwenden die einzelnen Werkzeuge gesonderte oder integrierte Spezifikationsformalismen (z.B. LTL, CTL).

Full text and
other links
PDF (1189079 Bytes)
Access to students' publications restricted to the faculty due to current privacy regulations
Department(s)University of Stuttgart, Institute of Parallel and Distributed High-Performance Systems, Distributed Systems
Project(s)Institut für parallele und verteilte Höchstleistungsrechnersysteme
Entry dateJune 3, 2002
   Publ. Computer Science