Projekte

Formale Spezifikation und Verifikation von Timed Automata (RABBIT)

(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

Unsere Webseite verwendet Cookies. Diese haben zwei Funktionen: Zum einen sind sie erforderlich für die grundlegende Funktionalität unserer Website. Zum anderen können wir mit Hilfe der Cookies unsere Inhalte für Sie immer weiter verbessern. Hierzu werden pseudonymisierte Daten von Website-Besuchern gesammelt und ausgewertet. Das Einverständnis in die Verwendung der technisch nicht notwendigen Cookies können Sie jeder Zeit wiederrufen. Weitere Informationen erhalten Sie auf unseren Seiten zum Datenschutz.

Erforderlich

Diese Cookies werden für eine reibungslose Funktion unserer Website benötigt.

Statistik

Für den Zweck der Statistik betreiben wir die Plattform Matomo, auf der mittels pseudonymisierter Daten von Websitenutzern der Nutzerfluss analysiert und beurteilt werden kann. Dies gibt uns die Möglichkeit Websiteinhalte zu optimieren.

Name Zweck Ablauf Typ Anbieter
_pk_id Wird verwendet, um ein paar Details über den Benutzer wie die eindeutige Besucher-ID zu speichern. 13 Monate HTML Matomo
_pk_ref Wird benutzt, um die Informationen der Herkunftswebsite des Benutzers zu speichern. 6 Monate HTML Matomo
_pk_ses Kurzzeitiges Cookie, um vorübergehende Daten des Besuchs zu speichern. 30 Minuten HTML Matomo