Ergebnisse des Treffens der Arbeitsgemeinschaft Analyse und Verifikation verteilter Systeme vom 15.09. - 16.09.1997

An den beiden Tagen wurden verschiedene Tools zur Verfikation verteilter Systeme vorgestellt und hilfreiche Ansätze für die Entwicklung derartiger Tools diskutiert.

Teilnehmer: Jörg Dölfer, Frank Huch, Philipp van Hüllen, Jörg Köller, Martin Leucker, Thomas Noll, Alexander Pretschner, Thomas Richert, Ramin Sadre, Sigmar Tholen, Stefan Tobies

Es folgt ein kurze Zusammenfassung:

Spin

Spin ist sicherlich das am weitesten entwickelte Tool zur Verifikation. Es enthält eine eigene Programmiersprache zur Spezifikation (Promela), erlaubt Simulation und Verifikation mittels einer Logik. Bermerkungen zu Spin:

• grafische Benutzeroberfläche ist hilfreich
• Promela als Spezifikationssprache leicht erlernbar, da ähnlich zu CSP und C (bzw. höherer Programmiersprache). Allerdings fehlen Funktionen und Datentypen, um den Spezifikationskomfort zu erhöhen.
• Zahlreiche Optimierungen: On-the-fly Model Checking, Bit-State-Hashing, Partial Order Reduction
• ermöglicht Simulation des Systems
• Guided Simulation zum Visualieren von erkannten Fehlern möglich
• Fehlerpfade können bzgl. der Länge optimiert werden
• Nur LTL-Model Checking

Es wurde ein Spin-Praktikum angedacht.

Unity

Unity stellt einen allgemeinen Rahmen für Spezifikation paralleler Programme dar. Dieser Ansatz wurde kurz vorgestellt und diskutiert. Es lag allerdings keine einheitliche Bewertung vor. Bemerkt wurde:

• Einfaches Modell
• gut geeignet für math. Programme
• abstrakte Beschreibung eines Algorithmus möglich
• gut für (manuelle) Beweise

CWB, NCSU-CWB, CF

Die Concurrency Workbench (CWB) ist vor einigen Jahren in Edinburgh entwickelt worden und dient als Testplattform neuerer Algorithmen. An der North Carolina State University wurde eine neue Version implementiert, die einen Prozeßalgebra-Compiler beinhaltet (PAC), der die einfache Integration verschiedener Prozeßkalküle erlaubt. Eine Variante der CWB, bei der Prozesse grafisch eingegeben werden können, wurde als Concurrency Factory implementiert. Bemerkungen:

• Mächtige Logik ( -Kalkül) (Zu mächtig??)
• PAC sehr hilfreich
• Visual CCS hilfreich
• Nicht immer terminierend (was aufgrund der Berechnungsstärke von CCS allerdings sein muß)

Rewriting Logic

Die Rewriting Logic stellt einen einheitlichen Rahmen zur Beschreibung verschiedener semantischer Modelle für Parallelität dar. Dies wird (jedoch) in einem eher syntaktischen Rahmen durchgeführt. Es wurde die Programmiersprache Maude erwähnt, die als Grundlage die Rewriting Logic hat. Bemerkungen:

• Termersetzung ist nicht gerade anschaulich
• Einheitlicher Rahmen erlaubt Entwicklung eines PAC für verschiedene semantische Modelle
• als ,,abstrakte Maschine`` sinnvoll einsetzbar
• Verifikation unklar

HyTech

HyTech stellt ein Verifikationstool basierend auf linearen hybriden Automaten für Echtzeitanwendungen zur Verfügung. Bemerkungen:

• Nur Erreichbarkeit testbar (evtl. ist dies ausreichend, keine Logik)
• Semientscheidungsverfahren (evtl. ist dies zwingend), dennoch evtl. hilfreich zum Aufspüren von Fehlern
• Visualisierung fehlt

Mobility Workbench

Die Mobility Workbench stellt ein Tool dar, welches die Bisimulation zweier Spezifikationen im -Kalkül entscheidet.

• Visualisierung fehlt
• Unterstützt den -Kalkül
• Nur Bisimulation. Was ist mit Logik oder Simulation?
• Version für polyadischen -Kalkül
• Ineffizient

Es wurde angeregt, die Beziehungen zwischen den Bisimulationen von CCS und dem -Kalkül herauszuarbeiten, um den Test auf Bisimulation einheitlich behandeln zu können.

Fixpunkte und Bdd-Package

Bei dem Paket handelt es sich um eine Sammlung von Funktionen zur Berechnung kleinster Fixpunkte von booleschen Formeln und zur effizienten Darstellung boolescher Funktionen. Es wurde angeregt, sich die Verwendung von Bdds in Model Checking Tools genauer anzusehen, was in einem weiteren AG-Vortrag stattfinden soll. Außerdem ist die Entwicklung eines verteilten Bdd-Pakets angedacht worden.

Java und Erlang

Es wurde darüber nachgedacht, eine Abstraktion für eine der Sprachen Java oder Erlang zu erarbeiten, die als Grundlage zur Verifikation dienen kann.

Schlußbemerkungen

Das Treffen wurde von allen Teilnehmern als sehr hilfreich aufgefaßt. Das nächste reguläre AG-Treffen findet statt am Freitag, den 17.10.1997 um 14.00 Uhr im Seminarraum des Lehrstuhls.

Über dieses Dokument ...

This document was generated using the LaTeX2HTML translator Version 96.1 (Feb 5, 1996) Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split 0 main.

The translation was initiated by Martin Leucker on Thu Sep 18 15:53:55 MET DST 1997