Projektstart: 01.05.2004

?

Projekttr?ger: Universit?t Augsburg

?

Projektverantwortung vor Ort: Dr. Peter H?fner

?

Beteiligte WissenschaftlerInnen der Universit?t Augsburg:?Prof. Dr. Bernhard M?ller

?

Beteiligte WissenschaftlerInnen / Kooperationen: Dr. Georg Struth (威尼斯赌博游戏_威尼斯赌博app-【官网】 of Sheffield)

?

?

Zusammenfassung

Hybride Systeme - heterogene Systeme die sowohl diskrete als auch kontinuierliche Komponenten beinhalten - werden dazu verwendet um sicherheitskritische Systeme zu beschreiben. Sie haben zahlreiche Anwendungen welche von Kontrollsystemen bis hin zu biologischen Prozessen reichen.
Die Forschungsziele umfassen grundlegende Methoden zur Analyse hybrider Systeme und die Entwicklung einer koh?renten Familie?algebraischer Kalküle für hybride Systeme

?

?

Beschreibung

Fehlerhafte Software hat in den letzten Jahrzehnten zahlreiche Menschenleben gefordert, Umweltsch?den hervorgerufen und regelm??ig zu enormen wirtschaftlichen Verlusten geführt. Besonders fehleranf?llig sind hierbei Systeme, welche st?ndig mit ihrer Umwelt interagieren, da sie auf diese flexibel, aber dennoch vorhersagbar reagieren müssen. Anders als für reine Softwaresysteme wie Büroanwendungen, sind Korrektheitsanforderungen in diesen Bereichen besonders hoch --- ein Airbag, der sich zu sp?t ?ffnet, ist nicht akzeptabel.
Solche sicherheitskritische Systeme k?nnen meistens als so genannte hybride Systeme charakterisiert werden. Bei diesen Systemen besteht ein Wechselspiel zwischenkontinuierlichem Systemverhalten und Kontrollereignissen zu diskreten Zeitpunkten, die Zustandswechsel ausl?sen. Anwendungsgebiete reichen von Steuerungselementen über 威尼斯赌博游戏_威尼斯赌博app-【官网】izintechnik bis hin zu Avionik. Aber auch chemische und biologische Systeme k?nnen mittels solcher Systeme mathematisch exakt beschrieben werden.
Hybride Systeme sind jedoch h?ufig so komplex, dass eine computergestützte Verifikation auch mit den heute verfügbaren gro?en Speicher- und Rechenkapazit?ten nicht durchführbar ist. Ziel der Arbeiten sind Untersuchungen zu einer kompakteren Behandlungsm?glichkeit von Verifikationsaufgaben. Zentrales Interesse finden hierbei algebraische Techniken, in denen Systeme durch Gleichungsregeln --- ?hnlich den aus der Schulalgebra bekannten --- beschrieben werden. Die generellen Vorteile eines algebraischen Ansatzes sind vor allem Klarheit und Einfachheit, insbesondere im Hinblick auf (computerunterstützbare) Rechenregeln. Die entwickelte algebraische Charakterisierung hybrider Systeme erm?glicht es beispielsweise, Sicherheitsaspekte mittels einfacher algebraischer Umformungen zu überprüfen. Ferner bietet dieser Ansatz den Vorteil, dass Standard-Computer-Algebrasysteme verwendet werden k?nnen. So k?nnen Theorembeweiser eingesetzt werden, um fundamentale Eigenschaften hybrider Systeme automatisch zu verifizieren.
Im letzten Jahrzehnt wurden Dutzende unterschiedlicher Logiken für hybride Systeme eingesetzt: Angefangen von klassischer Aussagenlogik über modale und temporale Logiken bis hin zu eigens für diese Systeme entwickelten Logiken. Die meisten dieser Logiken sind für sich wohlverstanden. Aber auf Grund der Vielzahl der verwendeten Begriffe sowie ihrer unterschiedlichen Notation und Bedeutung ist eine uniforme Behandlung der Logiken und ihrer Beziehungen zueinander sehr schwierig. In der vorliegenden Arbeit werden daher Untersuchungen zu einer kompakteren und einheitlichen Behandlung angestellt. Zentrales Interesse finden hierbei dieselben algebraischen Techniken wie zur Beschreibung von hybriden Systemen. Durch Algebraisierung ist es m?glich, Beziehungen zwischen Logiken aufzuzeigen und, für diese Arbeit von besonderer Bedeutung, diese Logiken in einer einheitlichen und systematischen Weise auf hybride Systeme anzuwenden.
Die Forschungsergebnisse umfassen grundlegende Methoden zur Analyse hybrider Systeme und münden bereits in eine koh?rente Familie?algebraischer Kalküle für hybride Systeme. Die Anwendbarkeit und Relevanz der Theorie ist durch erste Fallstudien belegt.