Automatische Verifikation

Die Grundidee des automatischen Verifizierens besteht darin, dass man das zu untersuchend System als einen Automaten rekonstruiert, dessen Verhalten man als einen Überführungsgraph (Engl.: 'transition graph') und diesen wiederum als einen Ausführungsgraphen (Engl.: 'Execution graph') darstellen kann. Ein Ausführungsgraph hat den Vorteil, dass er alle möglichen Pfade eines Automaten anzeigt. Sofern man jetzt jedem Zustand eines Automaten charakteristische Eigenschaften $\Phi^{i}$ zugeordnet hat, kann man ausschließlich durch 'Inspektion' des Ausführungsgraphen feststellen, ob in der Gesamtheit aller Pfade eine bestimmte Eigenschaft $\Phi$ wenigstens einmal vorkommt ('Reachability') oder niemals ('Safety'). Eine andere interessante Konstellation wäre, ob immer dann, wenn eine bestimmte Eigenschaft $\Psi$ aufgetreten ist, dann auch irgendwann unausweichlich Eigenschaft $\Phi$ folgen wird ('Liveness'). Eine spezielle Eigenschaft wäre die Freiheit von Deadlocks ('deadlock-Freeness'). Eine andere interessante Konstellation wäre die 'Wiederholung der Erreichbarkeit', genannt 'Faireness'. Damit ist gemeint, dass unter einer bestimmten Bedingung eine bestimmte Eigenschaft unbegrenzt oft in der Zukunft auftreten wird, usw.

Könnte man nun ein Realzeitsystem als einen Automaten so beschreiben, dass jeder Zustand hinreichend viele charakteristische Eigenschaften notiert, so dass man anhand dieser Eigenschaften in der Lage wäre, das Verhalten eines Automaten zu analysieren, dann könnte man sich jetzt überlegen, einen Algorithmus zu schreiben, der die Eigenschaften eines Ausführungsgraphen automatisch überprüft bzw. verifiziert. Um diese Aufgabe der Überprüfung der Eigenschaften der Zustände eines Graphen weitgehend zu vereinfachen und zu vereinheitlichen, hat man formale (logische) Beschreibungssprachen entwickelt, die sowohl hinreichend ausdrucksstark sind, um alle die gewünschten Eigenschaften repräsentieren zu können, als auch einfach genug, um noch in praktikabler Zeit entscheidbar zu sein.

Um die Idee einer automatischen Verifikation anwenden zu können muss man das Konzept eines Realzeitsystems (vgl. Schaubild 12.1) in eine geeignete Darstellung eines passenden Automaten übersetzen. Dies kann man entweder direkt tun oder über einen Zwischenschritt, indem man nämlich das Konzept des Realzeit-Schedulers (vgl. Schaubild 12.2) mittels einer geeigneten formalen Sprache $L$ 'kodiert' sprich 'programmiert'. Formale Sprachen werden über formale Grammatiken $G$ definiert. Die durch eine formale Grammatik $G$ definierte formale Sprache $L(G)$ kann dann von einem geeigneten Automaten $A$ 'erkannt' werden^12.1, Moll et. 1988 [67] oder Rozenberg et Salomaa 1997 [86]). Nachfolgend wird zunächst der Weg der direkten Kodierung gewählt.

Figure 12.1: Komponentendarstellung eines Realzeitsystems samt Umgebung

Figure 12.2: Scheduler eines Realzeitsystems als Aktivitätsdiagramm