Kompositionelle Synthese für komponentenbasierte Systeme (Statusvortrag)

Datum

23.08.2011

Zeit

13:00 - 14:00

Sprecher

Dipl.-Inform. Joachim Klein

Zugehörigkeit

Institut für Theoretische Informatik, Algebraische und logische Grundlagen der Informatik

Sprache

de

Hauptthema

Informatik

Andere Themen

Informatik

Beschreibung

Betreuerin: Prof. Dr. rer. nat. C. Baier Fachreferent: Prof. Dr.-Ing. habil. H. Vogler Formale Verifikationsmethoden, wie beispielsweise Model Checking, dienen der Unterstützung der Analyse und des Designs von immer komplexer werdenden, parallelen und verteilten Systemen. Die automatische Synthese geht einen Schritt weiter: Das klassische Syntheseproblem geht nur von einer formalen Spezifikation aus und fragt nach einem Systemmodell, welches diese erfüllt. Für einige logische Spezifikationsformalismen ist das Syntheseproblem algorithmisch durch automaten-basierte Verfahren zur Konstruktion eines Systemmodells, das eine gegebene Spezifikation erfüllt, lösbar. Der kompositionelle, komponentenbasierte Ansatz des Systemdesigns fördert wünschenswerte Designprinzipien, wie Informationskapselung, Austauschbarkeit und Wiederverwendbarkeit der Komponenten als den Bausteinen des Systems. Exogene Koordinationssprachen wie Reo erlauben dabei eine saubere Trennung zwischen den Berechnungen innerhalb der Komponenten und der Koordination zwischen den Komponenten mittels deren Schnittstellen. Eine Variante des klassischen Syntheseproblems in diesem Kontext ist die Frage nach der Existenz eines Controllers für die Koordination ausgewählter Komponenten, so dass das kontrollierte System die gewünschte Spezifikation erfüllt. Hierbei ist es wünschenswert, die schrittweise, inkrementelle Verfeinerung der Spezifikation durch die Synthese von Controllern für weitere kompatible Anforderungen zu ermöglichen. Dies setzt jedoch eine spezielle Form der in den vorherigen Schritten synthetisierten Controller voraus, nämlich dass diese "möglichst allgemein" sind und nicht vorzeitig mögliches Verhalten ausschließen, das in einem späteren Schritt benötigt werden könnte. Dieser Vortrag motiviert die Fragestellung und diskutiert den aktuellen Stand der relevanten Forschung, die Herausforderungen, die sich für ein kompositonelles Framework für die inkrementelle Controllersynthese ergeben sowie Lösungsansätze. Alle Interessenten sind herzlich eingeladen.

Letztmalig verändert: 23.08.2011, 09:36:06