Suche

Effizienz asynchroner Systeme


Projektstart: 01.01.1993
Projektträger: Universität Augsburg
Projektverantwortung vor Ort: Walter Vogler
Publikationen: Link zur Publikationsliste

Zusammenfassung

siehe Beschreibung

Beschreibung

Projektförderung durch DFG 1994 - 1999

Charakteristisch für asynchrone, also ungetaktete Systeme ist, dass sich ihre Komponenten nicht aufgrund von Zeitmessungen koordinieren können. Im Projekt werden solche Systeme in Prozessalgebren oder mit Petrinetzen modelliert.

  • Petrinetze sind aufgrund ihrer graphischen Darstellung für Praktiker zugänglicher und bilden damit eine geeignete Schnittstelle zwischen Praktikern und Theoretikern; ferner machen sie die Kausalität in Systemabläufen unmittelbar sichtbar und sind dadurch konzeptionell attraktiv.
  • Prozessalgebren modellieren Systeme durch algeraische Terme und unterstützen daher die praktisch unerlässliche modulare Systemkonstruktion.

Auch Petrinetze lassen sich durch Parallelkomposition aus Komponenten aufbauen, und diese Operation ist von entscheidender Bedeutung für das Projekt. In beiden Ansätzen lassen sich sowohl Spezifikationen als auch Implementierungen von Systemen modellieren.

Werden Petrinetze oder Prozessalgebren um Zeit erweitert, so führt das üblicherweise auf Modelle synchroner Systeme, die Funktionalität ändert sich also durch Einführung der Zeit; auch spielt Modularität oft keine Rolle bei einer solchen Erweiterung. Im Projekt wird Zeit lediglich zum Effizienzvergleich verwendet, die Funktionalität der asynchronen Systeme bleibt dabei erhalten.

Effizienztesten

Bei der Systemanalyse ist es offensichtlich wichtig, gerade solche Aspekte des Systemverhaltens zu untersuchen, die für den System-Benutzer wahrnehmbar sind; was das bedeutet, lässt sich im Testansatz von De Nicola und Hennessy formalisieren, der in der Regel auf Semantiken führt, die einen modularen Systementwurf ermöglichen. Mit dem Effizienztesten wurde im Projekt eine Variante dieses Ansatzes entwickelt, die auf eine "schneller-als"-Relation führt, welche asynchrone Systeme auf Basis der Worst-Case-Effizienz vergleicht.

Wichtige bisherige Ergebnisse sind die vom Testansatz unabhängige Charakterisierung dieser "schneller-als"-Relation und der Nachweis, dass diese Relation bei Verwendung von (realistischerer) kontinuierlicher Zeit dieselbe ist wie bei Verwendung von diskreter Zeit - wobei letztere natürlich einfacher handzuhaben ist. Gestützt auf letzteres Ergebnis wurde das Tool FastAsy entwickelt, das feststellt, ob ein System (modelliert als Petrinetz) für jeden Benutzer schneller ist als ein anderes. Es wurden verschiedene realistische Beispiele behandelt sowie der Zusammenhang zu fairem Verhalten untersucht; letzteres ist entscheidend für die Verifikation.

Diese Untersuchungen wurden zunächst anhand von Petrinetzen durchgeführt (Zusammenarbeit mit E. Bihler und L. Jenner, Uni. Augsburg), in neuerer Zeit aber vor allem unter Vewendung der Prozessalgebra PAFAS (Zusammenarbeit mit F. Corradini und M.-R. Berardini, Uni. Camerino, Italien). Damit wird der Ansatz einer erweiterten Community zugänglich gemacht und die Unabhängigkeit der Ergebnisse von der gewählten Modellierung demonstriert.

Effizienztesten fordert - ähnlich wie jeder übliche Testansatz -, dass ein System für jeden denkbaren Benutzer schneller ist; tatsächlich werden in der Praxis aber oft Annahmen über das Benutzerverhalten gemacht, d.h. ein System soll tatsächlich nur für eine gewisse Klasse von Benutzern schneller sein. Es wurde gezeigt, dass Pipelining unter gewissen realistischen Annahmen zu besserer Performanz führt, und es wurden weitere Ergebnisse zur quantitativen Bestimmung dieser Performanz erzielt.

Effizienzvergleich mit Bisimulationen

Alternativ zum Testansatz können "schneller-als"-Relationen auch auf Basis der Standard-Äquivalenz Bisimulation definiert werden, welche Systeme üblicherweise feiner unterscheidet. In Zusammenarbeit mit G. Lüttgen (Uni. York, UK) wurde dazu die verbreitete Prozessalgebra CCS in geeigneter Weise um Zeit erweitert. U.a. wurde eine "schneller-als"-Relation als eine Kombination von Bisimulation auf Aktionen und Simulation auf Zeitschritten definiert; diese technisch einfache Definition wurde validiert, indem ihre Übereinstimmung mit unmittelbar einsichtigeren, aber aufwendigeren Definitionen gezeigt wurde.