Kompositionale Analyse Komponenten-basierter Systeme mittels Cross-Checking

Applicant Professorin Dr. Mila Majster-Cederbaum
Subject Area Software Engineering and Programming Languages
Term from 2011 to 2015
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 175932198
 

Final Report

Final Report Year 2018

Final Report Abstract

In dem Projekt geht es um den Nachweis generischer Eigenschaften kooperierender Systeme wie Erreichbarkeit, Verklemmungsfreiheit und Fortschritt. Basierend auf einem Modell für Komponenten-basierte Systeme wurden verschiedene Fragen behandelt. Es wurde u.a. gezeigt, dass die Einschränkung der Architektur des Systems auf hierarchische, sternförmige oder lineare Strukturen die Komplexität grundlegender Fragen wie Erreichbarkeit oder Verklemmungsfreiheit nicht reduziert, sie bleibt PSPACE-vollständig. Weiter führten wir eine Methode zur Erzeugung geeigneter Überapproximationen des Systems ein, die nicht nur die Zustände sondern auch die Zustandsübergänge berücksichtigt. Um diese zu gewinnen, wird ausgehend von einer Familie von sog. abstrakten Überapproximationen der Fixpunkt bezüglich eines neu definierten Operators (Edge Match) berechnet. Das Ergebnis dient der Überprüfung von safety properties. Eine Implementierung mittels BDDs wurde vorgenommen und einige Case Studies durchgeführt. Des Weiteren wurde der Zusammenhang zur Relationalen Algebra untersucht. Es konnte u.a. gezeigt werden, dass sich der Edge Match Operator durch Operation der Relationalen Algebra darstellen lässt.

Publications

DFG Programme Research Grants