Spezifikation und Verifikation objektorientierter Design-Patterns im Kontext nebenläufiger Objektsemantiken
Zusammenfassung der Projektergebnisse
Im Rahmen des Projekts COPY haben wir das Verhalten von objekt-orientierten Design Patterns im nebenläufigen Kontext formal untersucht. Hierfür haben wir die deklarative Spezifikationssprache ReActor entwickelt, mit der aktorbasierte Entwurfsmustervarianten mathematisch präzise und programmiersprachenunabhängig spezifiziert werden können. Unsere Sprache unterstützt Klassenbeschreibungen, dynamische Objektstrukturen und asynchrone Nachrichtenkommunikation. Wir haben für die Syntax der Sprache eine grafische, schemabasierte Variante und eine textbasierte, maschinenlesbare Variante definiert, die in ihrer Ausdrucksmächtigkeit äquivalent sind. Ferner haben wir im Projekt eine operationale Semantik für ReActor entwickelt, die es erlaubt, die Bedeutung einer ReActor-Spezifikation in Form einer TLA-Spezifikation anzugeben. Die Semantik bildet den mathematischen Unterbau für eine von uns entwickelte Werkzeugumgebung zur Verifikation von ReActor-Spezifikationen. Wir konzipierten und implementierten einen Übersetzer, mit dem eine ReActor-Spezifikation in die Eingabesprache des Model-Checkers TLC übersetzt und dort auf wichtige Eigenschaften hin überprüft werden kann. Die Übersetzung erfolgt strukturerhaltend, so dass durch TLC aufgedeckte Fehler auf die ursprüngliche ReActor-Spezifikation leicht zurückgespielt werden können. Unsere Verifikationskomponente erfordert eine Beschränkung des Zustandsraums, die bei unserem Verfahren in einem separaten Konfiguratlonsmodul für eine ReActor-Beschreibung vom Nutzer angegeben wird. Zusätzlich haben wir die Effizienz der Verifikation dadurch verbessert, dass wir ein Speichermanagement für Aktorobjekte implementiert haben. Die entwickelte Spezifikationssprache und die dazugehörige Werkzeugumgebung wurden anhand von mehreren Entwurfsmustern evaluiert.
Projektbezogene Publikationen (Auswahl)
- LLVM2CSP : Extracting CSP models from concurrent programs. In: Proceedings of the Nasa Formal Methods Symposium. Springer, 2011, S. 500 - 505
Moritz Kleine, Björn Bartels, Thomas Göthel, Steffen Helke und Dirk Prenzel
(Siehe online unter https://dx.doi.org/10.1007/978-3-642-20398-5_39) - Refactoring object-oriented specifications with inheritance-based polymorphism. In: Proceedings of the 5th international Conference on Theoretical Aspects of Software Engineering (Hg. Z. Duan und C.-H. Luke Ong). IEEE CS Press 2011, S. 35 - 41
Graeme Smith und Steffen Helke
(Siehe online unter https://dx.doi.org/10.1109/TASE.2011.31) - The observer pattern applied to actor systems: ATLA/TLC-based implementation analysis. In: Proceedings of the 6th International Conference on Theoretical Aspects of Software Engineering (Hg. T. Margaria, Z. Qiu und H. Yang). IEEE CS Press 2012, S. 193 - 200
Rodger Burmeister und Steffen Helke
(Siehe online unter https://dx.doi.org/10.1109/TASE.2012.15) - Towards static modular software verification. In: Tagungsband der Konferenz Software Engineering (SE 2012). Gesellschaft für Informatik 2012, S. 147-153
Marcus Mews und Steffen Helke
- ReActor: A notation for the specification of actor systenns and its semantics, in: Tagungsband der Konferenz Software Engineering (SE 2013). Gesellschaft für Informatik 2014, S. 127 - 142
Rodger Burmeister
