(2000-2003)

Die Konstruktion eingebetteter Systeme, die starke Realzeit-Anforderungen zu erfüllen haben, wird in den verschiedensten Anwendungsbereichen immer bedeutsamer, z. B. in der Medizin, der Transporttechnik oder der Produktions­automatisierung. Formale Methoden unterstützen die fehlerarme Entwicklung solcher Systeme, weil sie auf einer präzisen mathematischen Grundlage aufbauen. Im Projekt RABBIT wurden mit der Sprache CTA ein geeigneter Modellierungsformalismus und effiziente Verifikationsverfahren für den Einsatz einer formalen Methode zur Spezifikation von Realzeitsystemen entwickelt. Durch die Einführung eines Modulkonzepts wird die Modellierung auch großer Realzeit-Systeme systematisch unterstützt. Für die Verifikation werden effiziente BDD-basierte Algorithmen verwendet, wobei auch das Problem des Findens guter BDD-Variablenordnungen gelöst wird. Damit ist eine drastische Reduktion der Größe des explizit zu repräsentierenden Zustandsraums möglich.

Es werden sowohl Erreichbarkeitsanalyse als auch Verfeinerungsanalyse unterstützt. Die Praktikabilität der Ansätze zur Modellierung und Verifikation wurden in verschiedenen Fallstudien aus den Bereichen der reaktiven Systeme und der Kommunikationsprotokolle demonstriert.

Projektbeschreibung