Holger Giese

Thomas Vogel

Sebastian Wätzoldt

Towards Smart Systems of Systems *

Systems of Systems (SoS) have started to emerge as a consequence of the general trend toward the integration of beforehand isolated systems. To unleash the full potential, the contained systems must be able to operate as elements in open, dynamic, and deviating SoS architectures and to adapt to open and dynamic contexts while being developed, operated, evolved, and governed independently. We name the resulting advanced SoS to be smart as they must be self-adaptive at the level of the individual systems and self-organizing at the SoS level to cope with the emergent behavior at that level. In this paper we analyze the open challenges for the envisioned smart SoS. In addition, we discuss our ideas for tackling this vision with our SMARTSOS approach that employs open and adaptive collaborations and models at runtime. In particular, we focus on preliminary ideas for the construction and assurance of smart SoS.

Introduction

Systems of Systems (SoS) [START_REF] Maier | Architecting principles for systems-of-systems[END_REF][START_REF] Valerdi | A research agenda for systems of systems architecting[END_REF] nowadays become a highly relevant challenge as the general trend can be observed that beforehand isolated systems are integrated into larger federations of systems. To unleash the full potential of such federations, SoS must be smart such that the contained systems are able to operate as elements in open, dynamic, and deviating SoS architectures and to adapt to open and dynamic contexts while being developed, operated, evolved, and governed independently. 1 Therefore, the resulting smart SoS must be selfadaptive at the level of the individual systems and self-organizing at the SoS level to cope with the emergent behavior at that level.

For a smart SoS holds that each of its systems has to be independent in the sense that it is developed, operated, evolved, and governed independently from the other systems in the SoS. Furthermore, these systems interact with each other in an open and dynamic world (cf. [START_REF] Baresi | Toward Open-World Software: Issue and Challenges[END_REF]), which causes individual systems to dynamically join or leave the SoS over time, the SoS architecture to deviate, and emergent behavior at the SoS level. Moreover, each independent system must adapt its behavior autonomously according to its own needs and peer systems in the SoS (self-adaptation [START_REF] Cheng | Software Engineering for Self-Adaptive Systems: A Research Roadmap[END_REF][START_REF] De Lemos | Software Engineering for Self-Adaptive Systems: A second Research Roadmap[END_REF]) while considering the interplay between its own behavior, the other systems' behavior, and the required SoS-level behavior (self-organization [START_REF]Self-organising Software[END_REF]). The envisioned interaction between the systems involves independently developed systems and requires means for exchanging knowledge between these systems at runtime. This knowledge covers aspects of a running system itself and the context or the requirements of a running system. While the outlined rich interaction is key, the development of the systems has to scale and thus only can take into account the publically available knowledge about possible collaborations with the other systems. Finally, the systems as part of a smart SoS will evolve in order to adjust to new needs or changing regulations (cf. software evolution [START_REF] Mens | Software Evolution[END_REF]). Since it seems today improbable or even impossible that all the required evolution steps can be covered automatically by a system itself (e.g., by self-adaptation or self-organization), it must still be possible that required evolution steps for each individually governed system are performed during the operation of the SoS. These challenges for engineering smart SoS are currently hardly covered by the available approaches.

The current state of the art suggests constructing SoS using an architecture perspective and services (cf. [START_REF] Mittal | Model-driven systems engineering for netcentric system of systems with DEVS unified process[END_REF]) employing, for example, the Service oriented architecture Modeling Language (SoaML) [START_REF]Object Management Group (OMG): Service oriented architecture Modeling Language (SoaML) Specification, Version 1[END_REF] and the Unified Modeling Language (UML) [12] to specify the cooperation of systems by means of service contracts and collaborations. In these collaborations, roles with dedicated interfaces describe the behavior of the systems while the SoS-level behavior emerges from the interactions of these roles.

The use of collaborations for the modeling of services [START_REF] Sanders | Using UML 2.0 Collaborations for Compositional Service Specification[END_REF][START_REF] Broy | A formal model of services[END_REF], the use of class diagrams for the structure and graph transformations for the behavior modeling [START_REF] Baresi | Modeling and Validation of Service-Oriented Architectures: Application vs. Style[END_REF][START_REF] Baresi | Style-based modeling and refinement of service-oriented architectures[END_REF], and a formal model of ensembles [START_REF] Hölzl | Towards a System Model for Ensembles[END_REF] have been proposed. However, none of these approaches supports the construction of dynamic collaborations as required for smart SoS where systems dynamically join or leave the federation. And even though well-established formal approaches such as π-calculus [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF] or bigrahs [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF] tackle such structural dynamics, to the best of our knowledge no work exists that especially covers the problem of providing assurances for dynamic collaborations of arbitrary size. Either the approaches require an initial system configuration and only support finite state systems (or systems for which an abstract finite state model of moderate size exist) [START_REF] Baresi | Modeling and Validation of Service-Oriented Architectures: Application vs. Style[END_REF][START_REF] Varró | Automated formal verification of visual modeling languages by model checking[END_REF][START_REF] Rensink | Towards model checking graph grammars[END_REF][START_REF] Frias | DynAlloy: Upgrading Alloy with actions[END_REF][START_REF] Ölveczky | Specification and analysis of real-time systems using Real-Time Maude[END_REF][START_REF] Zhang | Modular verification of dynamically adaptive systems[END_REF] or they lack the expressive power to describe typical problems concerning the structural dynamics [START_REF] Baldan | A static analysis technique for graph transformation systems[END_REF][START_REF] Bauer | Static Analysis of Dynamic Communication Systems by Partner Abstraction[END_REF].

In our own Mechatronic UML approach (mUML) [START_REF] Burmester | Tool Support for the Design of Self-Optimizing Mechatronic Multi-Agent Systems[END_REF] for the modeldriven development of self-optimizing embedded real-time systems, we already support collaborations of self-optimizing autonomous systems in a rigorous manner by means of role protocols. For mUML and its collaboration concepts an overall assurance scheme has been presented in [START_REF] Giese | Model-Driven Development of Safe Self-Optimizing Mechatronic Systems with MechatronicUML[END_REF]: it combines a modular verification approach [START_REF] Giese | Modular Design and Verification of Component-Based Mechatronic Systems with Online-Reconfiguration[END_REF] for the component hierarchies of the autonomous systems, the compositional verification [START_REF] Giese | Towards the compositional verification of real-time uml designs[END_REF] of ad hoc real-time collaborations between the autonomous systems, and a fully automatic checker for inductive invariants of graph transformation system rules [START_REF] Becker | Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation[END_REF] describing the possible changes of the dynamic architecture at the SoS level. Additional work on assurances for mUML employs a multi-agent system view on an SoS to study how commitments between the collaborating systems can be modeled and analyzed [START_REF] Giese | Systematic verification of multi-agent systems based on rigorous executable specifications[END_REF]. Therefore, with mUML an approach exists that provides assurances for systems that combine self-adaptive autonomous systems similar to an SoS. However, in contrast to the challenges of smart SoS, which are discussed in the next section, mUML provides no solution for collaborations with structural dynamics of the roles, is restricted to homogeneous systems (i.e., systems that evolve jointly and similarly and that have complete knowledge about each other), and does not support the runtime exchange of complex knowledge. Moreover, the self-adaptation is limited to pre-planned reconfigurations in hierarchical architectures.

Our Executable Runtime Megamodels approach (EUREMA) [START_REF] Vogel | Model-Driven Engineering of Self-Adaptive Software with EUREMA[END_REF] for the model-driven engineering of self-adaptive systems supports -in contrast to mUML -the flexible specification of self-adaptation by allowing us to employ abstract runtime models (cf. [START_REF] Blair | Models@run.time[END_REF]) of the context and the system itself such that the self-adaptation behavior can be specified by rules operating on such abstractions. However, EUREMA is so far limited to centralized and non-distributed systems and does not address collaborations or the self-organizing SoS level.

