@TechReport{BGN09-TR,
AUTHOR = {Becker, Basil and Giese, Holger and Neumann, Stefan},
TITLE = {{Correct Dynamic Service-Oriented Architectures: Modeling and Compositional Verification with Dynamic Collaborations}},
YEAR = {2009},
NUMBER = {29},
INSTITUTION = {Hasso Plattner Institute at the University of Potsdam},
PDF = {uploads/pdf/BGN09-TR_techreport.pdf},
ABSTRACT = {Service-oriented modeling employs collaborations to capture the coordination of multiple roles in form of service contracts. In case of dynamic collaborations the roles may join and leave the collaboration at runtime and therefore complex structural dynamics can result, which makes it very hard to ensure their correct and safe operation. We present in this paper our approach for modeling and verifying such dynamic collaborations. Modeling is supported using a well-defined subset of UML class diagrams, behavioral rules for the structural dynamics, and UML state machines for the role behavior. To be also able to verify the resulting service-oriented systems, we extended our former results for the automated verification of systems with structural dynamics and developed a compositional reasoning scheme, which enables the reuse of verification results. We outline our approach using the example of autonomous vehicles that use such dynamic collaborations via ad-hoc networking to coordinate and optimize their joint behavior.}
}