Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata

Más información sobre el libro

Die Konstruktion eingebetteter Systeme mit starken Realzeit-Anforderungen gewinnt in verschiedenen Anwendungsbereichen wie Medizin, Transporttechnik und Produktionsautomatisierung zunehmend an Bedeutung. Formale Methoden bieten Unterstützung für die fehlerarme Entwicklung solcher Systeme, da sie auf einer präzisen mathematischen Grundlage basieren. Der Autor entwickelt einen Modellierungsformalismus und effiziente Verifikationsverfahren für die Anwendung formaler Methoden. Eine Fallstudie demonstriert die Konstruktion zuverlässiger Software zur Steuerung von Produktionsanlagen. In unserer komplexer werdenden Welt, geprägt durch Automatisierung und Informationsverarbeitung, konstruieren wir Systeme, die oft schwer zu verstehen sind. Das Schlagwort "Komplexität" beschreibt diesen Zustand, wobei Systeme manchmal weniger kompliziert sind, als sie erscheinen. Das Verständnis hängt von der erkennbaren Ordnung im System ab. Ein zentrales Konzept zur Lösung dieser Probleme ist das Erkennen und Nutzen von Struktur. Die Arbeit behandelt die formalisierte Beschreibung technischer Systeme (Modellierung) und den Nachweis der Korrektheit dieser Beschreibung (Verifikation). Die Lösungsansätze basieren auf der Idee, dass "Strukturierung Ordnung schafft". Bei der Modellierung werden relevante Strukturelemente explizit dargestellt, um das System-Modell verständlicher zu machen. Bei der Verifikation wird die vorhandene Struktur für die Analyse d