In this paper, we will first analyze open challenges for engineering smart SoS. We will then discuss our Software with Models at Runtime for Systems of Systems (SMARTSOS) vision that employs collaborations and generic models at runtime for trustworthy self-organization and evolution of the systems at the SoS level and self-adaptation within the systems while taking the independent development, operation, management, and evolution of these systems into account. We will particularly outline the formal foundations underlying SMARTSOS based on graph transformation systems [START_REF] Rozenberg | Handbook of Graph Grammars and Computing by Graph Transformation: Foundations[END_REF][START_REF]Handbook of graph grammars and computing by graph transformation: vol. 2: applications, languages, and tools[END_REF] which cover in principle the identified challenges for the construction and assurance of smart SoS.

The rest of the paper is structured as follows: In Section 2, we discuss open challenges for smart SoS. Afterwards, our SMARTSOS vision is outlined in Section 3. Then, the concepts for constructing smart SoS with collaborations, components, and runtime models are outlined in Section 4. Afterwards, the results that enable the assurance for the smart SoS are presented in Section 5. The paper closes with a discussion of these results in Section 6 and provides in Section 7 some concluding remarks and an outlook on future work.

Challenges

SoS as a composition of systems that are operationally and managerially independent from each other [START_REF] Maier | Architecting principles for systems-of-systems[END_REF] is characterized by uncoordinated evolution steps and geographic distribution of these systems (cf. [START_REF]The Open Group Architectural Framework (TOGAF), version 9.1. Open Group Standard[END_REF]). Additionally, dynamic configuration capabilities, resilience, the ability to dynamically adapt and absorb deviations in the SoS structure, and the ability to deal with emergent behavior in context of self-organization that goes beyond developing contractual descriptions are crucial [START_REF] Valerdi | A research agenda for systems of systems architecting[END_REF] for smart SoS. These issues are challenging since each system as part of a smart SoS is independent in the sense that it is developed, operated, evolved, and governed independently from the other systems in the same SoS. Furthermore, the systems interact with each other in an open and dynamic world (cf. [START_REF] Baresi | Toward Open-World Software: Issue and Challenges[END_REF]), which causes individual systems to dynamically join or leave the smart SoS over time, the SoS architecture to deviate, and emergent behavior at the SoS level. Consequently, the SoS-level architecture and behavior are not controlled by a single, centralized authority.

As example in this paper we consider a large-scale transport system where different organizations operate fleets of autonomously driving shuttles that share a track system. This constitutes an SoS since the shuttles are operated, managed, and evolved by different authorities, they dynamically interact with each other (e.g., to build convoys), and they adapt to their own and the other shuttle's states and behavior (e.g., to decrease the speed when the shuttle's own battery level is low or when the speed of the shuttle running ahead decreases). 2Engineering such smart SoS imposes several challenges that we outline in Table 1. All of them aim for means for the construction and assurance of smart SoS and its individual systems, which must take the operational and managerial independence of the individual systems and the emergent behavior at the SoS level into account.

The first challenge considers the Construction/Assurance of Self-Adaptation (C1/A1) of the individual systems as each system within a smart SoS must adapt its behavior according to its own needs and the behavior of other systems as well as the emergent SoS-level behavior (cf. [START_REF] Vassev | The Challenge of Developing Autonomic Systems[END_REF][START_REF] Marconi | Research challenges on multi-layer and mixed-initiative monitoring and adaptation for service-based systems[END_REF]). For instance, a shuttle adapts its speed to its battery level, to the speed of the shuttle running ahead, or to an agreement established by all shuttles in a convoy. Such changes of the behavior must be systematically constructed and assured to enable trustworthy operation and in particular self-adaptation [START_REF] Cheng | Software Engineering for Self-Adaptive Systems: A Research Roadmap[END_REF][START_REF] De Lemos | Software Engineering for Self-Adaptive Systems: A second Research Roadmap[END_REF].

Due to the operational and managerial independence of the systems, the Construction/Assurance of SoS-Level Interactions for Self-Organization (C2/A2) challenge captures that the interactions among these systems must be selforganizing (cf. [START_REF]Self-organising Software[END_REF]) to achieve the SoS-level goals. For example, shuttles from different organization must interact to avoid collisions or they may even cooperate to build convoys in order to save energy. Such interplays of autonomous shuttles must be systematically constructed and assured to provide confidence for satisfying SoS-level goals (e.g., reliable and safe rail traffic).

Furthermore, since the operational context changes or the systems dynamically join or leave the SoS such that the SoS-level architecture dynamically changes, the challenge of the Construction/Assurance of SoS-Level Structural Dynamics (C3/A3) must be supported. For instance, autonomous shuttles may join or leave a convoy and the other shuttles already part of the convoy must account for it. Such dynamics must be constructed and assured to guarantee certain SoS-level behavior resulting from the interactions.

Additionally to the structural dynamics, the Construction/Assurance of SoS-Level Runtime Knowledge Exchange (C4/A4) is required since no system in the SoS typically has all the knowledge needed to achieve the SoS-level goals at runtime. This calls for exchanging knowledge between interacting systems. This knowledge refers to the current state, context, and requirements of individual systems. For instance, shuttles establishing a convoy may exchange their driving modes to agree on a common mode for the whole convoy. Such a knowledge exchange must be constructed and assured when engineering interactions to gain confidence that the SoS-level goals can be achieved.

In parallel to the self-adaptive and self-organizing behavior of systems in the SoS, the systems evolve in an uncoordinated way as they are managed independently from each other by different organizations. Evolution is caused by the permanent need to change the software in response to changing requirements of the stakeholders, no longer valid assumptions, or changing regulations the software has to adhere to (cf. software evolution [START_REF] Mens | Software Evolution[END_REF]). With evolution, we refer to introducing new or removing existing types of systems or interactions (and therefore, also behavior) from the SoS. For example, new shuttle versions that support new cooperation mechanisms are integrated into the SoS and they must not interfere with the already existing versions. To handle such radical changes in a trustworthy manner and to support the long-term existence of the SoS, the Construction/Assurance of Evolution of Smart SoS (C5/A5) is a main challenge.

In general, engineering smart SoS is challenging due to the ultra-large scale and complexity of such systems and due to the different authorities managing such systems. Therefore, the Scalable Construction/Assurance of Smart SoS (C6/A6) and the Construction/Assurance of Smart SoS with Restricted Knowledge (C7/A7) are also important aspects for the engineering. The first aspect is motivated by the fact that it is not feasible to construct the whole SoS upfront before its deployment, or to analyze all possible SoS configurations or architectures that grow exponentially with the number of participating systems. For instance, any number of shuttles of arbitrary types may run on the track system or may cooperate in a convoy. Thus, the construction and assurances for SoS must scale with the size of the SoS. The second aspect refers to the construction and assurances for smart SoS, which must work despite the restricted knowledge that participants of the SoS have. An organization responsible for an individual system in the SoS or the system itself might have no global view of the SoS and no concrete information about the other participants and possible interactions among participants. Nevertheless, assurances for each system and the SoS must be provided to enable trustworthy operations. For example, when constructing and assuring new shuttle versions supporting a certain interaction, details about other organizations' shuttle versions that are potential cooperators for the interaction might not be available. However, the construction and assurance must cope with the limited knowledge available.

These open challenges, each with a construction and assurance dimension as summarized in Table 1, reveal the difficulty of engineering and ruling smart SoS due to the complexity, dynamics, emergence, and decentralized management and governance.

SMARTSOS

In our vision SMARTSOS, we suggest combining the benefits of mUML and EUREMA to tackle the challenges for smart SoS. However, we do not suggest simply integrating the ideas of both approaches. Instead we developed a radically different and more abstract perspective on the SoS-level interactions to overcome the limitations of the state-of-the-art and former approaches and to master the complexity of smart SoS. This novel perspective is based on the combination of runtime models and collaborations.

Runtime Models

To realize the challenge of the Construction/Assurance of SoS-Level Runtime Knowledge Exchange (C4/A4), SMARTSOS employs models at runtime [START_REF] Blair | Models@run.time[END_REF] that suggest following model-driven engineering principles to engineer abstract runtime representations of running systems or their contexts and requirements. Such models are said to be causally connected to the running system, which means that changes in the system are reflected in the model and vice versa. Thus, "change agents (e.g., software maintainers, software-based agents) use [abstract] runtime models to modify executing software in a controlled manner" [40, p. 39] rather than directly adapting the running software at the code level.

