Guaranteed Verification of Dynamic Systems

Diese Arbeit beschreibt einen neuen Spezifikations- und Verifikationsansatz für dynamische Systeme. Der neue Ansatz ermöglicht dabei Ergebnisse, die per Definition frei von Fehlern 2. Art sind. Dies bedeutet, dass das Ergebnis der Verifikation keine versteckten Fehler enthalten kann. Somit können zuverlässige Ergebnisse für die Analyse von sicherheitskritischen Systemen generiert werden.
Dazu wird ein neues Verständnis von mengenbasierter Konsistenz dynamischer Systeme mit einer gegebenen Spezifikation eingeführt. Dieses basiert auf der Verwendung von Kaucher Intervall Arithmetik zur Einschließung von Messdaten. ... mehrKonsistenz wird anhand der vereinigten Lösungsmenge der Kaucher Arithmetik definiert. Dies führt zu mathematisch garantierten Ergebnissen. Die resultierende Methode kann das spezifizierte Verhalten eines dynamischen System auch im Falle von Rauschen und Sensorungenauigkeiten anhand von Messdaten verifizieren.
Die mathematische Beweisbarkeit der Konsistenz wird für eine große Klasse von Systemen gezeigt. Diese beinhalten zeitinvariante, intervallartige und hybride Systeme, wobei letztere auch zur Beschreibung von Nichtlinearitäten verwendet werden können. Darüber hinaus werden zahlreiche Erweiterungen dargestellt. Diese führen bis hin zu einem neuartigen iterativen Identifikations- und Segmentierungsverfahren für hybride Systeme. Dieses ermöglicht die Verfikation hybrider Systeme auch ohne Wissen über Schaltzeitpunkte. Die entwickelten Verfahren können darüber hinaus zur Diagnose von dynamischen Systemen verwendet werden, falls eine ausreichend schnelle Berechnung der Ergebnisse möglich ist.
Die Verfahren werden erfolgreich auf eine beispielhafte Variation verschiedener Tanksysteme angewendet.
Die neuen Theorien, Methoden und Algortihmen dieser Arbeit bilden die Grundlage für eine zuverlässige Analyse von hochautomatisierten sicherheitskritischen Systemen.

This thesis introduces a new specification and verification approach for dynamic systems. The introduced approach is able to provide type II error free results by definition, i.e. there are no hidden faults in the verification result. The approach is thus suitable to provide a reliable verification of safety critical systems.
A new notion of set based consistency for dynamic systems with a given specification is presented. Therefore Kaucher interval arithmetic is used to enclose the measurement data in a bounded error sense. The resulting method is able to verify the specified behavior of a dynamic system against its measurement data even in the presence of noise and sensor uncertainty. ... mehrConsistency is defined using the Kaucher arithmetic united solution set which leads to mathematically guaranteed results.
It is proven mathematically that the desired property holds for a wide class of systems, including time invariant, interval type and hybrid systems, which can be used to describe even nonlinearities. Several extensions are introduced, leading to a new iterative identification and segmentation algorithm for hybrid systems which is able to handle even unknown switching times. In case the calculations can be done fast enough, the developed approach can also be used for the diagnosis of dynamic systems.
The presented methods are successfully applied to several example systems, including theoretic settings and a variation of different tank settings.
The new theories, methods and algorithms developed in this thesis form the foundation for reliable safety analysis of highly automated safety critical systems.