Die Dozenten der Informatik-Institute der Technischen Universität Braunschweig laden im Rahmen des Informatik-Kolloquiums zu folgendem Vortrag ein:
Prof. Dr. Ernst-Rüdiger Olderog, Department für Informatik, Universität Oldenburg: Automatische Verifikation kombinierter Spezifikationen
Beginn: 18.06.2007, 17:00 Uhr Ort: TU Braunschweig, Informatikzentrum, Mühlenpfordtstraße 23, 1. OG, Hörsaal M 160 Webseite: http://www.ibr.cs.tu-bs.de/cal/kolloq/2007-06-18-olderog.html Kontakt: Prof. Dr. Ursula Goltz
Wir berichten über Forschungen im Projekt "Beyond Timed Automata" des Transregio-SFB "Automatic Verification and Analysis of Complex Systems" (AVACS), an dem die Universitäten Oldenburg, Freiburg und Saarbrücken beteiligt sind.
In diesem Projekt geht es darum, automatisch Sicherheitseigenschaften höherer System-Spezifikationen mit den Dimensionen Prozessverhalten, Daten und Realzeit nachzuweisen. Dabei liegt das Augenmerk darauf, Systeme mit unendlichen Datenbereichen und Realzeit-Bedingungen automatisch behandeln zu können und somit über die Möglichkeiten von Realzeitautomaten (Timed Automata) hinauszugehen. Als Spezifikationssprache wird CSP-OZ-DC betrachtet, eine Kombination von Konzepten aus Communicating Sequential Processes (CSP), Object-Z (OZ) und dem Duration Calculus (DC). Diese Kombination hat eine kompositionelle Semantik als Parallelkombination von Phasen-Event-Automaten, die sich sehr gut als Zwischendarstellung bei der Übersetzung von CSP-OZ-DC in die Eingabesprache eines Abstraction Refinement Model Checkers (ARMC) eignen. Mit ARMC lässt sich die Erreichbarkeit von Zustandsmengen automatisch überprüfen.
Wir illustrieren den Ansatz an Hand von zwei Fallstudien: einem parametrischen Fahrstuhl und einer Steuerung aus der Anwendungsdomäne von AVACS, dem European Train Control System (ETCS).