With EUREMA we have extended this perspective by providing runtime models at different levels of abstraction [START_REF] Vogel | Adaptation and Abstract Runtime Models[END_REF] and by specifying the adaptation itself, that is, software-based agents, using runtime models [START_REF] Vogel | Model-Driven Engineering of Self-Adaptive Software with EUREMA[END_REF]. The latter aspect leverages the flexibility of runtime models for managing the change agents at runtime in addition to the running systems. In SMARTSOS, we go another step further and suggest using generic in contrast to highly specific and optimized runtime models, which eases interoperability and evolution of systems in an SoS, as it excludes individual optimization and specific solution for the runtime models.

For an individual system in a smart SoS, such generic runtime models may capture the system's state, context, requirements, and adaptation logic. These models may be used locally for self-adaptation and assurances that each system fulfills its requirements. As discussed in the following, they may also be used for collaborations among systems leading to the self-organization of the SoS, which requires the exchange of runtime knowledge.

The basic idea to integrate runtime models and collaborations for the construction of smart SoS is depicted in Fig. 1. At first, each running system living in the cyber world may have a view on its physical context and its own state in the cyber and physical world by means of runtime models of the context and the self. In general, we consider runtime descriptions reflecting the running system and its context as Reflection Models. Particularly, System Models (Self in Fig. 1) reflect about architectural and behavioral key aspects of the system and they are causally connected to the system. Context Models (Context in Fig. 1) describe the environmental situation of a system (cf. [START_REF] Vogel | The Role of Models and Megamodels at Runtime[END_REF][START_REF] Wätzoldt | Classifying Distributed Self-* Systems Based on Runtime Models and Their Coupling[END_REF]). In our example, models of the Context and Self are depicted in the individual Shuttle systems in Fig. 1. This supports designing the self-adaptation of the shuttles as MAPE-K feedback loops (Monitor/Analyze/Plan/Execute-Knowledge) [START_REF] Kephart | The Vision of Autonomic Computing[END_REF] while the knowledge part is implemented by the runtime models. Such feedback loops are realized by analyze and plan activities that operate on the basis of the runtime models while linking the runtime models to the system and context is realized by the monitor and execute activities. The Self and Context runtime models can refer to the local state of a shuttle (e.g., the Mode and Battery status) as well as the available information about the context (e.g., whether there is another shuttle driving on the tracks ahead of the shuttle). This context does not only consist of the physical context such as the shuttle's position, the topology of the track system, and the positions of other shuttles nearby, but additionally the context in the cyber world. This cyber-world context covers, for instance, the established collaboration instances and context shared with other roles of these collaboration instances.

As depicted in Fig. 1, these runtime models of the context and self constitute an overall local runtime model, that is, the Reflection Model, for each :Shuttle system. As described in Fig. 2 in more detail, each system does not only operate on information about its own local context and itself, but can also get access to the information stored in runtime models of other systems concerning their context or themselves. 3 In our example, the left most Shuttle system has also access to information in form of runtime models in quite different ways. The directly visible elements are the information available local to the shuttle by means of runtime models (white with solid frame). Additional information like the position of the shuttle in front of it, which is encoded by the on edge between that shuttle and its current track, is accessible for shuttles that knows the Coord collaboration type (gray with dashed frame). Finally, information about the mode of the shuttle system in front of it is accessible for a shuttle, if it is connected to this via a Coord collaboration instance (gray with solid frame).

Likewise to EUREMA, the behavior of the systems in reaction to particular situations can now be directly described based on such overall local runtime models. This is illustrated at the top of the left-hand side of Fig. 2 showing the feedback loop (i.e., the monitor, analyze, plan, and execute activities) of a shuttle realizing the self-adaptation and therefore, addressing the Construction of Self-Adaptation (C1) challenge. In the following, we will elaborate the use of such generic runtime models in the context of collaborations. In general, such models as employed by SMARTSOS provide an idealization of the systems and contexts, which is discussed in Section 4.3.

Collaborations

To approach the challenges of the Construction/Assurance of SoS-Level Interactions for Self-Organization (C2/A2) and the Construction/Assurance of SoS-Level Structural Dynamics (C3/A3) while taking aspects of the Scalable Construction/Assurance of Smart SoS (C6/A6) and the Construction/Assurance of Smart SoS with Restricted Knowledge (C7/A7) into account, SoaML and UML provide basic concepts of modeling collaborations. They support specifying abstract collaboration types and corresponding roles. The interaction of roles is defined by sequence or activity diagrams and UML interface descriptions (in form of class diagrams). Role behavior may be also covered by protocol state machines. The mUML approach goes beyond the ideas of SoaML and UML by describing the possible interaction always via real-time variant of state machines for each role and the communication medium. Due to the well-defined semantics for all employed formalism such as the real-time variant of state machines, mUML enables the basic verification of the interactions through model checking.

SMARTSOS supports a more flexible concept for collaborations compared to mUML and SoaML/UML. In SMARTSOS a richer language to specify the collaborations is provided, which also covers the exchange of complex information as well as specifying structural dynamics covering, for example, how systems can join the collaboration, leave the collaboration, or how the structure of the collaboration may change at runtime. In order to ensure interoperability and achieve trustworthy behavior at the SoS level, we furthermore need also more sophisticated analysis capabilities, for example, to investigate the impact from one system part to another through collaborations.

The basic idea of separating the required interactions into separated collaborations is depicted in Fig. 1. The autonomous systems of the SoS can connect with each other as specified by the collaboration types and can establish collaboration instances to cooperate as needed. For example, the two left most Shuttle instances in Fig. 1 are linked by a Coord collaboration instance to build a temporary convoy and the right most Shuttle instance is linked to a Station instance by an Allocate collaboration instance.

It has to be noted that different collaboration types and their involved views on the physical or cyber world may not be disjoint. In such a case, the construction and assurance for the collaboration types that share some of their elements of the physical or cyber world have to take such overlapping into account. The required concepts for abstract shared collaborations types that includes runtime models with overlapping entities are discussed in Section 4. with each other by the next relationship, as well as the positioning of the Shuttles on the tracks by the on relationship.

The class diagram of a collaboration type implicitly specifies in form of all valid object configurations for the class diagram the possible states the collaboration may be in. Later on, we define rules that refer to such object configurations to capture the system behavior. We formally define these object configurations as attributed graphs in Section 4. To capture the laws that should hold for the different collaboration types, we specify behavior rules with Story Patterns (SPs) [START_REF] Giese | Graph Transformations for MDE, Adaptation, and Models at Runtime[END_REF] that define the permitted and mandatory behavior of each role, read rules with SPs having no side effects that define the visibility of shared runtime models, and the properties the collaboration has to ensure. These properties are described by SPs without side effects in the case of simple state properties and with Timed Story Sequence Diagrams (TSSDs) [START_REF] Klein | Joint Structural and Temporal Property Specification using Timed Story Sequence Diagrams[END_REF] in the case of sequence properties. A major duty for the SoS-level assurance is to ensure that the properties are the guaranteed outcome of the roles' behavior.

Fig. 4 depicts the behavior rules, that is, the SPs defining the permitted and mandatory behavior of each role of the Coord collaboration (we refer to [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF] for the complete set of behavior rules). The SP called move in coordination on the lower right-hand side of Fig. 4, for example, describes that after the building of a platoon encoded by the existence of the Coord instance, the rear shuttle instance can move with a reduced distance behind the front shuttle instance and therefore, both shuttle instances may even be positioned on the same Track instance. The instance name self used in a rule determines the role of the collaboration, for which this rule is intended, in this example, for the shuttle role (cf. self:Shuttle element). Furthermore, the create coordination SP defines that shuttles must create a collaboration if they are on neighboring tracks and do not yet collaborate (i.e., there is no Coord instance yet).

