23.05.2011

Informatik-Kolloquium

Im Sommersemester 2011 findet im Rahmen des Informatik-Kolloquiums der folgende Vortrag statt:

Montag, 23. Mai 2011, 17:00 Uhr, Turing-Hörsaal

Prof. Dr. Christoph Scholl (Universität Freiburg)

Verifikation Hybrider Systeme mit Symbolischen Methoden

Eingebettete Systeme, die in technischen Systemen komplexe Steuerungs-, Regelungs- und Datenverarbeitungsaufgaben übernehmen, erfahren eine immer größere Verbreitung. Aufgrund der Komplexität heutiger Eingebetteter Systeme wird es immer schwieriger, ihr korrektes Funktionieren zu garantieren. Da die entworfenen Systeme aber häufig in sicherheitskritischen Bereichen eingesetzt werden, sind Kompromisse hinsichtlich Zuverlässigkeitsgarantien nicht akzeptabel. Aus diesem Grund geht man immer mehr dazu über, simulative (und für größere Systeme inhärent unvollständige) Methoden zur Validierung durch formale Verifikation zu ersetzen.

Neben der Verifikation reiner Hardware- bzw. reiner Softwarekomponenten besteht eine große Herausforderung in der Verifikation heterogener Systeme bzw. in der Betrachtung Eingebetteter Systeme in ihrer Interaktion mit einem physikalischen Umfeld. Entsprechende Modelle sind Hybride Systeme oder gezeitete Systeme. Hybride Systeme bestehen aus interagierenden diskreten und kontinuierlichen Komponenten. Man findet sie häufig auch in sicherheitskritischen Anwendungen wie in der Luft- und Raumfahrt (z.B. bei der Steuerung der Landeklappen eines Flugzeugs), der Bahnregelung (z.B. bei Zugsicherungs- und Leitsystemen) oder in der Chemietechnik. Kontinuierliche Komponenten sind dabei gekennzeichnet durch physikalische Größen wie Geschwindigkeit, Beschleunigung, Temperatur etc., die sich nach physikalischen Gesetzmäßigkeiten kontinuierlich ändern können. Diskrete Komponenten wie Eingebettete Mikrocontroller steuern die kontinuierlichen Komponenten durch ihr diskretes Schaltverhalten. Die Aufgabe besteht nun darin, die korrekte Interaktion der diskreten Steuerung mit der kontinuierlichen Umgebung nachzuweisen.

Die in diesem Vortrag betrachteten Hybriden Systeme sind gegeben durch bedingte Zuweisungen an diskrete und kontinuierliche Variablen (zur Modellierung diskreter Komponenten mit Controllern, Sensoren und Aktoren) und durch eine Menge von (einfachen) Differentialgleichungen (zur Modellierung der kontinuierlichen Umgebung). Im Gegensatz zu Standardansätzen, die solche Systeme in flache Lineare Hybride Automaten (LHAs) übersetzen, führen wir eine Verifikation auf der Basis symbolischer Darstellungen durch, um - speziell bei nicht-trivialen diskreten Komponenten - das enorme Anwachsen der Darstellung bei der Übersetzung in flache Automaten zu verhindern. Auch die Repräsentation von Zustandsräumen bei der Verifikation erfolgt mit symbolischen  Methoden.