Formale Verifikation von exogenen Koodinationsmodellen

Abstract

In dieser Arbeit wird ein ganzheitlicher Ansatz zur Modellierung, Analyse und Synthese paralleler Systeme vorgestellt, welcher auf ausgewählten, aus der Literatur bekannten Formalismen aufbaut. Ziel ist die systematische und stringente Einbettung von Koordinationsaspekten. Der hier beschriebene Ansatz erlaubt es, das operationelle Systemverhalten auf beliebiger Ebene des Hardware-/Softwarestacks sowie die Interaktion und das komplexe Zusammenspiel unterschiedlicher Teilsysteme verschiedener Ebenen zu beschreiben und mithilfe formaler Methoden zu analysieren. Aufgrund der Komplexität moderner Hardware- und Softwaresysteme wurde ein hierarchischer Ansatz gewählt, welcher es erlaubt die Beschreibung komplexen Systemverhaltens auf mehrere Teilsysteme geringerer Komplexität zu verteilen. Die Interaktion und Kommunikation zwischen den Komponenten basiert hierbei auf der exogenen und kanalbasierten Koordinationssprache Reo. Diese unterstützt eine klare Trennung der Berechnung, welche durch die Komponenten durchgeführt wird, und der Koordination, welche durch ein Netzwerk aus synchronen und asynchronen Kanälen sichergestellt wird.