A simple SP denotes two graphs at once. The first one is the left-handside graph L that you try to find in the current instance situation encoded in the graph G and that consists of all unmarked elements and those marked with destroy . The second one is right-hand-side graph R that consists of all unmarked elements and those marked with create . If L can be matched in G, the SP rule can be applied. A rule application on G results in the replacement of the match of L in G by R. In the case of complex SPs that have a negative application condition (NAC) that defines a graph L resulting from extending L by all the crossed-out elements. Then, besides finding the left-hand-side graph L in G there must exist no match for the NAC L in G that extends that match for L. Otherwise, the rule cannot be applied.

On the upper right-hand side of Fig. 4, the move SP specifies using such a NAC that shuttles can move forward along the track over time if there is no other shuttle on the next track. Additionally, the SP defines a temporal condition that a shuttle must stay on a track at least ten time units before it can move to the next track. This temporal condition ensures that the move SP can only be applied with respect to realistic physical movement conditions of the shuttles. If the shuttle moves, the on reference is created on the t2 Track and the clock attribute timeAtTrack of the shuttle is reseted to zero. As a consequence, the shuttle has to stay on the next track again at least for ten time units before the move SP can be applied again.

Fig. 5 shows an example of an application of a graph transformation rule. If we consider the instance situation (start graph) on the left-hand side and apply the move SP rule from Figure 4, first a match for the move SP has to be found. Thereby, we can find a match, where the shuttle instance self from Figure 4 is matched to the s1 shuttle instance on the left side in Figure 5. Because there is no other shuttle on the next track t2, the move SP can be applied for the found match with the consequence that the on link from shuttle s1 to track t1 is deleted and a new on link from shuttle s1 to track t2 is created. Thus, we obtain the instance situation (result graph) as depicted on the right-hand side on Figure 5.

The properties the collaboration type Coord should guarantee are depicted in Fig. 3. We have the forbidden situations collision and missing collaboration that must not happen. Hence, these properties are marked with ¬∃. For example, the collision SP in the middle of Fig. 3 shows the situation where two shuttles that are not collaborating with each other are on the same track, that is, these two shuttles may collide. Furthermore, the missing collaboration SP on the right-hand side of Fig. 3 reflects the faulty situation where two shuttles are on neighboring tracks but they do not collaborate with each other. Both situations have to be excluded to ensure a proper operation of the collaboration. For both instance situations in Figure 5 must hold that all specified properties are fulfilled (that the forbidden collision and missing collaboration SP cannot be matched). The read rules for the collaboration type Coord are depicted in Fig. 6 using SPs and so called path expressions that allow us to describe the fraction of the runtime models that can be accessed in a more compact form than standard SPs without such path expressions. In general, read rules on the one hand describe what the roles can access (read) but also imply on the other hand that the other roles somehow have to provide the related information. In any case, the self instance name in a read rule that must always be present determines for which role this rule specifies access to other runtime models. The optional provider instance name if present in a rule indicates whether a related role is in charge of providing that information.

The first read rule, called common, describes that it is assumed that a shuttle (marked with the self instance name) has access to the complete track topology because the path expression next[0.. * ] denotes any finite path between two Tracks with arbitrary many omitted and thus not visible nodes in between. Looking at the class diagram in Fig. 3, it reveals that the omitted nodes must always be of type Track and thus, the path expression represents all sequences of Tracks connected by next edges. As this read rule does not require any instance of the Coord collaboration, it denotes that each shuttle knows the track topology on its own (a possible implementation would be that each shuttle has a map of the track topology).

