Verifikation reaktiver Systeme

sondern in fortdauernder Wechselwirkung mit ihrer Umgebung stehen;
verteilte Algorithmen, Kontrollsysteme und Telekommunikations-
protokolle sind Beispiele fuer reaktive Systeme. Die Korrektheit
reaktiver Systeme ist ueblicherweise durch eine Spezifikation mit
Formeln temporaler Logik oder mit Omega-Automaten charakterisiert.

In dem Vortrag werde ich Verifikationstechniken fuer reaktive Systeme
auf der Basis von alternierenden Omega-Automaten vorstellen. Dabei
wird der (moeglicherweise unendliche) Zustandsraum des Systems in
einem ersten Schritt durch eine endliche Abstraktion ersetzt, die die
fuer die Spezifikation relevante temporale Struktur des Systems
erhaelt. Durch die Kombination mit der Spezifikation entsteht ein
alternierender Omega-Automat, dessen Sprache jedes moegliche
Fehlverhalten des Systems enthaelt. In einem zweiten Schritt wird
durch Transformation des Automaten und durch systematische
Untersuchung des Zustandsraums bewiesen, dass die Sprache des
Automaten leer ist.

In der Praxis scheitert die Verifikation von reaktiven Systemen oft an
der Groesse des Zustandsraums. Als Beispiele fuer Ansaetze zur Loesung
dieses Problems werde ich auf die Komponenten-orientierte Verifikation
mit Message Sequence Charts und auf die Ergaenzung der statischen
Verifikation durch dynamische ("runtime") Verifikation eingehen.

Die beschriebenen Verifikationstechniken sind in STeP, dem Stanford
Temporal Prover, implementiert.