@phdthesis{Becker2013,
  author    = {Becker, Basil},
  title     = {Architectural modelling and verification of open service-oriented systems of systems},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-70158},
  school      = {Universit{\"a}t Potsdam},
  year      = {2013},
  abstract  = {Systems of Systems (SoS) have received a lot of attention recently. In this thesis we will focus on SoS that are built atop the techniques of Service-Oriented Architectures and thus combine the benefits and challenges of both paradigms. For this thesis we will understand SoS as ensembles of single autonomous systems that are integrated to a larger system, the SoS. The interesting fact about these systems is that the previously isolated systems are still maintained, improved and developed on their own. Structural dynamics is an issue in SoS, as at every point in time systems can join and leave the ensemble. This and the fact that the cooperation among the constituent systems is not necessarily observable means that we will consider these systems as open systems. Of course, the system has a clear boundary at each point in time, but this can only be identified by halting the complete SoS. However, halting a system of that size is practically impossible. Often SoS are combinations of software systems and physical systems. Hence a failure in the software system can have a serious physical impact what makes an SoS of this kind easily a safety-critical system. The contribution of this thesis is a modelling approach that extends OMG's SoaML and basically relies on collaborations and roles as an abstraction layer above the components. This will allow us to describe SoS at an architectural level. We will also give a formal semantics for our modelling approach which employs hybrid graph-transformation systems. The modelling approach is accompanied by a modular verification scheme that will be able to cope with the complexity constraints implied by the SoS' structural dynamics and size. Building such autonomous systems as SoS without evolution at the architectural level --- i. e. adding and removing of components and services --- is inadequate. Therefore our approach directly supports the modelling and verification of evolution.},
  language  = {en}
}
@book{BeckerGieseNeumann2009,
  author    = {Becker, Basil and Giese, Holger and Neumann, Stefan},
  title     = {Correct dynamic service-oriented architectures : modeling and compositional verification with dynamic collaborations},
  organization    = {System Analysis and Modeling Group},
  isbn      = {978-3-940793-91-1},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-30473},
  publisher      = {Universit{\"a}t Potsdam},
  year      = {2009},
  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 [7, 8] 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.},
  language  = {en}
}
@book{BeckerGiese2012,
  author    = {Becker, Basil and Giese, Holger},
  title     = {Cyber-physical systems with dynamic structure : towards modeling and verification of inductive invariants},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-217-9},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-62437},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {iv, 27},
  year      = {2012},
  abstract  = {Cyber-physical systems achieve sophisticated system behavior exploring the tight interconnection of physical coupling present in classical engineering systems and information technology based coupling. A particular challenging case are systems where these cyber-physical systems are formed ad hoc according to the specific local topology, the available networking capabilities, and the goals and constraints of the subsystems captured by the information processing part. In this paper we present a formalism that permits to model the sketched class of cyber-physical systems. The ad hoc formation of tightly coupled subsystems of arbitrary size are specified using a UML-based graph transformation system approach. Differential equations are employed to define the resulting tightly coupled behavior. Together, both form hybrid graph transformation systems where the graph transformation rules define the discrete steps where the topology or modes may change, while the differential equations capture the continuous behavior in between such discrete changes. In addition, we demonstrate that automated analysis techniques known for timed graph transformation systems for inductive invariants can be extended to also cover the hybrid case for an expressive case of hybrid models where the formed tightly coupled subsystems are restricted to smaller local networks.},
  language  = {en}
}
@book{Becker2010,
  author    = {Becker, Basil},
  title     = {Model-based extension of AUTOSAR for architectural online reconfiguration},
  isbn      = {978-3-86956-036-6},
  year      = {2010},
  language  = {en}
}
@book{GieseBecker2013,
  author    = {Giese, Holger and Becker, Basil},
  title     = {Modeling and verifying dynamic evolving service-oriented architectures},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-246-9},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-65112},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {97},
  year      = {2013},
  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.},
  language  = {en}
}
@book{AlnemrPolyvyanyyAbuJarouretal.2010,
  author    = {Alnemr, Rehab and Polyvyanyy, Artem and AbuJarour, Mohammed and Appeltauer, Malte and Hildebrandt, Dieter and Thomas, Ivonne and Overdick, Hagen and Sch{\"o}bel, Michael and Uflacker, Matthias and Kluth, Stephan and Menzel, Michael and Schmidt, Alexander and Hagedorn, Benjamin and Pascalau, Emilian and Perscheid, Michael and Vogel, Thomas and Hentschel, Uwe and Feinbube, Frank and Kowark, Thomas and Tr{\"u}mper, Jonas and Vogel, Tobias and Becker, Basil},
  title     = {Proceedings of the 4th Ph.D. Retreat of the HPI Research School on Service-oriented Systems Engineering},
  editor    = {Meinel, Christoph and Plattner, Hasso and D{\"o}llner, J{\"u}rgen Roland Friedrich and Weske, Mathias and Polze, Andreas and Hirschfeld, Robert and Naumann, Felix and Giese, Holger},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-036-6},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-40838},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {Getr. Z{\"a}hlung},
  year      = {2010},
  language  = {en}
}