The read rule detect-obstacle for the Shuttle role (cf. self instance name) employs the path expression next[0..3] to denote a path between two Tracks with 0 to 3 not visible Tracks in between. The provider instance name for the other Shuttle role indicates that this role must provide this fragments of its runtime model. As this read rule does not require any instance of the Coord collaboration, it defines that the shuttles are able to see other shuttles nearby even though no collaboration has been established yet (a possible implementation can be based on GPS and a related protocol to broadcast position data to the shuttle's vicinity [START_REF] Giese | Multi-Agent System Design for Safety-Critical Self-Optimizing Mechatronic Systems with UML[END_REF]). The read rule share-mode for the Shuttle role (cf. self instance name) is different as it always requires an instance of the Coord collaboration. Otherwise, it does not allow a shuttle to retrieve (read) the mode of the other Shuttle role. The provider instance name for that Shuttle role indicates that this role must provide this data.

Construction

To cover in particular the challenges of the Construction of SoS-Level Interactions for Self-Organization (C2), Construction of SoS-Level Structural Dynamics (C3), Construction of SoS-Level Runtime Knowledge Exchange (C4), Construction of Evolution of Smart SoS (C5), and Scalable Construction of Smart SoS (C6), SMARTSOS supports collaborations with a dynamic number of roles, runtime models, the independent evolution of the autonomous systems and their collaborations, and the specification of individual autonomous systems without having complete knowledge about the overall SoS. These aspects require at first a solid foundation for the concepts used for the construction and assurance of smart SoS. Based on this foundation we then can formally introduce types and instances of collaborations, systems, and SoS as well as the notions of runtime models and overlapping collaborations. Finally, we cover the evolution of smart SoS, that is, the set of types and instances of the SoS evolve (e.g., new types and instances are introduced).

Foundation

The formal foundation of SMARTSOS can be based on our former results in the context of mUML and experience in formal models for self-adaptive systems [START_REF] Becker | Modeling of Correct Self-Adaptive Systems: A Graph Transformation System Based Approach[END_REF] and model transformations [START_REF] Giese | Bridging the gap between formal semantics and implementation of triple graph grammars[END_REF] based on graph transformation systems. In this context, graphs serve as a formal model to represent object configurations capturing the SoS-level architecture and runtime models (see the formal model depicted in Fig. 1) while the graph transformation rules such as SPs denote the behavior of the collaboration roles and graph conditions the required properties. To address various software aspects, we have developed extended attributed graph transformations systems covering real-time [START_REF] Becker | On Safe Service-Oriented Real-Time Coordination for Autonomous Vehicles[END_REF], probabilistic [START_REF] Krause | Probabilistic Graph Transformation Systems[END_REF], and hybrid [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF][START_REF] Becker | Cyber-Physical Systems with Dynamic Structure: Towards Modeling and Verification of Inductive Invariants[END_REF][START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] behavior. These extensions can be used in the formal foundation of SMARTSOS.

In this paper, we will only introduce the basic ideas of the underlying formal model and refer to [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] for more details. The formal model we use can be described as follows:

Typed attributed graphs G with attributes describe the states of our model elements (system of systems, systems, and collaborations). They relate to the possible object configurations that a class diagram CD defines (cf. Figure 3 for the Coord collaboration). We use G ∅ (CD) to denote all those possible typed attributed graphs that fit to a class diagram CD and do not contain any role objects. We will further refer to the empty graph as G ∅ . An example of an object configuration is depicted in Figure 2, where two shuttles are linked by a Coord collaboration. The corresponding elements can also be found in the formal model depicted on top of Fig. 1.

Sets of graph transformation rules R define the behavior. They related to the SPs we employed earlier (cf. Figure 4 for the Coord collaboration). Rules r ∈ R can match a certain fragment of a graph representing the state and in addition describe how the graph changes when the rule is applied. Given a start graph and a number of rule applications we get a path π.

Furthermore, a suitable logic for state and sequence properties is assumed and we can describe whether a sequence property φ holds for a path π (π |= φ) or for all paths generated by a start graph G and a set of rules R applied on G (G, R |= φ). Simple state conditions are specified by SPs without side effects (cf. Fig. 3), while TSSDs [START_REF] Klein | Joint Structural and Temporal Property Specification using Timed Story Sequence Diagrams[END_REF] can be employed to describe sequence properties.

Additionally, we use a refinement notion for graph transformation rule sets R R that guarantees preservation of safety properties while allowing us to extend the rules unless guaranteed behavior will be blocked.

We further exploit the fact that the different elements in our formal model are by construction separated either by their types or so-called pseudo types 4For two rules separated by their types or pseudo types holds that the behavior cannot interfere in unexpected ways.

Collaborations, Systems, and System of Systems

Collaborations Similar to SoaML and mUML, collaborations are the main elements to address the interactions among individual systems in SMARTSOS. However, we need an extended formalization as presented in more detail in [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] to cover also the structural dynamics such as joining a collaboration, leaving a collaboration, or changing the structure of a collaboration. 5 At first and in addition to the simplified view depicted in Fig. 1, we have to add extra nodes in the graphs for the role instances of a collaboration: Definition 1 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A role type ro i equals a node type ro i .

In our application example, the Shuttle element of the Coord collaboration is such a role type.

In addition to the basic notion of collaborations used in SoaML/UML and the extended one provided by mUML, we have to cover more information for a collaboration type as depicted in Fig. 1, 2, 3, and 4.

Definition 2 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A collaboration type Col i = (col i , (ro 1 i , . . . , ro ni i ), CD i , R i , Φ i ) consists of a collaboration type node col i , a number of role types ro j i , an UML class diagram CD i , a function R i : {col i , ro 1 i , . . . , ro ni i } → 2 R assigning rules to role types, and a guaranteed property Φ i .

A collaboration instance of collaboration type Col i is represented by a node of type col i . In our example we have the Coord and Allocate collaboration types (see related dashed oval shapes in Fig. 1) as well as single :Coord and :Allocate collaboration instances (see related solid oval shapes in Fig. 1).

For two different role types ro k i and ro l i the set of assigned rules has to be disjoint

R i (ro k i ) ∩ R i (ro l i ) = ∅.
The creation of collaboration instances of collaboration type Col i is only possible through the collaboration type's roles ro k i and their assigned behavior R i (ro k i ). E.g., see the create shuttle SP in Fig. 4. The relation among the collaboration Col i 's role types ro 1 i , . . . , ro ni i and any additional data types that are used within the collaboration are specified by the class diagram CD i . The class diagrams of different collaborations have to be separated by different name spaces.

In our example, we have a role type Shuttle and its behavior rules are given by the set { create shuttle, move, create coordination, move in coordination } of SPs as depicted in Fig. 4. The corresponding class diagram CD i defining the roles and all the other elements in the rules is depicted on the left-hand side of Fig. 3. The guaranteed property Φ i is in our example the and-combination of two forbidden properties collision and missing collaboration depicted in the middle and right-hand side of Fig. 3. The read rules that are depicted in Fig. 6 are not explicitly covered in the formal model but the behavioral rules of the systems that realize the roles have to take them into account. This issue will be discussed in more detail in Section 4.3.

Within a collaboration many styles of interactions, particularly, synchronous or asynchronous ones can be used. For asynchronous message passing, the following scheme can be employed: an instance of the Shuttle role creates a new message (i.e., a node in the graph) and links it to another instance of the Shuttle role that should be the receiver of the message. The latter shuttle instance can afterwards process the message that has been linked to this instance. For synchronous interactions, an instance of a role may directly modify links and data of another instance. For example, an instance of the Shuttle role may if permitted directly change the mode of another instance of the Shuttle role (cf. Fig. 1).

Systems Similar to UML and SoaML, we employ components to represent systems that interact through collaborations by realizing the related roles. Our specification of a system further comprises safety properties that have to be fulfilled by the system's implementation. Definition 3 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A system type Sys i = (sys i , (ro 1 i , . . . , ro mi i ), CD i , R i , I i , Ψ i ) consists of a system type node sys i , a number of role types ro j i , a class diagram CD i , a function R i : {sys i , ro 1 i , . . . , ro mi i } → 2 R assigning rules to role types, a set of initial rules I i ⊆ R i (sys i ), and a safety property Ψ i .

A system as an instance of system type Sys i is represented by a node of type sys i , which also fulfills the pseudo-typing requirements and thus separates elements from each other that belong to different systems. In our example we have the Shuttle and Station system types (see related dashed boxes in Fig. 1) as well as several :Shuttle and one :Station system of the corresponding types (see related solid boxes in Fig. 1).

All rules of Sys i preserve a pseudo-typing linking of all nodes to sys i . The function R i is defined as for collaboration types (see Definition 2). The only way a system/instance of type Sys i can be created is through the execution of any of the creation rules in I i . The system type's class diagram CD i contains all class diagrams of the collaboration types that are used by the system type. 6 Additionally, the system itself represented by a class sys i (node type) and all data types required by the system are contained in CD i . We further write R i (ro k i ) ⊆ R i (sys i ) to refer to the set of all rules that belong to the system Sys i 's implementation of role ro k i .

System of Systems

To cover SoS, we employ system of system types and instances. System of systems combine collaboration and system types to a conceptual unit (depicted by the outer dashed box in Fig. 1).

Definition 4 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A system of system type SoS = ((Col 1 , . . . , Col n ), (Sys 1 , . . . , Sys m )) consists of a number of collaborations types Col i and a number of system types Sys j .

Definition 5 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A system of system instance is a pair sys = (SoS, G sys ) with system of system type SoS = ((Col 1 , . . . , Col n ), (Sys 1 , . . . , Sys m )) and an initial configuration G sys that is type conform to SoS.

As this paper does not include the details of a system type and system of system type for our example, we refer to [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF][START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] to obtain these details and an example that cover abstract system specifications and a system of system type.

Runtime Models

As depicted in Fig. 1, in our formal model an idealized view of the context is directly visible and accessible by the shuttle systems. This idealization reflects that the systems handle the related information about the physical and cyber world by means of runtime models and their exchange. The idea of the read rules depicted in Fig. 6 generalizes the concept of [START_REF] Giese | Systematic verification of multi-agent systems based on rigorous executable specifications[END_REF] to capture the capabilities of sensors and actuators for the physical world. Consequently, the formal model describes what can be read directly by local sensors or indirectly by the exchange of runtime models reflecting the context or the other systems' internal states.

The read rules are not formalized but the behavior rules of the systems have to adhere to them, that is, the rules must not access information that should not be visible to them through local runtime models or the exchange/sharing of runtime models. In the example of Fig. 1, this visible information of the local and shared runtime models relates to the local context as well as the mode and battery status of the shuttle itself, the topology as given by the common read rule, the position of the shuttles nearby as given by the detect-obstacle read rule, and the mode of the other shuttles that are connected by a Coord collaboration instance as given by the share-mode read rule (cf. Fig. 6).

It has to be noted that the outlined formal model is an idealization. It assumes that the systems operate on consistent and not delayed observations and ignore the risk of partial failures. However, it many cases the outlined idealization is quite reasonable. At first, any solution that would not work for the idealization will also likely not work under more realistic assumptions. Secondly, a more detailed design would in particular acknowledge that the effects due to partial failures and delayed and inconsistent observations are limited to the extent which can be tolerated for the considered problem addressed by the collaboration type (e.g., see the protocol developed in [START_REF] Giese | Multi-Agent System Design for Safety-Critical Self-Optimizing Mechatronic Systems with UML[END_REF] that covers the loss of connection while preserving a basis for a safe behavior).

Another issue that has to be taken into account is that even though different collaborations can be employed to talk about different required interactions, as soon as they refer to the same phenomena of the physical or cyber world, the observations in the different collaborations must be consistent. Therefore, we require that in these cases an initial collaboration has to cover the interrelated phenomena of the domain that should be considered in a consistent manner and share these phenomena with the other collaborations.

If other and more specific collaboration types take a subset of the phenomena of the physical or cyber world covered by such an initial collaboration type into account, they have to extend the initial collaboration type. Then, these more specific collaboration types cannot be specified completely separated from each other and the shared one. Definition 6. An overlapping collaboration type Col i = (col i , (ro 1 i , . . . , ro ni i ), CD i , R i , Φ i ) extending a shared collaboration type Col j = (col j , (ro 1 j , . . . , ro nj j ), CD j , R j , Φ j ) consists of a collaboration type node col i , a number of roles ro j i with n i ≥ n j and for all 1 ≤ l ≤ n j ro l i = ro l j , an UML class diagram CD i extending CD j , a function R i : {col i , ro 1 i , . . . , ro ni i } → 2 R extending R j assigning rules to roles, and a guaranteed property Φ i .

In our example depicted in Fig. 1, the Allocate collaboration type refines the Coord collaboration type and therefore is aware that the shuttles may move.

Evolution

One aspect of our motivation for this work is that individual systems in a smart SoS are subject to independent changes (evolution), which has to be handled by construction and assurance. In the following, we will explicitly consider the modeling of evolution, which is not addressed by SoaML or mUML.

Definition 7 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). An extended evolution sequence is a sequence of system of systems (SoS 1 , G 1 S ), . . . , (SoS n , G n S ) such that (1) SoS i+1 only extends SoS i by additional collaboration and system types, (2) G i+1 S is also type conform to SoS i , and (2) G i+1 S can be reached from G i S in the system of system (SoS i , G i S ). An evolution sequence is a sequence of system of system types SoS 1 , . . . , SoS n such that at least one related extended evolution sequence (SoS 1 , G 1 S ), . . . , (SoS n , G n S ) exists.

