Die Idee für die Analyse der Deadlock- und Livelockeigenschaften von FML und AVI basiert auf der Verwendung von Occam als Programmiersprache: die Spezifikationssprache CSP (Communicating Sequential Processes) ist für die Spezifikation von kommunizierenden Prozessen konzipiert und erlaubt eine schrittweise Verfeinerung von Spezifikationen zu Occam Programmen.
Abbildung 1: Abstraktion von occam-Code zu CSP-Spezifikation
(Anklicken für vergrößerte Darstellung)
Bei der Abstraktion von occam-Code zu CSP-Spezifikationen werden die Regeln der Tabelle von Abbildung 2 angewendet. Ziel dieser Abstraktion ist die Verwendung von maximalem Nichtdeterminismus bei Fallunterscheidungen, in diesem Fall das Weglassen von konkreten Bedingungen. Weiterhin findet eine Abstraktion von konkreten Daten statt, soweit dies möglich ist; konkret der Reduktion von Kommunikationen über Kanäle auf einfache Kanalereignisse. Maximaler Nichtdeterminismus und Datenabstraktion führen zu kleinen Modellen.
Abbildung 2: Abstraktion von Occam-Code zu CSP-Spezifikation
(Anklicken für vergrößerte Darstellung)
An Abbildung 2 kann man die Abstraktion nachvollziehen. Der Occam Code entspricht einem kleinen System aus 2 Prozessen P und Q, die über gemeinsame Kanäle a und b Daten (boolesche Werte) austauschen und über den gemeinsamen Kanal c den Wert der globalen Variablen mc. Hierbei gibt es eine racing condition: der Wert nach Ausführung des Schleifenrumpfs hängt im Fall mc = 1 davon ab, ob P oder Q die Zuweisung als letztes durchführt. Die angegebene CSP- Abstraktion ignoriert die Daten, die über die Kanäle transportiert werden und modelliert in diesem Sinne lediglich die Reihenfolgen der Kanalnutzung.
Die Definition von S1 enthält die Information über die Kanäle über die synchronisiert wird. Ein Modell, dass die Fallunterscheidung auf Basis der Variablen mc getreuer wiederspiegelt, benötigt dafür zusätzlich eine Modellierung der Variablen als Prozess und den Datenbereich der Kanäle a und b und erfordert daher einen größeren Zustandsraum.
Für die Deadlock- und Livelock-Analysen wurden zunächst der Pseudocode und später der Code von FML und AVI zu CSP Spezifikationen abstrahiert und zwar in einer Art, die zwar das Kommunikationsverhalten, nicht aber andere funktionale Eigenschaften des Codes berücksichtigt. Auf diese Art entstanden relativ kleine Modelle der Anwendungen, für die nun eine partiell automatisierte Analyse durchgeführt wurde. Der Modelchecker FDR2 (Failures Divergence Refinement) erlaubt die Prüfung von CSP Spezifikationen bezüglich Verfeinerung, Deadlock und Livelock unter Verwendung von Model-Checking-Methoden. Die interne Repräsentation der Spezifikationen sind Transitionsgrafen, die Prüfung erfolgt mittels Durchsuchen des Zustandsraumes dieser Grafen. FDR2 gehört zu den leistungfähigsten Modelcheckern, die zu dem damaligen Zeitpunkt und auch noch heute verfügbar sind.
Leider erwies es sich, dass das Werkzeug nicht in der Lage ist, eine vollständige Spezifikation eines FML oder AVI zu analysieren aufgrund einer Zustandsexplosion basierend auf dem hohen Grad an Nebenläufigkeit. Alternative: Mit Hilfe der kompositionellen Theorie von CSP ist es in bestimmten Fällen möglich, die Ergebnisse von Deadlock- oder Livelock-Analysen für lokale Prozesse auf das
Prozess-System zu übertragen, wobei die Art der Komposition der Prozesse eine Rolle spielt. Wo diese formalen Argumente nicht mehr verwendbar waren, wurden informelle (im Englischen rigorous) Argumente herangezogen.
Somit ergibt sich eine Kombinationen unterschiedlicher Methoden, deren Erfahrungen positiv waren hinsichtlich der gefundenen Probleme und Effizienz.
Zurück zum Überblick Deadlock- und Livelock-Analyse für die internationale Raumstation ISS
Nächster Gliederungspunkt Erfahrungen |
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren