Kompositionale Analyse Komponenten-basierter Systeme mittels Cross-Checking
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
- Reachability in Tree-Like Component Systems is PSPACE-Complete, ENTCS, 263:197-210
Mila Majster-Cederbaum, Nils Semmelrock
(See online at https://doi.org/10.1016/j.entcs.2010.05.012) - 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
(See online at https://doi.org/10.1007/s10703-012-0160-6) - 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
(See online at https://doi.org/10.1016/j.scico.2013.02.006) - Reachability in Cooperating Systems with Architectural Constraints is PSPACE-Complete, GRAPHITE 2013
Mila Majster-Cederbaum, Nils Semmelrock
(See online at https://doi.org/10.4204/EPTCS.138.1) - Formalizing Selfadaptive Clouds with KnowLang. ISoLA (1) 2014: 117-130
Emil Vassev, Mike Hinchey, Philip Mayer
(See online at https://doi.org/10.1007/978-3-662-45234-9_9) - 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
(See online at https://doi.org/10.1016/j.scico.2014.07.006) - An Empirical Analysis of the Utilization of Multiple Programming Languages in Open Source Projects. EASE, 2015
Philip Mayer, Alexander Bauer
(See online at https://doi.org/10.1145/2745802.2745805) - A taxonomy of cross-language linking mechanisms in open source frameworks. Computing 99:701– 724, 2017
Philip Mayer
(See online at https://doi.org/10.1007/s00607-016-0528-3)