As presented in [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF], type conformance for the introduced evolution concepts can be defined that ensure a proper typing of collaborations, systems, and system of systems.

Assurance

Existing instance-based formal approaches do not scale and are often not applicable to the specific settings of SoS such as openness, dynamic structures, and independent evolution. Thus, the challenges of establishing Assurance of SoS-Level Interactions for Self-Organization (A2), Assurance of SoS-Level Structural Dynamics (A3), and Assurance of Evolution of Smart SoS (A5) and in particular the Scalable Assurance of Smart SoS (A6) and the Assurance of Smart SoS with Restricted Knowledge (A7) for the assurance for smart SoS are not covered.

Therefore and similar to the mUML approach, we propose establishing the required guarantees for the assurance by referring only to the collaboration and system types rather than to the instance level. For the verification at the type level we show that the correctness proven for the collaboration and system types and only type conformance for the system of systems type will by construction imply that the related correctness also holds at the instance level for any possible configurations of the related system of systems. The scalability of our approach comes from the fact that the size of the type level is independent of the size of the instance level. However, we have to show as a general property of our approach that the results we yield for the type level are also valid for the instance level.

To tackle assurance for the envisioned SMARTSOS approach, we will first address the correctness at the type level looking into collaboration and system types. Then, we will look at the instances of collaboration and system types and show that the correctness established for the types can be transfered to the instances. Afterwards, we outline how the special case of collaborations with overlapping runtime models can be handled. Finally, we cover evolution where the set of types and instances of a SoS may evolve.

Collaboration and System Types

We start our considerations with defining what we mean by correct types for collaborations and systems (see dashed inner elements in Fig. 1).

Definition 8 (see [54]). A collaboration type Col

i = (col i , (ro 1 i , . . . , ro ni i ), CD i , R i , Φ i ) is correct if for all initial configurations G I ∈ G ∅ (CD i ) holds that for R i (Col i ) = R i (ro 1 i ) ∪ • • • ∪ R i (ro n i ) ∪ R i (col i ))
the overall behavior of the collaboration the reachable collaboration configurations are correct:

G I , R i (Col i ) |= Φ i .
Please note that looking only at the behavior of all roles and to consider only the initial object configurations G I without any roles is sufficient to cover all possible behavior, as we have a closed model where only the behavior of the roles is allowed to create or delete roles or any other considered elements.

For our example and the behavior rules of the Coord collaboration type as depicted in Fig. 4, it can be formally verified that the collaboration type is correct employing an automated checker (cf. [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF][START_REF] Becker | On Safe Service-Oriented Real-Time Coordination for Autonomous Vehicles[END_REF]). These checks only work for state properties and operate at the level of the types. Therefore, they do not have to consider the instance situation that would require checking infinite many and arbitrary large object configurations over arbitrary long sequences of steps. Another option that would allow us to cover sequence properties might be to use incomplete techniques such as simulation/testing or bounded or statistical model checking to establish a certain confidence for the correctness of a specific collaboration type.

A correct system type requires that the resulting behavior ensures the guarantees and that the system's implementation refines the combined role behavior.

Definition 9 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A system type Sys i = (sys i , (ro 1 i , . . . , ro mi i ), CD i , I i , Ψ i ) is correct if for all initial configurations G I ∈ G ∅ (CD i ) holds that (1) the reachable configurations are correct G I , R i (sys i ) ∪ COM P (Sys i ) ∪ I i |= Ψ i and that (2) the system behavior R i (sys i ) refines the orthogonally combined role behavior and creation behavior R i (sys i )

R i (ro 1 i ) ∪ • • • ∪ R i (ro mi i ) ∪ I i .
To add the collaboration behavior to the system behavior for each role without the role itself, we employ here COM P (Sys i ) = 1≤l≤mi COM P (Sys i , ro l i ) with COM P (Sys i , ro l i ) = R j (Col j ) which is covered by R i (sys i ) to derive a related closed behavior.

Due to lack of space, we do not discuss an example for a correct system type and refer to [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF][START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] for such an example and its formal verification. Again, another option might be to employ incomplete techniques such as simulation/testing or bounded or statistical model checking to establish a certain confidence for the correctness of a specific system type.

Collaborations and System Instances

After defining our notion of correctness for the types, we have to define the related notion of correctness at the instance level (cf. the solid elements in Fig. 1).

Definition 10 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). A concrete system of system sos = (SoS, G S ) with system of system type SoS = ((Col 1 , . . . , Col n ), (Sys 1 , . . . , Sys m )) is correct if it holds:

G S , R(sys 1 )∪• • •∪R(sys m )∪R(col 1 )∪• • •∪R(col n ) |= Φ 1 ∧• • •∧Φ n ∧Ψ 1 ∧• • •∧Ψ m .
Then, we can show in the following Theorem 1 that the type conformance of the system of system type and the correctness of collaboration types and system types ensures correctness at the instance level for the system of system.

Theorem 1 ( [54]

). A system of systems sos = (SoS, G ∅ ) with system of system type SoS = ((Col 1 , . . . , Col n ), (Sys 1 , . . . , Sys m )) is correct if (1) the system of system type SoS is type conform, (2) all collaboration types Col 1 , . . . , Col n are correct, and (3) all system types Sys 1 , . . . , Sys m are correct.

Theorem 1 provides sufficient but not necessary conditions to ensure the correctness. It permits us to straightforward establish the required correctness of the types by checking refinement and the guarantees for the properties using the rule sets as employed in condition ( 2) and (3). 7Due to lack of space, we do not present an example for a correct system of system type here and refer to [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF][START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] for such an example. In general, at the system of systems level, we only have to collect the evidence for correctness that is provided for the collaboration and system types being part of this system of systems.

Runtime Models

The sharing of runtime models by a single collaboration type as depicted in Fig. 1 for the Coord collaboration can be covered with the introduced basic concepts for collaborations. Thus, the results of Theorem 1 also apply in such cases and permit us to provide the required assurance. However, this does not hold for overlapping collaborations.

For collaboration types that refine a shared collaboration type we can exploit the following Definition 12 and Lemma 1 that outline under which circumstances the correctness of the composition of all overlapping collaboration types can be derived only on the basis of the correctness of all the overlapping collaboration types, the correctness of the refined shared collaboration type, and the compatibility of their roles. Definition 11. An overlapping collaboration type Col i = (col i , (ro 1 i , . . . , ro ni i ), CD i , R i , Φ i ) extending the shared collaboration type Col j = (col j , (ro 1 j , . . . , ro nj j ), CD j , R j , Φ j ) is correct if for all initial configurations G I ∈ G ∅ (CD i ) holds that the reachable collaboration configurations are correct

G I , R i (Col i ) |= Φ j ∧ Φ i for R i (Col i ) = R i (ro 1 i ) ∪ • • • ∪ R i (ro n i ) ∪ R i (col i ))
the overall behavior of the collaboration and that all added roles refine roles of the refined shared collaboration type: ∀l ∈

[n j + 1, n i ]∃k ∈ [1, n j ]R i (ro l i ) R i (ro k j ).
We can combine a set of overlapping collaboration types of the same shared refined collaboration type to obtain the related resulting collaboration type.

