Prof. Dr. Franz Josef Rammig

»Nicht nur in Realzeitsystemen, sondern auch beim Transfer wissenschaftlicher Erkenntnisse in die Praxis spielt Zeit eine zentrale Rolle. Ein zu spät vorliegendes Ergebnis ist oft wertlos. In der schnelllebigen Informatik gilt es, unsere wissenschaftlichen Erkenntnisse unmittelbar praktisch umzusetzen.«

Freitag, 10. Februar 2012 10.02.12 12:06 Alter: 6 Jahre

Der Unendlichkeit eine Grenze setzen
Sichere Navigation in komplexen Systemen

Foto (Jana Neuhaus): Graphabstraktion anschaulich: Dominik Steenken und Steffen Ziegert (rechts) bei Planung und Fehlervermeidung

Können Navigationsnetze mit unendlich vielen Systemzuständen sicher programmiert werden? So sicher, dass sie jederzeit allen Sicherheitsanforderungen standhalten? Schwierig.

Neue Verkehrssysteme bei ständig steigendem Verkehrsaufkommen – sie müssen effizient, rentabel und sicher sein. Eine Lösung ist das Paderborner RailCab-System. Die Entwicklung ist jedoch komplex, Zuverlässigkeit und Sicherheit der Navigationssoftware müssen garantiert werden: Nicht nur bei der Anwendung in Verkehrssystemen, sondern generell bei der Kommunikation in vernetzten Strukturen. Herkömmliche Software-Tests können bei großen komplexen Systemen nicht alle potentiellen Fehler aufdecken. Mehr Sicherheit bieten Verifikationen. Sie sind jedoch sehr aufwändig und bei unbegrenzten Systemzuständen vom Menschen nicht zu bewältigen.

Noch einmal: Kann man sicherheitskritische Systeme mit unendlich vielen denkbaren Fehlern sicher programmieren? Man kann! Die Arbeitsgruppe um Prof. Wehrheim nutzt Techniken, die auf Model Driven Software Development (MDSD) aufsetzen, einem Entwicklungskonzept für komplexe Software-Systeme. Das Ziel von MDSD ist, mittels formaler Techniken aus abstrakten Modellen direkt funktionstüchtige Software zu generieren.

Reale Navigationsszenarien bieten extrem viele Möglichkeiten, aus denen uneffektives Verhalten oder sogar Gefahrensituationen entstehen können. Mitarbeiter Dominik Steenken versucht zu garantieren, dass solche Fehler von Beginn an vermieden werden und nutzt dafür die Shape-Analyse: Um die unendlich große Anzahl möglicher Zustände verifizieren zu können, vereinfacht er rechnerisch die Graphenstruktur zu einem abstrakten Modell. Dabei ist die Abstraktionsebene flexibel und an das jeweilige Problem anpassbar. Gleichzeitig muss der Computer sinnvolle Strukturen erkennen: Er darf weder zu wenig abstrahieren – dann bleibt der Zustandsraum unendlich. Noch darf er zu viel abstrahieren, denn dann wären wichtige Eigenschaften nicht mehr verifizierbar. Unendliche Graphen realer Szenarien lassen sich drastisch in der Größe reduzieren und als endliche Strukturen repräsentieren. Da die Ergebnisse aus dem abstrahierten Modell auch für das ursprüngliche, konkrete Modell gelten, können Gefahrensituationen bereits während des Entwicklungsprozesses erkannt und beseitigt werden.

Während Steenken sicherstellt, dass das System keine gefährlichen Zustände wie z.B. Kollisionen enthält, optimiert Mitarbeiter Steffen Ziegert Abfolgen von Zuständen hinsichtlich ökonomischer Aspekte. Er betrachtet konkrete Graphen bzw. Systemzustände und plant zukünftiges Verhalten. Ein komplexes Vorhaben, da er verschiedene Faktoren beachten muss: Welches Verhalten ist angebracht, um möglichst schnell ein bestimmtes Ziel zu erreichen? Wie kann energiesparsam gefahren und der Komfort gleich-zeitig beibehalten werden? Wie können unter diesen Aspekten Konvois gebildet und Konflikte vermieden werden? Im Gegensatz zur Verifikation plant Ziegert zur Laufzeit: Während das System in Betrieb ist, muss das Verhalten aller Teilnehmer permanent einkalkuliert werden.

Nicht nur die Navigation des RailCab wird mit diesen Methoden wesentlich verbessert. Durch die Planung und die Vermeidung von Fehlern können komplexe Systeme generell sicher und effektiv befahren werden. Auch andere Systeme wie z.B. Maschinenbau, Automobilindustrie oder Medizintechnik profitieren von den Ergebnissen.

Die Arbeiten sind Bestandteil des Teilprojekts B1 des „SFB 614 – Selbstoptimierende Systeme des Maschinenbaus“.


Kontakt:
Prof. Dr. Heike Wehrheim
Spezifikation und Modellierung von
Softwaresystemen
05251 60-4331
wehrheim(at)uni-paderborn.de


Kontakt: Patrizia Höfer, Institut für Informatik, 05251 60-3341, hoefer[at]upb.de