1 Introduction

The growth and adaptation of a system is realized by behavioral adaptation and/or structural adaptation. While structural adaptation aims to adapt the system behavior by changing its architecture, behavioral adaptation focuses on modifying the functionalities of computational entities. Behavioral adaptation is usually suitable for the cases that minor changes are required to adapt the system. Structural adaptation is more scalable and suitable for large-scale and distributed adaptations. Yet changing the system structure to achieve minor changes is rather expensive. Hence, both behavioral and structural adaptations are often required to design complex adaptive systems.

A system must be able to evolve and grow continually even in unforeseen situations. Since an adaptation requirement might be unknown at design time, adaptive behavior must be built in a way that is flexible and modifiable at runtime. Furthermore, to guarantee the functionality of a complex software system, we have to provide mechanisms to ensure that the system is operating correctly. Here formal methods can play a key role.

Several frameworks and models have been inspired by natural systems to design large-scale adaptive systems [5, 22, 26, 27]. Although, they support self-organization, self-adaptability and long-lasting evolvability, they are not provided with a formal foundation. Moreover, specification and analysis of dynamic adaptation have been given lots of attention in the last decade [1, 2, 8, 14, 19, 20, 25] where most of the approaches deal with either behavioral adaptation or structural adaptation [6, 7]. However, dynamic adaptation and self-* properties are restricted to responding to short-term changes, while systems must be additionally able to evolve and grow to cover the long-term evolution of systems [9]. Therefore, we need an approach to design complex software systems which supports behavioral and structural adaptations to tackle the long-term evolution, flexibility, complexity, scalability and assurance problems.

The use of policies has been given attention as a powerful mechanism to achieve flexibility in adaptive and autonomous systems which allows one to “dynamically” specify the requirements in terms of high level goals. A policy is a rule describing under which conditions a specified subject must (can or cannot) perform an action on a specific object [15]. PobSAM (Policy-based Self-Adaptive Model) is a policy-based model with formal foundation for developing and modeling self-adaptive systems that supports behavioral adaptation. A PobSAM model consists of a set of managers and actors. Managers control the behavior of actors by enforcing policies. This model provides a high degree of flexibility at the behavioral level by allowing one to change policies dynamically. However, it only supports behavioral adaptation.

In this paper, we consider an extension of PobSAM [14, 15], called HPobSAM (Herarchical PobSAM) to support modeling large-scale adaptive systems. In HPobSAM, self-adaptive modules have been added to PobSAM as a structuring feature. A self-adaptive module consists of managers, actors and possibly other self-adaptive modules. The notion of a role is introduced to specify structure-independent adaptations. Roles are dynamically assigned to self-adaptive modules and actors. Structural adaptation occurs by changing the roles of entities which leads to creation, removal or changing the interactions of entities. The managers are responsible to perform structural adaptations using structural adaptation policies that are defined in terms of roles.

HPobSAM is used in [13] to model a case study in the area of smart airports. In [13], we refer to an unpublished technical report for a complete description of HPobSAM. Here we present the description, architecture, and formal syntax and semantics of HPobSAM. We use prioritized hierarchical hypergraph (hh-graph) transition systems to specify the operational semantics of HPobSAM. Prioritized hh-graph transition systems are essentially classical prioritized state transition systems augmented with a function mapping states into hh-graphs and transitions into partial morphisms, i.e. a state is provided with a hh-graph indicating the current system structure.

Formal methods have been proposed for the modeling and analysis of adaptive software systems, but they are not always suitable for designing large-scale software systems. We propose a flexible policy-based approach with formal foundation to design large-scale software systems. Compared to existing work, our approach has the following novel features:

  1. 1.

    We present a formal extension of PobSAM to model large-scale systems that is flexible and supports both structural and behavioral adaptations. We use structural adaptation policies as a mechanism for performing structural adaptation that can be modified at runtime, without the need to change the low-level programs.

  2. 2.

    We present an operational semantics for HPobSAM whose semantics rules allow us to transform a substructure that is specified only partially, i.e. we can add or remove a self-adaptive module whose internal structure is not known completely. This feature is an advantage in open systems where limited knowledge is available about the entities.

Fig. 1.
figure 1

The architecture of server clusters.

Full size image

2 Case Study

Here, we introduce the running example of the paper shown in Fig. 1. Consider a service-based system that dynamically adapts its behavior to provide an appropriate quality of service to clients. The system includes several clusters of application servers that require data provided by the data servers. The cache handler is used to determine the best cluster for handling a request considering the quality of service constraints, and the logger monitors the incoming requests. The request receiver analyzes the requests and transmits them to the request dispatcher of the proper cluster. The latter forwards the request to an application server in the cluster. When a request is processed, the result is sent back to the request receiver component. This component sends the result back to the requester and/or to the cache handler.