Definition 12. For a set of overlapping collaboration types Col i1 , . . . , Col im extending a shared collaboration type Col 0 = (col 0 , (ro 1 0 , . . . , ro n0 0 ), CD 0 , R 0 , Φ 0 ) the resulting collaboration type is defined as Col i = (col i , (ro

Φ i = Φ 0 ∧ (∧ 1≤k≤m Φ i k ).
In a next step we can show with the following Lemma that the resulting collaboration type is correct, if all overlapping collaboration types of the related shared collaboration types are correct.

Lemma 1. If all overlapping collaboration types Col i1 , . . . , Col im and the shared refined collaboration type Col 0 = (col 0 , (ro 1 0 , . . . , ro nj 0 ), CD 0 , R 0 , Φ 0 ) are correct, then the resulting collaboration type Col i = (col i , (ro 1 i , . . . , ro ni i ), CD i , R i , Φ i ) is also correct.

Proof. For any correct overlapping collaboration type Col i k = (col i k , (ro 1 i k , . . . , ro

ni k i k ), CD i k , R i k , Φ i k ) of the shared refined collaboration type Col 0 = (col 0 , (ro 1 0 , . . . , ro nj 0 ), CD 0 , R 0 , Φ 0 ) holds that G I , R i k (Col i k ) |= Φ 0 ∧Φ i k .
As the extension of each overlapping collaboration type are disjoint and the shared behavior is refining the roles of the shared collaboration, we can conclude that also G I , R i (Col i ) |= Φ i k will hold. As Φ i = Φ 0 ∧ (∧ 1≤k≤m Φ i k ) we only have to combine this finding for all 1 ≤ k ≤ m and get

G I , R i (Col i ) |= ∧ 1≤k≤m Φ i k and thus G I , R i (Col i ) |= Φ i such that Col i is correct.
Due to Lemma 1 we can now employ Theorem 1 to cover overlapping collaborations.

Evolution

So far the presented results for assurance do not cover the evolution of SoS. Therefore, we will extend the former results to cover typical evolution scenarios such as adding new collaboration or system types. If we look at our former results in more detail, we can notice that the assumption has been made that all types are known at verification time. This assumption is not true for a steadily evolving system where new type definitions are added over time. Furthermore, the different organizations involved in an SoS will only have a partial view and thus do not know all currently existing types in the SoS. For a given extended evolution sequence (cf. Definition 7) we can define correctness as follows:

Definition 13 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). An extended evolution sequence (SoS 1 , G 1 S ), . . . , (SoS n , G n S ) with SoS n = ((Col 1 , . . . , Col p ), (Sys 1 , . . . , Sys q )) is correct if for any combined path

π 1 • • • • • π n such that π i is a path in SoS i leading from G i S to G i+1 S
for i < n and that π n is a path in SoS n starting from G n S holds:

π 1 • • • • • π n |= Φ 1 ∧ • • • ∧ Φ p ∧ Ψ 1 ∧ • • • ∧ Ψ q . An evolution sequence SoS 1 , . . . , SoS n is correct if all possible related extended evolution sequence (SoS 1 , G 1 S ), . . . , (SoS n , G n S ) are correct.
A first observation is that SoS n contains all types defined in any SoS i . However, for a combined path π

1 • • • • • π n such that π i is a path in SoS i leading from G i S to G i+1 S
for i < n does not hold in general that an equal path π in SoS n exists that goes through all G i S , as the rules added by later added types may influence the possible outcomes if added at the start. 8 Another observation is that the properties guaranteed for newly introduced collaboration or system types have to be true as long as the types have not yet been introduced as otherwise the evolution cannot be correct. We can exploit these observations and construct related collaboration types E(Col i ) and system types E(Sys j ) encoding that the types come into existence later. Based on this we can then define E(SoS 1 , SoS n ) as that system of system type where the types of SoS n not present in SoS 1 can come into existence later. E(SoS 1 , SoS n ) therefore includes all possible combined paths of any possible extended evolution sequences for a given evolution sequence SoS 1 , . . . , SoS n .

We can then use the fact that the related dynamically evolving system of system type includes all possible extended evolution sequences to check also the correctness for all possible evolution sequences.

Theorem 2 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). An evolution sequence of systems SoS 1 , . . . , SoS n is correct if the related dynamic evolving system of system type E(SoS 1 , SoS n ) is correct.

Lemma 2 (see [START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF]). For a correct collaboration type Col holds also that its dynamic extension E(Col) is correct. For a correct system type Sys holds also that its dynamic extension E(Sys) is correct.

Due to Lemma 2, it is sufficient to simply check the collaboration and system types and this already guarantees that any extended evolution sequence will also show correct behavior.

Moreover, due to Theorem 2 and Lemma 2, an organization that wants to extend the system of system type accordingly does not require any knowledge about all the other types besides those which are refined or where an overlap exists. Furthermore, if two independent extensions are done which do not refer to each other, the concrete order of these extensions does not matter as the checks remain the same. Therefore, each organization can simply check its own extension by means of added collaboration and system types without considering when the other extensions are enacted.

Due to lack of space, we do not present an example for a correct system of system type with evolution here and refer to [START_REF] Becker | Architectural modelling and verification of open service-oriented systems of systems[END_REF][START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] for such an example.

Discussion

In SMARTSOS, we combine ideas from mUML and EUREMA to tackle the challenges for smart SoS that are discussed in Section 2. A radically different and more abstract perspective on the SoS-level interactions based on runtime models and collaborations is employed to overcome the limitations of the state-of-the-art and our former approaches and to master the complexity of smart SoS. In the following, we will discuss which challenges are addressed by the proposed ideas, particularly, by the concepts of collaborations and runtime models, the novelty of these ideas, and the additional benefits of these ideas.

Runtime Models

As discussed for the envisioned SMARTSOS approach in Section 3 and its formal model in Sections 4 and 5, SMARTSOS employs generic runtime models.

On the one hand, this supports the engineering of the self-adaptation for individual systems in the smart SoS as required by the challenge of Construction/Assurance of Self-Adaptation (C1/A1) (cf. Section 2). Similar to EUREMA, the self-adaptation for each system is implemented in SMARTSOS by a feedback loop with monitor, analyze, plan, and execute activities that operate on the generic runtime models. For instance, the self-adaptive behavior of each shuttle in the large-scale transport system is specified by such feedback loops operating on partially shared runtime models that reflect the shuttle itself and the shuttle's context (cf. top of the left-hand side of Fig. 2).

On the other hand, SMARTSOS uses the generic runtime models to exchange information between individual collaborating systems, which addresses the challenge of Construction/Assurance of SoS-Level Runtime Knowledge Exchange (C4/A4). This aspect distinguishes SMARTSOS from the state of the art in engineering SoS that employ specific and optimized runtime models without exchanging them among individual systems.

Therefore, SMARTSOS goes beyond the mUML approach and the state of the art by supporting generic runtime models of the contexts and the systems in the SoS. SMARTSOS also goes beyond EUREMA and the state of the art by supporting the runtime exchange of these models between the individual collaborating systems in an SoS. In the context of collaborations, such runtime models can also reflect agreements between the collaborating systems which is a prerequisite for jointly achieving the SoS-level goals. Thereby, such collaborations may be established in a self-organizing manner while each system still evolves and self-adapts independently from the other systems in the SoS.

While the generic nature of the runtime models used in SMARTSOS clearly leads to a higher complexity of the models compared to the state of the art, it also leverages a number of benefits: (B1) As a "success in regulation implies that a sufficiently similar model must have been built," [START_REF] Conant | Every good regulator of a system must be a model of that system[END_REF], it is consequently unavoidable that the software captures all the relevant variety of the controlled system itself, the requirements, and the context to be able to control their variability effectively. (B2) Herbert A. Simon observed for the example of an ant that "[t]he apparent complexity of its behavior over time is largely a reflection of the complexity of the environment in which it finds itself" [56, p. 52]. Thus, it can be expected that including the physical and cyber environment by runtime models will in fact help to reduce the complexity of the remaining software solution that operates on the basis of these runtime models. Finally, (B3) while specialized solutions that only capture a minimal amount of information about the environments lead to simpler software in the short run, it can be expected that the envisioned generic runtime models without such optimizations result in a direct-mapping [START_REF] Meyer | Concurrency, distribution, client-server and the Internet[END_REF] between the original (e.g., the system or context) and the model. Such a mapping is usually more stable in the long run and considerably eases interoperability. The latter aspect is a critical issue to achieve open and dynamic collaborations in smart SoS.

