Geplante Arbeiten: abstrakte Schicht

Diese Schicht modelliert das Gesamtsystem (bestehend aus dem zu realisierenden System und der steuernden Umgebung), u. a. mittels hybrider Automaten. Typischerweise wird dabei das zu modellierende kontinuierliche Verhalten unter anderem über Differentialgleichungen definiert werden. Dabei sollen existierende Spezifikationsmethodiken (z.B. Beschreibung der Umgebung und der Regelalgorithmen nach in der Regelungstechnik üblichen Verfahren) leicht angebunden werden können.

Im Falle einfacher Differentialgleichungen bieten sich Werkzeuge wie HyTech, Uppaal und Kronos an, sowie ein gegenwärtig am DFKI entwickelter und implementierter Prüfer symbolischer Modelle, der im Rahmen des Arbeitspakets 3 weiterentwickelt und auf die Bedürfnisse des Projekts zugeschnitten wird. Für komplexere Differentialgleichungen hingegen muß auf interaktive Systeme zurückgegriffen werden, in denen komplexere Computer-Algebra-Methoden implementiert sind.

Die grundsätzliche Idee hinter dieser abstrakten Sicht liegt dabei darin, schon in frühen Phasen des Entwicklungsprozesses Fehler zu finden und auszumerzen.

Zusätzlich zu den oben genannten Spezifikationsmethoden bieten sich Realtime-Designmodelle wie Zustands- und Verlaufsdiagramme zur Spezifikation derartiger ressourcenbehafteter Modelle an. Anforderungen, wie z.B. die Einhaltung von Fristen, lassen sich dann über eine Übersetzung in zeitabhängige Automaten und anschließende Verifikation mittels Werkzeuge wie HyTech, Uppaal und Kronos nachweisen. Zu diesem Zweck wird gegenwärtig an der TU Dresden an einem automatischen Übersetzer gearbeitet, der in SuReal im Rahmen des Arbeitspakets 3 angepaßt und erweitert werden soll.

Als Beispielanwendung stelle man sich eine in einem Fahrzeug installierte radargestützte Abstandserfassung vor, mit deren Hilfe die relative Geschwindigkeit zum vorausfahrenden Fahrzeug ermittelt werden kann. Zu automatisieren ist das situationsabhängige automatische Bremsen oder Beschleunigen des Fahrzeugs. Eine mögliche zu verifizierende Anfrage an das Modell wäre beispielsweise die maximal zulässige Antwortzeit der beteiligten Systeme, bei der ein Auffahren verhindert wird. In Arbeitspaket 4 sollen in diesem Zusammenhang die zur Anwendung kommenden Beschreibungstechniken analysiert und miteinander verknüpft werden.

Allgemein sollten Grenzen der Lösungsräume ermittelt werden, die Aussagen über die sichere Einhaltung bzw. Verletzung der Realzeitanforderungen erlauben. Die Grenzen sollen dabei nicht nur als Beispielszenarien innerhalb des Lösungsraums dienen, sondern auch als eine Menge von Einschränkungen vorliegen, die wechselseitige Abhängigkeiten und engere Grenzen aufgrund von Wiederverwendung berücksichtigen.

Zusätzlich sollen im Falle von Beispielszenarien außerhalb des Lösungsraums die kritischen Pfade identifiziert werden können, d.h. die Stellen, an denen durch Optimierung einzelner oder mehrerer lokaler Gegebenheiten unmittelbar eine globale Verbesserung erreicht wird.

Eine Möglichkeit ist auch, für bestimmte Komponenten Obergrenzen des Ressourcenverbrauchs (Laufzeit) festzulegen und an die unteren Schichten als Beweisverpflichtung weiterzuleiten. Auch in diesem Fall kommen die Ergebnisse des Arbeitspakets 4 zusammen mit den Verfeinerungsbeweisen aus Teilen des Arbeitspakets 5 ins Spiel.

· Zwischenschichten