The system should be able to adapt its behavior to provide the requested service properly. The behavioral adaptation is done by dynamically balancing the load of clusters/servers and can be effective to some extent. However, if the load of system becomes high enough such that the current number of servers cannot handle the requests, structural adaptations come into play. We need to adapt the system structure by adding or replacing the clusters to improve the system throughput.

3 Overview of PobSAM

A PobSAM model is composed of three layers [14, 15]:

  • The functional behavior of the system is implemented by the actor layer and contains computational entities, i.e., the actors.

  • The view layer consists of view variables that provide an abstraction of the actors’ states for the managers. A view variable is an actual state variable, or a function applied to state variables of actors.

  • The main layer of PobSAM is the manager layer containing the autonomous managers. Managers control the behavior of actors according to predefined policies. A manager may have different configurations of which one is active at a time. Behavioral adaptation is performed by switching among those configurations. A configuration contains two classes of policies: governing policies and behavioral adaptation policies. A manager directs the actors’ behavior by sending messages to them according to the governing policies. A governing policy is of the form \(\langle o ,e ,\psi \rangle {\bullet }a\) where \(o \in \mathbb {N}\) is the policy priority, \(e \in \mathcal {E}\) is an event, \(\psi \) is the policy condition defined over views, and a is the policy action. Whenever a manager receives an event e it identifies all the governing policies that are triggered by that event. For each of the triggered policies, if the policy condition evaluates to true and there is no other triggered governing policy with priority higher than o, action a is requested to be executed by instructing the relevant actors to do so (by sending them asynchronous messages). The behavioral adaptation policies are used to perform behavioral adaptations by switching among different configurations.

Example 1

We model the request dispatcher of a cluster as a manager that is responsible to manage and control the behavior of the cluster. This manager has two configurations and to control the cluster behavior respectively, in low-loaded and high-loaded conditions. The servers are modeled as the actors responsible for handling incoming requests. The view layer provides some information about the processing power of each server, their current loads, the whole throughput of the cluster, and the average number of handled requests by each server. The following governing policy of with priority n defined for the request dispatcher of the cluster A states that when a new request x is received and the load of \(\mathsf {server1}\) is less than l, ask \(\mathsf {server1}\) to handle the request: \({ g = \langle n ,\mathsf {newreq}(x) ,\mathsf {load1}<l\rangle {\bullet } {\mathsf {(server1.handle}(x)) }}\).

4 The Architecture of HPobSAM

The components of a HPobSAM model are (i) self-adaptive modules, (ii) actors, (iii) the multi-level view layer, (iv) managers, and (v) roles. A system at the highest level is defined as a self-adaptive module. Figure 2 gives a schematic view of the HPobSAM architecture.

The concept of self-adaptive modules is inspired by SMC (Self-Managed Cells) [24] for structuring complex adaptive systems. A Self-Adaptive Module (SAM) is a policy-based building block which is able to automatically adapt its behavior in a complex dynamic environment. A self-adaptive module contains (i) possibly other lower-level self-adaptive modules, (ii) the actors, (iii) a view layer, and (iv) a manager. To cater for large-scale systems, multiple self-adaptive modules are composed and aggregated hierarchically into a single larger self-adaptive module. A self-adaptive module may provide services to other self-adaptive modules. Note that the services are provided and used by the manager of a self-adaptive module.

Fig. 2.
figure 2

A typical self-adaptive module.

Full size image

A manager is aware of its substructure and is responsible for performing structural and behavioral adaptations of its module. The managers are provided with a new type of policies, so-called structural adaptation policies to perform structural adaptation. When the system requires adaptation, different managers are informed and they plan various adaptations to adapt the system behavior to the current context. Hence, adaptation is performed in a distributed manner in the system and not a single entity is responsible for performing an adaptation.

In PobSAM, the view layer provides information about the actor layer to the managers. In HPobSAM, a view layer exists at multiple levels. Each self-adaptive module has a view layer defined based on the view layers of its self-adaptive modules in addition to the actors’ state variables of that module. The view layer acts as a tuple space to coordinate interactions of self-adaptive modules and a self-adaptive module can have controlled access to the view layer of other self-adaptive modules.

