Kompositionale Analyse Komponenten-basierter Systeme mittels Cross-Checking

• Antragstellerin: Professorin Dr. Mila Majster-Cederbaum
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2011 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 175932198

• Erstellungsjahr: 2018

Zusammenfassung der Projektergebnisse

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.

Projektbezogene Publikationen (Auswahl)

• Reachability in Tree-Like Component Systems is PSPACE-Complete, ENTCS, 263:197-210
  Mila Majster-Cederbaum, Nils Semmelrock
  
• Analysis of Cooperating Systems by Refined Over-Approximations (Extended Abstract), FACS 2011
  Nils Semmelrock
  
• A Refinement Technique for Overlapping Over-Approximations of Cooperating Systems, SOFSEM 2012
  Nils Semmelrock
  
• Deadlock-freedom in Component Systems with Architectural constraints. Formal Methods in System Design 41(2): 129-177 (2012)
  Moritz Martens, Mila Majster-Cederbaum
  
• Software Components and Formal Methods from a Computational Viewpoint, Dissertation, Universität Mannheim 2012
  Christian Lambertz
  
• Complexity Results for Cooperating Systems and Approximated Reachability by Abstract Over-Approximations, Dissertation, Universität Mannheim 2013
  Nils Semmelrock
  
• Efficient Deadlock Analysis of Component-based Software Architectures. Sci. Comput. Program. 78(12): 2488-2510 (2013)
  Christian Lambertz, Mila E. Majster-Cederbaum
  
• Reachability in Cooperating Systems with Architectural Constraints is PSPACE-Complete, GRAPHITE 2013
  Mila Majster-Cederbaum, Nils Semmelrock
  
• Formalizing Selfadaptive Clouds with KnowLang. ISoLA (1) 2014: 117-130
  Emil Vassev, Mike Hinchey, Philip Mayer
  
• A basis for compositionally ensuring safety properties and its connection to relational algebraic operators. Sci. Comput. Program. 98:516- 530, 2015
  Mila Majster-Cederbaum, Nils Semmelrock
  
• An Empirical Analysis of the Utilization of Multiple Programming Languages in Open Source Projects. EASE, 2015
  Philip Mayer, Alexander Bauer
  
• A taxonomy of cross-language linking mechanisms in open source frameworks. Computing 99:701– 724, 2017
  Philip Mayer