Collaborations

Based on the generic runtime models, SMARTSOS employs open and dynamic collaborations (cf. Section 3) to achieve self-organizing interactions between individual systems of the smart SoS. The collaboration concept of SMARTSOS is also covered in the formal model for the construction and assurance of smart SoS (cf. Sections 4 and 5). In contrast to state of the art approaches, this perspective on the SoS-level interactions addresses the challenges of Construction/Assurance of SoS-Level Interactions for Self-Organization (C2/A2) and Construction/Assurance of SoS-Level Structural Dynamics (C3/A3) (cf. Section 2). Moreover, it is key to address the challenges of Construction/Assurance of Evolution of Smart SoS (C5/A5), Scalable Construction/Assurance of Smart SoS (C6/A6), and Construction/Assurance of Smart SoS with Restricted Knowledge (C7/A7).

In this context, SMARTSOS extends EUREMA that does not consider collaborations at all since EUREMA focuses on centralized and non-distributed systems. In contrast to mUML, SMARTSOS employs open and more dynamic collaborations that are governed by laws supporting self-organization at the SoS level and that support the structural dynamics of smart SoS where, for example, systems may dynamically join or leave the SoS. The collaboration concept of SMARTSOS supports abstracting details of individual systems in the SoS by means of roles, runtime models, and behavioral contracts while distinguishing the type and instance levels (cf. Section 3). This collaboration concept leverages the independent development, operation, management, and evolution of these systems (cf. Sections 4 and 5). Thus, the evolution of smart SoS and its contained systems with respect to construction (cf. Section 4.4) and assurance (cf. Section 5.4) aspects is supported. By abstraction and explicitly distinguishing the type and instance levels of smart SoS, the construction and assurance are scalable as they mainly work at the type level -hence abstracting from the sheer scale and number of all possible instance situations of a smart SoS. In the same line of reasoning, the construction and assurance of smart SoS works despite not considering the complete instance situation and thus all details of the SoS. Therefore, SMARTSOS can handle the restricted knowledge of SoS caused by multiple authorities governing the SoS.

In general, the collaboration concept of SMARTSOS is motivated by the beneficial observations that (B4) in our society we have established legal domains, which we consider independent of each other. We can expect that the individuals behave according to the laws of each of these legal domains independent of the other domains. This approach allows us to cooperate even though the systems and legal domains evolve and adapt in principle independently from each other (cf. law-governed interaction [START_REF] Minsky | Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems[END_REF]). In the traffic domain, for example, rules for driving vehicles and related regulations and laws impose what individual drivers are allowed to do while within these bounds the individuals are free to act. In our example, the Coord collaboration in Fig. 1 establishes such a solution with respect to the driving behavior of the shuttles. As another example, individuals in the traffic domain may establish contracts with each other to allocate parking slots. In our example, a Shuttle may establish such a contract to have the privilege to stop at a specific platform of a Station by means of an Allocate collaboration instance as depicted in Fig. 1.

Conclusion and Future Work

In this paper we analyzed the open challenges for the envisioned smart SoS looking in particular into construction and assurance of such SoS. In this context, we presented our ideas how to tackle this vision with our SMARTSOS approach, specifically, by employing open and adaptive collaborations and generic models at runtime. We discussed that by supporting generic runtime models at the SoS level, the challenge of Construction/Assurance of SoS-Level Runtime Knowledge Exchange (C4/A4) can be covered by SMARTSOS. Furthermore, based on such runtime models, the SMARTSOS collaboration concept directly covers the challenges of Construction/Assurance of SoS-Level Interactions for Self-Organization (C2/A2) and Construction/Assurance of SoS-Level Structural Dynamics (C3/A3). Moreover, it provides the required foundation to tackle the challenges of Construction/Assurance of Evolution of Smart SoS (C5/A5), Scalable Construction/Assurance of Smart SoS (C6/A6), and Construction/Assurance of Smart SoS with Restricted Knowledge (C7/A7). While SMARTSOS addresses the challenges related to the SoS level, the challenge of Construction/Assurance of Self-Adaptation (C1/A1) of individual systems in the SoS is mainly addressed by our former work on mUML and EUREMA.

Our plans for future work are to further elaborate SMARTSOS by extending the model-driven EUREMA approach [START_REF] Vogel | Model-Driven Engineering of Self-Adaptive Software with EUREMA[END_REF] with open and adaptive collaborations and means for the distributed management of runtime models. Additionally, we plan to further strengthen the links between runtime and developmenttime models [START_REF] Vogel | On Unifying Development Models and Runtime Models[END_REF] and model-driven techniques in runtime scenarios [START_REF] Giese | Graph Transformations for MDE, Adaptation, and Models at Runtime[END_REF].

Fig. 1 .

 1 Fig. 1. Local and shared runtime models of a complex SoS architecture.

Fig. 2 .

 2 Fig. 2. Visibility of local and shared runtime models.

3 .Fig. 3 .

 33 Fig. 3. Class diagram of the collaboration type Coord (left); properties of the collaboration type Coord as forbidden SPs (middle and right).

Fig. 4 .

 4 Fig. 4. Behavior rules for the Shuttle role of the Coord collaboration as SPs.

Fig. 5 .

 5 Fig. 5. Application of the move SP from Figure 4 on an exemplary instance situation.

Fig. 6 .

 6 Fig. 6. Read rules for the Shuttle role of the Coord collaboration type as SPs.

  1 i , . . . , ro ni i ), CD i , R i , Φ i ) with a collaboration type node col i , a set of roles that unites the roles sets of Col 0 , Col i1 , . . . , Col im , an UML class diagram CD i = CD 0 ∪ 1≤k≤m CD i k , a function R i : {col i , ro 1 i , . . . , ro ni i } → 2 R extending R 0 and all R i k for 1 ≤ k ≤ m assigning rules to roles, and a guaranteed property

See http://www.railcab.de for an example with the outlined characteristics.

In the case of heterogeneous local runtime models, efficient incremental model synchronization techniques such as triple graph grammars[START_REF] Giese | Graph Transformations for MDE, Adaptation, and Models at Runtime[END_REF] can be employed. Such techniques realize required translation steps between runtime models that are specified in different modeling languages but that capture similar content. We already applied them to create and maintain multiple runtime models of a system in[START_REF] Vogel | Adaptation and Abstract Runtime Models[END_REF].

Their types separate two rules if they have no node and edge type in common. Their pseudo types separate them, if for all nodes of shared type holds that always a single link to a special node with not shared type at the instance level are demanded.

The terminology used in[START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] has been adjusted and extended in this paper to better fit the concepts of SoS.

A system type uses a collaboration type if it implements a role that has been defined for this collaboration type.

As outlined in[START_REF] Giese | Modeling and Verifying Dynamic Evolving Service-Oriented Architectures[END_REF] in detail, based on the refinement of the rule sets for the involved roles the result of Theorem 1 can also be extended to abstract system and collaboration types.

For example, in a refined model there may be urgent rules that have to be executed if enabled and thus may preempt other rules when added during the evolution.

Acknowledgment We thank Basil Becker for his contribution to the presented results and his comments on draft versions of this paper.

* This work was partially developed in the course of the project "Quantitative analysis of service-oriented real-time systems with structure dynamics" (Quantum) at the Hasso Plattner Institute at the University of Potsdam, published on its behalf, and funded by the Deutsche Forschungsgemeinschaft. See http://www.hpi.de/en/giese/projects/quantum.html Construction/Assurance of Self-Adaptation (C1/A1) Construction/Assurance of SoS-Level Interactions for Self-Organization (C2/A2) Construction/Assurance of SoS-Level Structural Dynamics (C3/A3) Construction/Assurance of SoS-Level Runtime Knowledge Exchange (C4/A4) Construction/Assurance of Evolution of Smart SoS (C5/A5) Scalable Construction/Assurance of Smart SoS (C6/A6) Construction/Assurance of Smart SoS with Restricted Knowledge (C7/A7)