Formale Semantik modularer Zeitverfeinerung in AUTOFOCUS

Abstract

Moderne automobile eingebettete Systeme bilden hochkomplexe verteilte Steuergerätenetzwerke. Modellbasierte Entwicklung ist ein verbreiteter Ansatz, um dieser Komplexität zu begegnen. AUTOFOCUS ist ein CASE-Werkzeugprototyp zur formal fundierten modellbasierten Entwicklung eingebetteter Systeme. Ein Modell wird hierarchisch aus Komponenten aufgebaut, die über getypte Kanäle kommunizieren. AUTOFOCUS verfügt über eine robuste und übersichtliche formale Semantik: die Kommunikation und Ausführung sind über einen globalen Takt für alle Komponenten synchronisiert. In diesem Artikel stellen wir eine Erweiterung der AUTOFOCUS- Semantik um eine Zeitverfeinerung von Komponenten vor. Diese ermöglicht eine einfachere Modularisierung von Systemen, eine bessere Strukturierung von Verhaltensspezifikationen und eine bessere Abbildung auf die Zielplattform realer eingebetteter Systeme. Gleichzeitig bleiben die Vorteile fest getakteter AUTOFOCUS-Semantik wie starke Kausalität und sichere Terminierung von Berechnungsschritten erhalten.