Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata

Die Konstruktion eingebetteter Systeme, die starke Realzeit-Anforderungen zu erfüllen haben, wird in den verschiedensten Anwendungsbereichen immer bedeutsamer, z. B. in der Medizin, der Transporttechnik oder der Produktionsautomatisierung. Formale Methoden unterstützen die fehlerarme Entwicklung solcher Systeme, weil sie auf einer präzisen mathematischen Grundlage aufbauen. Der Autor entwickelt einen geeigneten Modellierungsformalismus und effiziente Verifikationsverfahren für den Einsatz einer formalen Methode. In einer Fallstudie wird zuverlässige Software zur Steuerung von Produktionsanlagen konstruiert. Unsere Welt wird immer komplexer – oder besser: Wir selbst machen sie in unserem Automatisierungs- und Informationszeitalter immer schwieriger zu verstehen, indem wir immer komplexere Systeme konstruieren und in unseren Lebensalltag integrieren. ”Komplexität” ist zu einem Schlagwort geworden. Manchmal sind Systeme aber gar nicht so kompliziert, wie sie erscheinen. Das Verständnis hängt davon ab, wieviel Ordnung des Systems erkennbar ist. Eines der Schlüsselkonzepte zur Beherrschung der von uns zu lösenden Probleme ist das Erkennen und Nutzen von Struktur. Die beiden Hauptprobleme, mit deren Lösung sich die vorliegende Arbeit beschäftigt, sind die formalisierte Beschreibung von technischen Systemen (Modellierung) und der anschließende Nachweis der Korrektheit dieser Beschreibung (Verifikation). Die vorgeschlagenen Lösungsansätze beruhen jeweils auf der Idee ”Strukturierung schafft Ordnung”. Bei der Modellierung bedeutet dies, die für das Problem relevanten Strukturelemente eines Systems explizit in der Beschreibung auszudrücken und das System-Modell somit verständlicher zu gestalten. Bei der Verifikation bedeutet es, die im Modell vorhandene Struktur für die Datenstrukturen und Algorithmen der vollautomatischen Analyse des Modells zu benutzen und somit eine effiziente Verifikation zu ermöglichen.