Modeling and verifying dynamic evolving service-oriented architectures

Mehr zum Buch

Service-Orientierte Architekturen ermöglichen die dynamische Zusammensetzung und Rekonfiguration komplexer IT-Landschaften durch die Bindung von Service Contracts zur Laufzeit, das Starten neuer Komponenten und das Beenden veralteter. Die Evolution dieser Systeme umfasst nicht nur den Austausch von Komponenten-Implementierungen, sondern auch das Hinzufügen neuer Service-Contracts. Aktuelle Ansätze zur Modellierung und Verifikation unterstützen diese Eigenschaften oft nur unvollständig. In diesem Bericht präsentieren wir eine Erweiterung des OMG-Vorschlags zur Service-Modellierung mit UML - SoaML - die diese Einschränkungen beseitigt. Unser Ansatz ermöglicht die Modellierung von Service Contracts auf verschiedenen Abstraktionsniveaus und bietet eine fundierte formale Semantik für alle Modellierungskonzepte sowie die Verifikation kritischer Eigenschaften. Der kompositionale und inkrementelle Verifikationsansatz erlaubt die Überprüfung komplexer Eigenschaften, einschließlich Kommunikationsparameter und Zeit. Er deckt die dynamische Bindung von Service Contracts, den Austausch von Komponenten und die Evolution des Systems durch das Hinzufügen neuer Service Contracts ab. Die Modellierungs- und Verifikationsfähigkeiten unseres Ansatzes werden durch ein Beispiel aus dem Lieferkettenmanagement veranschaulicht.