The structure of a system can change due to adding or removing an actor or a self-adaptive module, and modifying the actors and/or the self-adaptive modules interconnections. If the policies of a manager are described in terms of individual actors or self-adaptive modules, any modification of the manager’s underlying substructure (i.e. by joining or deleting actors or self-adaptive modules) influences the specification of its policies and the view layer, and subsequently, policies and view variables have to be redefined to become consistent with the new structure. To tackle this problem of structure-dependent policies, we use the notion of roles to refer to the agents with the same functionality. The roles are assigned by a manager to the actors and the self-adaptive modules that it controls, and managers’ policies as well as view variables are described in terms of roles. A structural reconfiguration is realized by changing the roles assigned to the entities, and hence, the managers’ policies become structure-independent and do not have to be modified after a structural reconfiguration.

Fig. 3.
figure 3

(a) HPobSAM architecture of running example; (b) a hierarchical hypergraph.

Full size image

Example 2

Figure 3(a) partially shows the HPobSAM architecture of our example. The whole system is a self-adaptive module that contains (i) several lower-level self-adaptive modules each corresponding to a cluster, (ii) a manager modeling the request receiver, and (iii) two actors for the cache handler and the logger. The roles , , and are assigned by the request receiver to the cluster A (as a low-power cluster), the logger, and the cache handler, respectively.

5 The Syntax of HPobSAM

In this section, we first briefly introduce hierarchical hypergraphs that are used to model the system structure; then we specify the structural modeling of HPobSAM; and,finally, we give the syntax of HPobSAM.

5.1 Hierarchical Hypergraphs Overview

A hypergraph is a generalization of a graph, where an edge can connect any number of nodes.

Definition 1

(Hypergraph). A hypergraph is a tuple \(G=(N,E,\theta )\), where N is the set of nodes, E is the set of hyperedges, \(\theta : E \rightarrow N^*\) is the tentacle function mapping each hyperedge to a unique finite non-empty multiset of nodes.Footnote 1

Given two hypergraphs \(G_1\) and \(G_2\) with \(G_i = (N_i,E_i,\theta _i)\) for \(i = 1, 2\), a hypergraph morphism \(m : G_1 \rightarrow G_2\) is a pair of mappings \(m=(m_N,m_E)\) with \(m_N: N_1 \rightarrow N_2\) and \(m_E: E_1 \rightarrow E_2\), such that for all \(e \in E_1\), the multiset defined by \(\theta _2(m_E(e))\) is the multiset defined by \(m_N(\theta _1(e))\).Footnote 2

Such a morphism is injective (surjective, bijective) if both \(m_N\) and \(m_E\) are injective (respectively surjective, bijective, partial or total). If there is a bijective morphism \({m: G_2 \rightarrow G_1}\), then \(G_1\) and \(G_2\) are isomorphic.

Hierarchical hypergraphs [10] are hypergraphs in which some hyperedges, called frames, may refer to hypergraphs that can be hierarchical again, with an arbitrary but finite depth of nesting.

Definition 2

(Hierarchical Hypergraph). Let \(\mathcal {X}\) be a set of symbols called variables. Let \(\mathcal {H} = \mathcal {H}_0(\mathcal {X})\) be a set of triples \({H=\langle G, F, cts\rangle }\) where G is a hypergraph, \(F = \emptyset \), and cts the trivial function from F to \(\mathcal {X}\).

For \(i > 0\), \(\mathcal {H}_i(\mathcal {X})\) consists of all triples \({H=\langle G, F, cts\rangle }\) where \(G=(N,E,\theta )\) is a hypergraph, \(F \subseteq E\) is the set of frame hyperedges of G, and \(cts: F \rightarrow \mathcal {H}_{i-1}(\mathcal {X})\cup \mathcal {X}\) assigns to each frame its content.

The class \({\mathcal {H({X})}=\bigcup _{i \ge 0} \mathcal {H}_i(\mathcal {X})}\) is the set of hierarchical hypergraphs (hh-graphs) derived from \(\mathcal {H}\) with variables in \(\mathcal {X}\).

Example 3

Figure 3(b) shows a hh-graph which has hyperedges \(\{e_1,e_2,e_3\}\), seven nodes depicted by circles, and two frames depicted using double-lined rectangles.

The concept of a graph morphism can be generalized to the hierarchical case  [10]. Let \(\mathcal {X}\) be a set of variables. For \(i=\{1,2\}\), let \(H_i = \langle {G_i}, F_i, cts_i\rangle \) be two hypergraphs with variables in \(\mathcal {X}\), and let \(X_i\) denote the set \({\{f \in F_i \mid cts_i(f) \in \mathcal {X}\}}\) of variable (or primitive) frames of \(H_i\).

