@TechReport{BeckerG2013,
AUTHOR = {Becker, Basil and Giese, Holger},
TITLE = {{Modeling and Verifying Dynamic Evolving Service-Oriented Architectures}},
YEAR = {2013},
NUMBER = {75},
INSTITUTION = {Hasso Plattner Institute at the University of Potsdam},
PDF = {uploads/pdf/BeckerG2013_report.pdf},
ABSTRACT = {The service-oriented architecture supports the dynamic assembly and runtime reconfiguration of complex open IT landscapes by means of runtime binding of service contracts, launching of new components and termination of outdated ones. Furthermore, the evolution of these IT landscapes is not restricted to exchanging components with other ones using the same service contracts, as new services contracts can be added as well. However, current approaches for modeling and verification of service-oriented architectures do not support these important capabilities to their full extend. In this report we present an extension of the current OMG proposal for service modeling with UML --- SoaML --- which overcomes these limitations. It permits modeling services and their service contracts at different levels of abstraction, provides a formal semantics for all modeling concepts, and enables verifying critical properties. Our compositional and incremental verification approach allows for complex properties including communication parameters and time and covers besides the dynamic binding of service contracts and the replacement of components also the evolution of the systems by means of new service contracts. The modeling as well as verification capabilities of the presented approach are demonstrated by means of a supply chain example and the verification results of a first prototype are shown.}
}