Correct dynamic service oriented architectures

More about the book

Bei der Modellierung service-orientierter Systeme werden Kollaborationen zur Beschreibung der Koordination mehrerer Rollen durch Service-Verträge eingesetzt. Dynamische Kollaborationen ermöglichen das Hinzufügen und Entfernen von Rollen zur Laufzeit, was komplexe strukturelle Dynamik erzeugt und die automatische Analyse erschwert. In dieser Arbeit präsentieren wir einen Ansatz zur Modellierung und Verifikation solcher dynamischen Kollaborationen. Eine spezielle Untermenge der UML wird verwendet, um Klassendiagramme, Verhaltensregeln für die strukturelle Dynamik und UML-Zustandsdiagramme für das Verhalten der Rollen zu modellieren. Um die Verifikation der modellierten Systeme zu ermöglichen, erweiterten wir frühere Ergebnisse zur Verifikation von Systemen mit struktureller Dynamik und entwickelten einen kompositionalen Verifikationsansatz, der die Wiederverwendung von Ergebnissen erlaubt. Die Techniken werden anhand autonomer Fahrzeuge veranschaulicht, die dynamische Kollaborationen über ad-hoc Netzwerke zur Koordination und Optimierung ihres Verhaltens nutzen. Unser Ansatz zielt darauf ab, die Herausforderungen der dynamischen Kollaborationen zu adressieren und die korrekte sowie sichere Funktionsweise dieser Systeme zu gewährleisten.