Das SH-Verification Tool

Das SH Verification-Tool (SH steht für Simple Homomorphism) hat zum Ziel, kooperierende Systeme auf bestimmte Eigenschaften zu überprüfen. APA sind eine Möglichkeit kooperierende Systeme zu spezifizieren. Wenn in einem gegebenen Zustand eines APA mehrere elementare Automaten einen Zustandsübergang durchführen können (d.h. es sind Voraussetzungen für verschiedene Zustandsübergänge erfüllt) ist nicht definiert, welcher der Agenten einen Zustandsübergang macht. Das ist eine Form von Nicht-Determinismus, welcher typisch für kooperierende Systeme ist. In solchen Nicht-Deterministischen Systemen ist das Verifizieren von bestimmten Eigenschaften sehr schwierig, da der Zustandsraum (die Menge der möglichen Zustände) sehr schnell mit der Anzahl der beteiligten Komponenten wächst. Um dennoch eine Analyse durchführen zu können, betrachtet das SHVT Abstraktionen des eigentlichen Systems. Unter bestimmten Bedingungen lassen sich aus Eigenschaften der Abstraktionen Aussagen über entsprechende Eigenschaften des Originalsystems ableiten.

Das SHVT ist nicht an eine formale Spezifikationssprache gebunden. Für den praktischen Einsatz muss es daher mit Tools kombiniert werden, welche 'labeled transition systems' (kurz LTS) generieren. Derzeit werden vom SHVT Produktnetze (eine spezielle Form von Petrinetzen) und APA als Spezifikationssprachen unterstützt. Ein LTS ist gegeben durch einen Zustandsraum, einer Menge von Transitionen (Zustandsübergängen) darauf und einen Startzustand. Es kann daher mit einem gerichteten Graphen visualisiert werden. Für Systeme aus der Praxis sind solche Darstellungen jedoch extrem umfangreich und daher nicht wirklich zur Veranschaulichung geeignet. Ein LTS definiert eine formale Sprache - die lokale Sprache des LTS. Die Transitionen des LTS bilden das Alphabet $\Sigma$ dieser Sprache, d.h ein Buchstabe entspricht einem Tripel aus Zustand, Beschriftung der Transition, und Folgezustand. Ein Wort der lokalen Sprache eines LTS ist also eine mögliche Folge von Zustandsübergängen ausgehend vom Startzustand. Mit $\Sigma^*$ wird die Menge aller endlichen Folgen von Buchstaben aus $\Sigma$ notiert.

Auf solchen formalen Sprachen lassen sich Abstraktionen durch Homomorphismen repräsentieren. Eine Abbildung $h: \Sigma^* \rightarrow \Sigma'^*)$ heißt Homomorphismus, wenn $h(\epsilon) = \epsilon$ und $h(uv) = h(u)h(v)$ gilt, wobei $\epsilon$ das leere Wort und $u,v$ beliebige Wörter aus $\Sigma^*$ sind. Ein Homomorphismus heißt alphabetisch, wenn er einzelne Buchstaben aus $\Sigma$ auf einzelne Buchstaben in $\Sigma'$ oder das leere Wort abbildet ( $h(\Sigma) \subseteq \Sigma' \cup \{\epsilon\}$). Alle vom SHVT betrachteten Abstraktionen sind alphabetische Homomorphismen.

Eine Abstraktion entspricht einer Vereinfachung des Systems. Werden bestimmte Buchstaben auf das leere Wort abgebildet, so werden die damit verbundenen Zustandsübergänge ignoriert und das System wird einfacher (Verbergen von Aktionen). Werden verschiedene Buchstaben auf denselben Buchstaben abgebildet, so können die damit verbundenen Aktionen in der Abstraktion nicht mehr unterschieden werden (Identifikation von Aktionen), was das System ebenfalls vereinfacht.

Also entspricht eine solche Abstraktion einem Verlust von Information über das System. Interessant sind nun solche Abstraktionen, aus deren Analyse Rückschlüsse auf das Originalsystem gezogen werden können. Man kann zeigen, daß schlichte Homomorphismen diese Schlussfolgerung zulassen.

Definition: Ein Homomorphismus heißt schlicht auf der Sprache $L$, wenn gilt:

$$\begin{eqnarray*} \forall_{x \in L} \; \exists_{w \in h(x)^{-1}(h(L))}: && w^{-... ...L)) \\ wobei: && w^{-1}(L) = \{y \in \Sigma^* \vert wy \in L\} \end{eqnarray*}$$

Dabei bezeichnet $w^{-1}(L)$ die Menge aller möglichen Fortsetzungen von $w$ um ein Wort der Sprache $L$ zu erhalten.

Für reguläre Sprachen ist Schlichtheit von Homomorphismen entscheidbar, die Algorithmen dazu sind jedoch sehr komplex. Es gibt jedoch notwendige und hinreichende Bedingungen für Schlichtheit, die sich auf einem LTS-Graphen effizient testen lassen. Für größere Systeme ist es allerdings sehr aufwendig einen Graphen zum entsprechenden LTS zu konstruieren (da diese Graphen sehr schnell sehr groß werden). Für 'günstig' strukturierte Systeme lässt sich die Schlichtheit von Homomorphismen überprüfen, ohne das komplexe LTS des Originalsystems zu berechnen. Dazu bettet man die einzelnen Komponenten des Systems in einfachere Umgebungen ein, die dasselbe Schnittstellenverhalten wie die Umgebungen der Komponenten im Originalsystem aufweisen. Für die so erhaltenen Systeme (Komponenten in jeweils einfacher Umgebung) kann die Schlichtheit von Homomorphismen vergleichsweise leicht geprüft werden. Die so erhaltenen Homomorphismen für verschiedene disjunkte Komponenten lassen sich nun zu einem Homomorphismus für das Gesamtsystem kombinieren. Unter bestimmten Bedingungen für die einzelnen Homomorphismen (unter anderem: Schlichtheit) kann man zeigen, daß der bei Kombination entstehende Homomorphismus ebenfalls schlicht ist. Für 'geeignet' strukturierte Systeme lässt sich so eine beträchtliche Reduktion des Zustandsraumes erreichen. APA sind in diesem Sinne geeignet strukturiert. Sie bestehen bereits aus einzelnen Komponenten (den elementaren Automaten), die so kombiniert sind, daß sie direkt Kandidaten für die oben erwähnte Einbettung in einfache Umgebungen darstellen.

Das SHVT arbeitet halbautomatisch. Es benötigt Hilfe vom Benutzer, um geeignete Homomorphismen zu generieren. Dabei stellt es die Möglichkeit zur schnellen Überprüfung der Schlichtheit zur Verfügung. Ist Schlichtheit nicht erfüllt oder nicht nachzuweisen, kann mit Hilfe der Ausgaben des SHVT die problematische Stelle gefunden werden, bei der eine Verfeinerung des Homomorphismus nötig ist.

Das SHVT wurde in Allegro Common Lisp implementiert und ist für nicht-kommerzielle Anwendungen frei erhältlich. Ein anonymer FTP-Download ist jedoch nicht möglich aufgrund von lizenzrechtlichen Einschränkungen der Laufzeitbibliothek des Lisp-Systems.