Hybride Systeme modellieren Systeme, die sowohl kontinuierliches als auch diskretes Verhalten aufweisen. Da hybride Systeme oft zur Modellierung sicherheitskritischer Systeme verwendet werden, ist es notwendig eine Garantie für deren Zuverlässigkeit zu liefern.

Stabilität bzgl. einer Region (engl. region stability) beschreibt das Verhalten eines hybriden Systems, dessen Trajektorien eine Menge von Zuständen, eine Region, erreichen und diese nicht wieder verlassen. Stabilität bzgl. einer Region kann gezeigt werden, indem man die Endlichkeit der Folgen von Momentaufnahmen (engl. snapshot sequences) des hybriden Systems beweist. Die Folgen von Momentaufnahmen sind zeit-divergente Diskretisierungen der Trajektorienteile, die außerhalb der Region liegen. Die Endlichkeit einer Menge von Folgen von Momentaufnahmen wird von der Wohlfundiertheit einer entsprechenden binären Erreichbarkeitsrelation impliziert. Die Berechnung der binären Erreichbarkeitsrelation kann durch die (unäre) Erreichbarkeitsanalyse eines transformierten hybriden Systems mit doppelter Dimension, d.h. doppelter Anzahl von kontinuierlichen Variablen, durchgeführt werden. Die Erreichbarkeitsanalyse des Systems mit doppelter Dimension ist das Nadelöhr dieses Verfahrens zur Überprüfung von Stabilität bzgl. einer Region, da sie sehr hohe Ausführungszeiten für hybride Systeme mit höherer Dimension in Anspruch nimmt.

Der konzeptionelle Beitrag dieser Arbeit ist eine neue Kompositionalitätsform für die Beweisführung von Korrektheitseigenschaften von hybriden Systemen im Allgemeinen, und insbesondere von Stabilität bzgl. einer Region. Technisch haben wir drei kompositionelle Methoden zur Verifikation hybrider Systeme entwickelt. Experimentelle und theoretische Ergebnisse zeigen das Potenzial unserer Methoden.

Im ersten Verfahren beziehen wir, basierend auf dem Begriff der Verweilzeit, die Ergebnisse der Erreichbarkeitsanalyse einer Abstraktion eines gegebenen hybriden Systems H in die Erreichbarkeitsanalyse einer anderen Abstraktion des gleichen hybriden Systems H ein. Verweilzeit (engl. dwell time) ist die Zeit, die das hybride System H in einer Location kontinuierlich verbringen kann. Die gegenseitige Abhängigkeit zwischen den möglichen Werten der kontinuierlichen Variablen des hybriden Systems kann über Schranken für die Verweilzeit approximiert werden. Wir berechnen Schranken für die Verweilzeit in einer Abstraktion von H, und nutzen jene Schranken in der Safety- oder Stabilitäts-Analyse der anderen, komplementären Abstraktion von H. Wir nennen diese Methode Verweilzeitverfeinerung.

Zweitens erweitern wir die Verweilzeitverfeinerung zu einer allgemeineren, constraint-basierten Verfeinerung. Für die Komposition von zwei Analysen verwenden wir constraints über alle kontinuierlichen Variablen. Wir berechnen constraints für eine Location in einer Abstraktion des hybriden Systems, und verwenden diese, um eine andere Abstraktion des gleichen hybriden Systems zu verfeinern.

Das dritte Verfahren basiert auf der Beobachtung, dass wir die Folgen von Momentaufnahmen schrittweise berechnen können. Für die Analyse der Stabilität bzgl. einer Region eines hybriden Systems mit Dimension n berechnen wir Teile der Folgen von Momentaufnahmen durch Erreichbarkeitsanalyse eines transformierten hybriden Systems, das nur eine verdoppelte Variable enthält, d.h. mit Dimension (n +1). Die Erreichbarkeitsanalyse des hybriden Systems mit (n +1) Variablen liefert die Darstellung eines Teils der Folgen von Momentaufahmen des ursprünglichen hybriden Systems in Form einer partiellen, binären Erreichbarkeitsrelation. Die Wohlfundiertheit einer dieser partiellen binären Relationen impliziert bereits Stabilität bzgl. der Region. Darüber hinaus ergibt die Zusammensetzung der partiellen binären Relationen für alle kontinuierlichen Variablen die gleiche Menge von Folgen von Momentaufnahmen wie die Erreichbarkeitsanalyse des hybriden Systems mit doppelter Dimension. Damit reduzieren wir die Komplexität der Verifikation von Stabilität bzgl. einer Region von der Komplexität der Erreichbarkeitsanalyse eines hybriden Systems mit 2n kontinuierlichen Variablen auf die Komplexität, die sich aus der Komposition der Ergebnisse von höchstens n Erreichbarkeitsanalysen von hybriden Systemen mit Dimension (n +1) ergibt.

Schlagwörter: Hybrid Systems; Compositional Methods; Model Checking; Region Stability Verification; Dwell Time Inferration and Exploitation

Berichte aus der Informationstechnik