Definition 3

(Hierarchical Morphism). A hierarchical morphism m from \(H_1\) to \(H_2\) is a pair \({m=(\bar{m}, m^f)}\) where \({f \in F_1 \backslash X_1}\) and

(i) \({\bar{m} :{G_1} \rightarrow {G_2}}\) is a graph morphism;

(ii) for all frames \(f \in F_1\), \({\bar{m}_E(f)} \in F_2\), and if \(\bar{m}_E(f) \in X_2 \) then \({f \in X_1}\);

(iii) \({m^f: cts_1(f) \rightarrow cts_2( \bar{m}_E (f))}\) is a hierarchical morphism for all \({f \in F_1 \backslash X_1}\).

A hierarchical morphism is injective (surjective, bijective, partial or total) if both \(\bar{m}\) and \(m^f\) are injective (respectively surjective, bijective, partial or total).

With graph constraints, certain graph properties can be expressed. In particular, it can be formulated that a graph G must (or must not) contain a certain subgraph \(G'\). An atomic graph constraint (\(\textsf {gcons}(C,C')\)) informally states that if a graph G contains the sub-graph C (premise), then it contains the sub-graph \(C'\) (conclusion) too [11].

Definition 4

(Atomic Graph Constraint). Let C and \(C'\) be two graphs. An atomic graph constraint is specified as a graph morphism \(k: C \rightarrow C'\).

Fig. 4.
figure 4

Part of the hierarchical hypergraph model of our example.

Full size image

A graph G satisfies atomic graph constraint \(\textsf {gcons}(C,C')\) specified by the graph morphism \(k: C \rightarrow C'\). if, for every injective graph morphism \({p : C \rightarrow G}\), there exists an injective graph morphism \(q : C' \rightarrow G\) with \({q \circ k = p}\). A graph constraint is a boolean formula over atomic graph constraints: (i) True and every atomic graph constraint are graph constraints, and (ii) if c and \(c'\) are two graph constraints, then \(c \vee c'\), \(c \wedge c'\) and \(\lnot c\) are graph constraints.

5.2 HPobSAM Syntax

Structural Modeling. The system structure is modeled as a hh-graph. We model role assignments as nodes, self-adaptive modules as frames, and managers, actors and roles as hyperedges. The hh-graph \(H=(G,\mathcal {K},cts)\) describes how several elements of a self-adaptive module \(\kappa \) are connected together logically. The set of self-adaptive modules of \(\kappa \) is \(\mathcal {K}\), and cts gives their internal structure. The hypergraph G shows the first-level internal structure of \(\kappa \) defined as follows:

$$ G =(N , E, \theta {})~,~ E = \{m\} \cup A \cup R \cup \mathcal {K}$$

where m is the manager of \(\kappa \), A indicates the set of \(\kappa \)’s actors, and R indicates the set of roles assigned by m.

Example 4

Figure 4 partially depicts the hh-graph of our example.

Views. A self-adaptive module \(\kappa \) has its own view layer V consisting of view variables defined over the state variables of its (immediate) actors (A) and the view variables of its (immediate) self-adaptive modules (\(\mathcal {K}\)), i.e., a view variable \(v \in V\) is a function over V, \(\mathcal {K}\), and the state variables of the actors in A.

Managers. A manager m is defined as a tuple \({m=\langle C,c_0,\kappa ,V, H\rangle }\), with C the (finite) set of configurations of m, \({{c_0}\in C}\) its initial configuration, \(\kappa \) the self-adaptive module of which m is the manager, V the (finite) set of view variables of \(\kappa \), and the hierarchical hypergraph \(H=(G,\mathcal {K},cts)\) describes how m is logically connected to other agents.

A configuration \(c \in C\) is defined as \(c=\langle {P_G}, {P_B},{{P_S}} \rangle \), where \({P_G}\), \({P_B}\) and \({P_S}\) indicate the governing policy set, the behavioral adaptation policies set, and the structural adaptation policy set of c, respectively. A primitive action of a governing policy is of the form \(\mathsf {r.msg}\) and is intended to send the message \(\mathsf {msg}\) to some actors/self-adaptive modules with role r. The behavioral adaptation policies are not influenced by this extension (See Sect. 3).

A structural adaptation policy \(sp \in {P_S}\) is defined as \({ sp\mathrm{\normalsize =} \langle o ,e ,\psi _H\rangle {\bullet }a_H}\) consists of priority \({o \in \mathbb {N}}\), event e, condition \(\psi _H\) and an action \(a_H\). The condition \(\psi _H\) can be defined as a combination of ordinary boolean expressions defined over the view layer and graph constraints defined over H, the internal structure of \(\kappa \). Let as be an actor or a self-adaptive module. The action \(a_H\) is a strategy to apply a dynamic reconfiguration with the primitive actions of the forms

  • \(\mathsf {r.msg}\) to send the message msg to the agents with role \(r \in R\),

  • \(\mathsf {join(r,as)}\) for assigning role r to as,

  • \(\mathsf {quit(r,as)}\) for releasing as from role r,

  • \(\mathsf {add(as)}\) for adding as to the substructure of m, and

  • \(\mathsf {remove(as)}\) for removing as from the substructure of m.

The condition \(\psi _H\) of a structural adaptation policy is defined as follows where \(\textsf {gcons}(Y,Y')\) is an atomic graph constraint:

$$\begin{aligned} \psi _H = ({\exists r \in R}). \psi _H ~|~ ({\forall r \in R}). \psi _H ~|~ \psi _H \wedge \psi _H ' ~|~\lnot \psi _H ~|~ \textsf {gcons}(Y,Y') \end{aligned}$$

Example 5

The policy \(\mathsf {PolicyA}\) states that when the request load is high, the cache handler is activated, i.e. the role \(\mathsf {cacheHandlerRole}\) is assigned to the cache handler by executing the action \(\mathsf {join(cacheHandlerRole,cachehandler)}\). Then, the logger is deactivated (\(\mathsf {quit(loggerRole,logger)}\)) and a new cluster with powerful servers (\(\mathsf {clusterD}\)) is added to the system. The operators ;  and || are resp. the sequential and parallel composition of the algebra CA\(^a\) that is used to specify policy actions (See [15]):

Self-adaptive Modules. A self-adaptive module \(\kappa \) is formally defined as \(\kappa =\langle V, H_\kappa \rangle \) where V and \(H_\kappa \) respectively represent the view layer and the hh-graph of \(\kappa \). Observe that \(H_\kappa \) is a hyperedge with the content H as defined above.

6 Structural Operational Semantics

We present prioritized hh-graph transition systems to define the operational semantics of HPobSAM models. Prioritized hh-graph transition systems are essentially prioritized state transition systems [15] augmented with a function mapping states into hierarchical hypergraphs and transitions into partial hierarchical morphisms. Thus every state is provided with a graph indicating the current system structure.

Definition 5

(Prioritized State Transition System). A prioritized state transition system is a tuple \(T =\langle S, \delta , L, s_0 \rangle \) where \(S\) is a set of states, \(s_0\in S\) is the initial state, L is a set of labels, and \(\delta \subseteq S\times L\times S\) is a set of transitions.

Labels \(l \in L\) are of the form \((\phi ,\alpha ,n)\) and a transition \({s{{\xrightarrow {( \phi ,\alpha ,n)}}}s'}\) means that it is possible to perform action \(\alpha \) under condition \(\phi \) in state \(s\) when there is no enabled transition with higher priority than n in state \(s\), and then make a transition to \(s'\).

Definition 6

(Prioritized hh-Graph Transition System). A prioritized hh-graph transition system is given by a pair \(\langle T, g\rangle \), where T is a prioritized state transition system and g is a pair \(g = \langle g_1, g_2 \rangle \) of mappings such that \(g_1(s)\) is a hh-graph for each state \(s\in S\), and \(g_2 (t) : g_1(s) \rightarrow g_1(s')\) is an injective partial hierarchical morphism for each transition \(t:{s\xrightarrow {l}s'} \in \delta \).

The conditions of a transition \(t:{s\xrightarrow {l}s'} \in \delta \) can contain graph constraints that are to be evaluated over \(g_1(s)\). The semantics of the actor layer remains unchanged by this extension. The semantics of the view layer is similarly defined as that of PobSAM [14, 15]. In this paper, we restrict ourselves to introduce the semantics of managers as the core part of HPobSAM.

Overview of a Manager’s Semantics. We use the notation \([{M} ]^c\langle b, p, a, q,H \rangle \) to describe a manager M where \(c =\langle P_G , P_B,P_S\rangle \) is its current configuration, \(b \in P_B\) is its triggered behavioral adaptation policy, \({p \subseteq P_G \cup P_S}\) is its set of triggered governing/structural adaptation policies, a is its current executing action (that can belong to a governing policy or a structural adaptation), q is its input message queue, and H is a hh-graph denoting the substructure of M. The semantics of triggering structural policies is identical to that of governing policies presented in [15]. Hence, we focus on their enforcement and use the notation \({M}\langle p, a, q,H \rangle \) for the sake of simplicity. The notation \(\surd \) is used to show an empty action. The operational semantics of managers in HPobSAM is described by the transition rules for PobSAM proposed in [15] and the transition rules given in Figs. 5 and 7 which we explain later. The conditions of transitions specifying managers’ semantics (e.g. \(\phi \) in Fig. 5) are evaluated on M’s view and its substructure.

The Semantics of a Manager’s Interactions is presented in Fig. 5 that contains graph constraints presented in Fig. 6. The rules description and the definition of symbols are described in the following. A primitive action of a PobSAM manager is sending an asynchronous message msg to an actor a that results in putting the message msg in a’s queue. In HPobSAM, there are three types of interactions that a manager may initiate: (i) sending a message to an actor with the role r, (ii) sending a message to a lower-level self-adaptive module with the role r, and (iii) sending a message to the sibling self-adaptive modules with the role r. The operational semantics of case (i) is expressed using the rule \({ \textsc {MSR1}}\) where \(G_1\) is a graph depicted in Fig. 6(a), \(\textsf {gcons}(\emptyset ,G_1)\) is a graph constraint that holds if the actor a has the role r, and \(s_a\) and \(s'_a\) indicate the local states of a before and after receiving the message msg. The rule \({ \textsc {MSR2}}\) expresses the semantics of case (ii). In this rule, a message is sent to a lower-level self-adaptive module \(\kappa '\) with the role r that contains a manager \(M_2\). The graph \(G_2\) is defined in Fig. 6(b). The manager \(M_1\) in the self-adaptive module \(\kappa \) has assigned the role r to its sibling self-adaptive module \(\kappa '\) that contains the manager \(M_2\). The manager \(M_1\) uses the rule \({ \textsc {MSR3}}\) to send a message to \(M_2\) (case (iii)) where \(\textsf {gcons}(\emptyset ,G_3)\) is a graph constraint with graph \(G_3\) as defined in Fig. 6(c) and \(H_{\kappa '} \cup H_\kappa \) is the union of \(H_{\kappa '}\) and \(H_\kappa \).

Fig. 5.
figure 5

The rules for managers’ interactions.

Full size image
Fig. 6.
figure 6

The graph constraints of interactions semantics.

Full size image

The Semantics of Structural Adaptation is presented in Fig. 7. In this figure, a function \(f' = f | \{(e_1,v_1),\ldots ,(e_2,v_n)\}\) is defined as \(f'(x)=\left\{ \begin{array}{lc} v_k&{}x=e_k\\ f(x) &{} - \end{array} \right. \). The predicate \(\mathsf {conn}(e,n,e')= n \in \theta (e) \cap \theta (e')\) informally states that the hyperedges e and \(e'\) are connected through the node n in a hypergraph G. The underlying substructure of M before and after a reconfiguration is respectively H and \(H'\) where \(H=\langle G,F,cts \rangle \), \(G=(N,E,\theta )\), and \(H'=\langle G',F',cts' \rangle \), \(G'=(N',E',\theta ')\). Note that for the sake of readability, only updated components of H are given in the rules.

Fig. 7.
figure 7

The rules for structural adaptation.

Full size image

When the action \(\mathsf {add}(as)\) is executed by the manager M, the actor or the self-adaptive module as is added to its underlying structure (Rule AAR). The hyperedge as is added to the hyperedge set (\( E'=E \cup \{as\} \)), and it becomes connected to the predefined role \(\iota \) through the node \(n_2\). If as is associated to a hh-graph with the content \(G_{as}\) (\(\mathsf {hhyper}(as,G_{as})\)), it is added to the frame set (\(F'=F \cup \{as\}\)) and cts is updated to reflect the content of as. The rule RAR is used to remove an actor or a self-adaptive module as (\( E'=E \backslash \{as\} \)). If as is a self-adaptive module, it is removed from the frame set (\(F'=F \backslash \{as\}\)) and cts is updated correspondingly.

The rule JAR is used to assign the role r to as. This rule adds the node \(n_2\) to the set of nodes connecting by the hyperedge as (\(\theta ' = \theta | \{(as,\theta (as) \cup \{n_2\})\}\)). Similarly, execution of the primitive action \(\mathsf {quit}(r,as)\) results in quitting as from the role r using the rule \({ \textsc {QAR}}\). In this rule, as is connected to r through the node \(n_2\) and this connection is removed by eliminating \(n_2\) from the nodes connected by as, i.e., (\(\theta '(as)=\theta (as) \backslash \{n_2\}\)). If an actor or a self-adaptive module quits from all of its roles, since it has the predefined role \(\iota \), will remain as an underlying actor of the manager m.

Example 6

Let Fig. 4 show the current structure of our example. Figure 8(a) illustrates the structure after the execution of \(\mathsf {add}(\mathsf {clusterD})\) in Example 5 that assigns the default role r to the self-adaptive module \(\mathsf {clusterD}\). Then, execution of the action \(\mathsf {join(powerfuleClusterRole,clusterD)}\) leads to the system structure shown in Fig. 8(b). To remove or add a cluster, the request receiver does not need to know the internal structure of the cluster which is an advantage of our model.

Fig. 8.
figure 8

The graph transformations of Example 6.

Full size image

The set of nodes connected by a set X is defined as \(\theta (X)= \underset{e \in X}{\bigcup }\theta (e)\). Let a self-adaptive module \(\kappa \) contain a manager M, the set of actors A, the set of self-adaptive modules \(\mathcal {K}\) and the set of roles R assigned by M. We define the well-formedness of \(\kappa \)’s structure as follows:

Definition 7

Well-formed structure. The hh-graph \(H=(G,\mathcal {K},cts)\) describing \(\kappa \)’s internal architecture, is well-structured if (1) H has at least a managed element, i.e. \(A \cup \mathcal {K}\ne \emptyset \), (2) the manager M is only connected to the roles, i.e. \(\theta (M) \subseteq \theta (R)\), (3) every role \(r \in R\) is connected to M (i.e. \(\exists n. \theta (M) \cap \theta (r) =\{n\}\)) in addition to the actors and the self-adaptive modules (i.e. \(\theta (r) \subseteq \theta (\mathcal {K}) \cup \theta (A)\)), (4) every actor \(a \in A\) is only connected to other actors or roles, i.e. \(\theta (a) \subseteq \theta (R) \cup \theta (A \backslash \{a\})\), (5) every self-adaptive module \(\kappa \in \mathcal {K}\) is connected to the role hyperedges, i.e. \(\theta (\kappa ) \subseteq \theta (R)\), and (6) every self-adaptive module \(\kappa \in \mathcal {K}\) is well-formed.

The following lemma states that the transformation rules used to specify the reconfiguration semantics are sound:

Lemma 1

If H is a well-formed hh-graph showing the underlying structure of M, then \(H'\) obtained after some structural adaptations by M is also a well-formed hh-graph.

Proof

We prove this by induction on the number of performed structural adaptations. We show the structure after n structural adaptations by \(H_n\).

Base Case. If there is no structural adaptation, \({H'=H=H_0}\) and the conclusion is obvious.

Inductive Step. Assume it holds for n adaptations, i.e. \(H_n\) is well-formed. We should prove that \(H_{n+1}\) is well-formed. To prove this, we should prove that all six conditions are preserved by each of the rules in Fig. 7.

None of the rules changes the manager M, the roles and the nodes connected by M, i.e. \(\theta '(M)=\theta (M)\) and \(\theta '(R)=\theta (R)\), therefore, (1), (2) and the first part of (3) are preserved by all the rules. In the first rule, two cases can happen:

  • if as isn’t aframe, this rule adds a new edge as that connects only the node \(n_2\) where \(n_2\) belongs to \(\theta (\iota )\), i.e. \(n_2 \in \theta (\iota )\). The updates performed by this rule include adding the new hyperedge as and setting \(\theta '(as)\) to \(\{n_2\}\), i.e. \(\theta '(as)=\{n_2\}\). From, \(n_2 \in \theta (\iota )\) and \(\iota \in R\), we can conclude \(\theta '(as) \subseteq \theta '(R)\) and subsequently the item (4) holds. The self-adaptive modules do not change, i.e. \(\theta '(\mathcal {K})=\theta (\mathcal {K})\), hence (5) and (6) are followed from the inductive step hypothesis and the fact that \(\theta '(\kappa )=\theta (\kappa )\) for all \(\kappa \in \mathcal {K}\).

  • if as is a frame, the proof of (5) will be similar to that of (4) in the previous case. This rule also adds as to the frames and (6) is trivially followed from the side-conditions of this rule (i.e. \(\mathsf {wellFormed(G_{as})}\)) and the inductive step hypothesis.

The proof for the rule RAR is similar to that of AAR. The rule JAR only updates the graph by adding \(n_2\) to the nodes connected by as, i.e. \(\theta '(as) = \theta (as) \cup \{n_2\}\). If as is a self-adaptive module, from \(n_2 \in \theta '(r)\) and the assumption that \(\theta (as) \subseteq \theta (R)\), it follows \(\theta '(as) \subseteq \theta '(R)\) (i.e. (5) holds). The conditions (4) and (6) are respectively followed from the facts that this rule does not change nodes connected by the actors (i.e. \(\theta '(A)=\theta (A)\)) and no frame is added or modified by this rule (i.e. \(\theta '(R)=\theta (R)\)). Similarly, we can prove QAR.

7 Discussion and Related Work

In [13], the suitability of HPobSAM for modeling large-scale self-adaptive systems has been discussed, particularly, it was discussed how the hierarchical structure of this model to support centralized and decentralized adaptations, improves scalability. In [17], the authors refer to [13] and mention that how the hierarchical structure offers a form of controlled autonomy and balances agent autonomy and system controllability, for example to prevent unsafe situations caused by a selfish acting ATV. Since we use hierarchical hypergraphs and a type of graph transformation rules which allows us to add or remove components with no need to be aware of their internal structure, this feature enables us to model open evolving systems where components enter or leave at any time, while their internal structure is unknown. Moreover, we use roles to specify structure-independent adaptation logic which allows us to adapt the system without changing the adaptation logic.

Three different features - separation of concerns, computational reflection and component-based design - guarantee th flexibility of the apporach to develop self-adaptive systems. Policies are used to adapt the system behavior and the system structure which can be changed and loaded dynamically. This feature provides a high-degree of flexibility and makes HPobSAM a suitable model to model evolving software systems. We believe this work is original in using both structural and behavioral adaptations which are directed by an identical flexible mechanism. The applicability of this model has been shown by applying it on two case studies in the areas of server clusters and an autonomous transportation system in a smart airport [13].

In [14, 15], we have compared PobSAM with existing approaches for modeling behavioral adaptation in terms of flexibility, separation of concerns and formal foundation. The main aim of the research presented here is to extend our formal approach for architectural modeling and structural adaptation of software intensive systems. Hence we focus here on related work concerned with the design of software-intensive systems and formal modeling of structural adaptation.

Another related area of research is structural adaptation which has been given strong attention. Formal techniques have been extensively used to model and analyze dynamic structural adaptation (see [7]). Structural adaptation (or dynamic reconfiguration) is usually modeled using graph-based approaches (e.g. [8, 25]) or ADL-based approaches (e.g. [18, 21]). Compared to the proposed approaches based on graph transformation, we use hierarchical hypergraphs and a type of graph transformation rule which allows us to add or remove components without need to be aware of their internal structure. Moreover, most existing work concentrates on modeling structural changes [6, 7], while we have integrated both behavior and architecture in our model. The authors in [6] model the system as graphs and use graph transformation to model the system behavior. In this work, both behavior and structure are modeled with the same formalism, however handling large and complex graphs would be difficult for large-scale systems. We take the benefit of both an ordinary state-based formalism for specifying behavioral information in addition to graphs as a natural model to express the system structure.

In [3, 4], a coordinated actor model for self-adaptive track-based traffic control systems is introduced which is inspired from PobSAM and Rebeca language [23]. In coordinated actor model, unlike HPobSAM we have a centralised coordinator. Creol is a formal object-oriented language to develop open distributed systems that supports dynamic upgrading of classes [28]. While this language supports some limited levels of dynamism that can be used for behavioural adaptations (e.g. by upgrading a method) or structural adaptations (e.g. by defining new interfaces), however, (i) it is not flexible as HPobSAM is, and (ii) its supported adaptations are limited and fine-grained, e.g. one cannot remove a whole sub-system. DR-BIP [12] is a component framework for programming reconfigurable systems that supports structural adaptations. In contrast to HPobSAM, this framework does not support behavioural adaptation and is not flexible.

8 Conclusion

We provided a formal semantics for HPobSAM which is a formal model to specify structural and behavioral adaptations in large-scale systems. In this model, self-adaptive modules are used as autonomous building blocks to structure a system. We used hierarchical hypergraphs to model the system structure. The proposed semantics rules enable us to add or remove a component of which the internal structure is not given. To support reasoning about systems designed using HPobSAM, we plan to extend a tool developed in [13] to generate Maude specifications from HPobSAM models which will allow us to use the reasoning techniques provided by Maude (e.g. model checking). Furthermore, the behavioural equivalence theory proposed for PobSAM [15, 16] can be slightly extended to support graph morphisms and reason about behavioural/structural equivalence.