Cédric Eichler

Thierry Monteil

Patricia Stolf

Luigi Alfredo Grieco

Khalil Drira

Alfredo Grieco

Enhanced Graph Rewriting Systems for Complex Software Domain

Keywords: Constrained and attributed rewriting systems, Graph rewriting systems, Non-functional requirements, Dynamic software architecture, Correctness by construction

come   L'archive ouverte pluridisciplinaire

Introduction

Dynamic software architectures enable adaptation in evolving distributed systems [START_REF] Gacek | Architectural description of dependable software systems[END_REF][START_REF] Kephart | The vision of autonomic computing[END_REF]. Their description cannot be limited to a unique static topology, but it has to encompass the entire scope of possible configurations [START_REF]Ieee recommended practice for architectural description of software-intensive systems[END_REF]. This scope is characterized by an architectural style, qualifying what is correct and what is not. Once this distinction made, system transformations themselves must be specified to depict their applicability conditions and effects. A crucial undesirable implication of these evolutions is a potential loss of correctness, the system withdrawing from the scope of consistency.

Besides correctness, the system has evolving functional and non-functional requirements, which are tightly linked to its appropriateness or efficiency. For example, configurations can be evaluated with reference to quality of service, energy consumption, and robustness to software or machine breakdowns. These objectives are potentially concurrent. In fact, deploying more software components or using more machines may ameliorate robustness but worsen energy consumption. The satisfaction of an objective depends on the properties of each software component, such as the machine it is deployed on, and the components reachable from it. In turn, those characteristics are dynamic and may be interdependent. The set of entities accessible through a component of the system, for example, recursively depends on the elements accessible through the components reachable in one hop. Said set is prone to evolve as components are deployed or terminated.

Hence, modeling a system to ease its management carries two particular aspects which are usually considered separately [38]: correctness and appropriateness with regard to functional and non-functional requirements. These concerns motivate the need for suitable description languages and formalisms avoiding ambiguities for correct architectural design, management and analysis.

Formal unambiguous methods are necessary to study the consistency of a system at a given time, i.e., its compliance to an architectural style. Several ways of doing so have been developed in the literature. The most immediate approach, checking the consistency of the system at run-time, may lead to combinatorial explosions and the necessity of roll-backs if it is discovered that the system is in an inconsistent state. To efficiently tackle correctness in the scope of dynamic reconfiguration, correctness by construction [START_REF] Saxena | The scaling challenge: can correct-byconstruction design help?[END_REF] through formal approaches have emerged [START_REF] Baleani | Correct-by-construction transformations across design environments for model-based embedded software development[END_REF][START_REF] Gössler | Program analysis and compilation, theory and practice[END_REF][START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF]. Based on formal proofs and reasoning in design-time, they guarantee the correctness of a system, requiring little or no verifications in runtime. A way to achieve such proofs is to investigate the properties of transformations with regard to consistency preservation, so as to ensure that if a transformation is applicable on a correct configuration its result is another correct configuration.

Modelling dynamic systems with graph-based methodologies has a long tradition [START_REF] Métayer | Describing software architecture styles using graph grammars[END_REF][START_REF] Loulou | Towards a unified graph-based framework for dynamic component-based architectures description in z[END_REF][START_REF] Hirsch | Consistent transformations for software architecture styles of distributed systems[END_REF][START_REF] Baresi | Stylebased modeling and refinement of service-oriented architectures[END_REF][START_REF] Rodriguez | A rule-driven approach for architectural self adaptation in collaborative activities using graph grammars[END_REF][START_REF] Eichler | Graph-based formalism for machine-to-machine self-managed communications[END_REF]. As generic models, graphs may be used to represent a broad range of systems according to diverse architectural views. Graph rewriting techniques allow to elaborate style-based frameworks for the specification of dynamic systems granting correct by construction, style-preserving, evolutions. However, they exhibit restraints critically weakening the possibility of assessing a configuration appropriateness when considering non-simplistic systems.

With reference to a concrete example, this article first highlights limitations of currently available graph based methods in describing system properties and their inter dependencies. The running example, known as DIET 12 [START_REF] Caron | Diet: A scalable toolbox to build network enabled servers on the grid[END_REF], consists in a hierarchical load balancer for dispatching jobs over a distributed infrastructure.

A formal extension of graph rewriting systems is then proposed to lift these shortcomings. The pivotal features of this enhancement are: mutators, admissible relationships specification, and constraint oriented encoding. It is demonstrated 1 Distributed Interactive Engineering Toolbox 2 Sources and further information are available at http://graal.enslyon.fr/DIET that the proposed solution brings three main beneficial advantages with respect to classic graph rewriting approaches. First, experimental results show that the proposed solution is significantly more efficient and scalable than existing one with regard to attribute modifications.

Second, characteristics of the system can be more efficiently assessed by combining evaluation on demand and/or update on modification. A property can be evaluated whenever its value has to be known. To avoid frequent evaluations, this value can also be kept in memory and updated whenever it changes. The choice between these two options rely on the relatives complexities and frequencies of updates and evaluations.

Third, the model allows to quickly grasp the appropriateness of a configuration, identify objectives that can be ameliorated, and component implying constraints violation. Therefore the management of the system and its evolutions is facilitated.

The rest of the paper is articulated as follows: existing approaches and their main features are illustrated in the next section. The running example, DIET, is presented in Sec. [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF]. Section 4 introduces the proposed formal extension of classical graphs and graph-grammars related theory. Section 5 exploits this enhanced model to characterize DIET, and demonstrates its fitness for appropriateness evaluation and system management. Experimental results regarding the efficiency and the scalability of the proposed method are presented and discussed in Sec. [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF]. Finally, Sec. 7 is dedicated to conclusion and outlooks.

2 Related Works

Language-Based Approaches

Architecture Description Languages (ADL) [START_REF] Oquendo | Pi-method: a model-driven formal method for architecture-centric software engineering[END_REF][START_REF] Allen | A formal basis for architectural connection[END_REF][START_REF] Garlan | Acme: Architectural description of component-based systems[END_REF][START_REF] Magee | Dynamic structure in software architectures[END_REF] have have been widely used to model software systems [START_REF] Lun | Relationship between testing criteria for architecture configuration testing based on wright specification[END_REF][START_REF] Rong | Modeling aspectoriented software architecture based on acme[END_REF]39]. Thanks to a rigorous syntax and semantic, they allow the definition of architectural entities and relations, as well as the description of the structural and behavioral properties and constraints of a system. However, such languages usually focus on the description of architectural instances, whereas dynamic aspects have been mildly studied [START_REF] Kacem | Evaluation and comparison of adl based approaches for the description of dynamic of software architectures[END_REF]. Darwin [START_REF] Magee | Dynamic structure in software architectures[END_REF] and ACME [START_REF] Garlan | Acme: Architectural description of component-based systems[END_REF] only allow component replication and optional components/connections, respectively. Dynamic-Wright [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF] adds evolving capabilities to the language Wright [START_REF] Allen | A formal basis for architectural connection[END_REF], limiting itself to predefined dynamics. The system should have a finite number of configurations and reconfiguration policies known in advance.

Model-Based Approaches

General-purpose modeling techniques can provide efficient means for handling dynamism, thanks to the definition of reconfiguration rules driving the evolution on an application in run-time. They furnish very intuitive and visual formal or semi-formal description of structural properties [START_REF] Bradbury | A survey of self-management in dynamic software architecture specifications[END_REF]. Designing and describing software models using UML, for example, is a common practice in the software industry. UML provides a standardized definition of system structure and terminology, while facilitating a more consistent and broader understanding of software architecture [36]. Nevertheless, the generic fitness of model-based approaches implies some limitations in describing specific issues like behavioral properties. Therefore, they often require the adoption of ad hoc description languages [37,39] to map architectural concepts into the visual notation of a model (e.g., UML) [START_REF] Loulou | Towards a unified graph-based framework for dynamic component-based architectures description in z[END_REF][START_REF] Kandé | Towards a uml profile for software architecture descriptions[END_REF]. Moreover, in spite of their wide acceptance, UML-based descriptions appear to lack formal tools for efficiently guaranteeing consistency, due to the inherent semi-formalness of UML.

Graph-Based Approaches

Among model-based approaches, graph-based methods are appropriate for conceiving correct by construction frameworks. Graphs and graphs rewriting have been successfully applied for modeling structural constraints and properties of a vast range of systems in multiple fields, including software architectures. As a generic model, graphs may be used to represent different architectural views, be it componentbased [START_REF] Eichler | Graph-based formalism for machine-to-machine self-managed communications[END_REF], service-based [START_REF] Baresi | Stylebased modeling and refinement of service-oriented architectures[END_REF], event-oriented, or even human applications [START_REF] Rodriguez | A rule-driven approach for architectural self adaptation in collaborative activities using graph grammars[END_REF]. Furthermore, this genericness allows, similarly to approaches combining languages-and model-based solutions, the use of graphs to conduct adaptation in systems described with UML.

Within graph-based approaches, a configuration is represented by a graph and graph rewriting rules can express horizontal or vertical transformations, i.e. reconfigurations or refinements. Architectural styles can be characterized by either a type graph [40,[START_REF] Baresi | Stylebased modeling and refinement of service-oriented architectures[END_REF] or a graph grammar [START_REF] Hirsch | Modeling software architectures and styles with graph grammars and constraint solving[END_REF][START_REF] Hirsch | Consistent transformations for software architecture styles of distributed systems[END_REF]. The first suffers from the same lack of expressiveness as UMLbased methods. Graph grammars offer a generative definition of the scope of correctness, where graph rewriting rules have two distinct values. They intervene in both the characterization of an architectural style as part of a rewriting system and in the specification of consistency preserving reconfiguration rules [START_REF] Hirsch | Consistent transformations for software architecture styles of distributed systems[END_REF]. This fitness for designing correct by construction transformations is a key motivation for the adoption of graph grammars as a modeling tool of dynamic software architectures.

Attributed Graphs

The very first thing to consider with graph-based models is the definition of attributes, representing the basic properties of a system element. The most complex solution, adopted by GROOVE 3 , is to consider attributes as special vertexes of the graph [START_REF] Ehrig | Fundamental theory for typed attributed graphs and graph transformation based on adhesive hlr categories[END_REF]. In particular, their domain of definition and operations are defined in the form of a many sorted algebraic signatures [START_REF] Ehrig | Fundamentals of algebraic specification[END_REF] SIG, thus viewing attributes as elements of a SIG-algebra [START_REF] Ehrig | Fundamental theory for typed attributed graphs and graph transformation based on adhesive hlr categories[END_REF]. A direct implication is a natural manipulation of attributes using predefined operators and their addition or deletion as regular vertexes of the graph. This modularity does not come without drawbacks. Graph rewriting rules rely on finding graph morphisms, a time-consuming problem. As a consequence, it first seems inefficient to increase the size of the input graphs.

In a simpler solution, each elements of the graph, i.e., vertexes and edges, is assigned a list of couples representing attributes along with their domains of definition [START_REF] Rodriguez | A rule-driven approach for architectural self adaptation in collaborative activities using graph grammars[END_REF]. To allow attribute modifications, graph transformation environments relying on this model usually allows the specification of changes within or alongside a rule. AGG4 is a well established graph transformation environment. It possesses in particular an efficient transformation engine that can be used on its own. It supports a large range of verification techniques applied to attributed and typed graph grammars. Attribute modifications can be specified within a rule. GMTE 5is an other engine that handles graph matchings and transformations. It provides specialized features such as inexact matching and connection instructions. Modification instructions, specified alongside a rule, allow attribute modifications.

In both approaches, a rule can only modify an attribute within its scope, i.e., that appears in the rule. This leads to an increased number of rule applications. In particular, this may create a domino effect when changing an attribute recursively impact a chain of interdependent ones.

Variable attributes are usually considered in graph rewriting rules alone. However, it may occur in real systems that the value of an attribute is unknown, due to a lack of information or the postponing of a decision. Consequently, attributes of the conceptual graph modeling the system state at a given time should also be variable.

A novel formalism is presented in the sequel of the paper. It mitigates these restraints and makes graph rewriting systems able to efficiently cope with functional and nonfunctional requirements in evolving contexts.

Illustrative Example and Problem Statement

Distributed Interactive Engineering Toolbox

In order to clarify the issues addressed in this article, a practical example is taken from SysFera-DS 6 , an industrial solution for federating and managing hybrid HPC environment. DIET [START_REF] Caron | Diet: A scalable toolbox to build network enabled servers on the grid[END_REF] is a hierarchical load balancer for dispatching computational jobs over a distributed infrastructure, like a grid or a cloud. This example is studied with regard to horizontal transformations applied to a component-based view. Its architecture is based on a set of agents: Master Agents (MA) manage pools of computational SErver Deamons (SED) via none, one or several strati of Layer Agents (LA). SEDs can achieve specialized computational services. Communications between agents are driven by the omniORB naming service (OMNI). MAs listen to client requests and dispatch them through the architecture to the best SED that can carry out the required service. This application has been described using class diagrams [37], but, in addition to correction-granting issues, the fact that a LA can manage another LA could not be taken into consideration.

Without lack of generality, a simplified architecture with a single MA and a single OMNI will be considered here. The main characteristics of the application are as follow :

1. While being deployed, each component records itself to the OMNI. 2. Each LA and each SED has a hierarchical superior (i.e., the parent node in the tree). 3. The MA and each LA manage from one (minSonsMA / minSonsLA) to ten (maxSonsMA / maxSonsMA) entities. Later in this paper, we will see that these conditions could be trivially extended to any number of minimum and maximum managed entities. Furthermore, from now on, a LA will be said to provide a certain service whenever at least of its child nodes does. 4. Due to hypothetical software restrictions and limited number of machines, the architecture is composed by at most one hundred agents. Once again, this arbitrary value could be expanded to any other.

Figure 1 offers a visual example of how a configuration of DIET may look like, with and without an OMNI. For obvious clarity concerns, the naming service will not be represented in future figures.

All instances of an architectural style are NOT created equal. At a given time, even though a configuration meets all the requirements of the application, another configuration may meet them in a "better way". In particular, we consider the following criteria : the energy consumption, the robustness, i.e. the fault-tolerance with regard to the breakdown of a machine or a software component, and the quality of service.

We assume that the energy consumption depends only on the number of used machines and of the software components deployed on them. The robustness, instead, is assessed based on three criteria that refers to the set of SEDs running the same service: (i) redundancy degree; (ii) location; (iii) balance within the hierarchical structure. For example, even if multiple SEDs are used for the same service (i.e., redundancy) it is important to allocate them on different machines (i.e., location) to reduce the vulnerability to hardware breakdowns. Similarly, spreading the SEDs far apart within the system tree helps improving the resiliency to LA failures (subject to the constraint that the LAs, not belonging to the same path from the MA to a SED, run on different machines).

Regarding quality of service, the load balance among the different vertice at the same depth in the tree is considered as criterion. Let LA(d) be the set of LA of depth d, and M(c) be the number of entities managed by the component c. An entity can be deployed and directly managed by a LA ∈ LA(d) if it does not make the standard deviation of la∈LA(d) M(la) become greater than a target threshold value, noted maxσ . An interesting point here is that robustness and energy consumption are concurrent, in the sense that deploying more software components or using more machines will, while ameliorating the first, badly impact the second.

To value these three objectives, it is crucial to keep track of some attributes of the software components :

1. the depth of each LA, 2. the number of entities managed by each component c of type LA and MA : M(c), 3. the set of services carried out by each SED and LA, 4. the machine on which each entity is deployed.

Notations introduced to describe DIET are summarized in Table 1.

Problem Statement

Herein we illustrate the main issues in modelling the DIET architecture using classical approaches:

Interdependency of attributes

The attributes of an entity v may depend on attributes belonging to a set S of other entities. In classical string grammars, attributes are classified as inherited or synthesized depending on whether the elements of S are parents/siblings of v in the parse tree or not, respectively. The value of synthesized attributes cannot be known in the context where they first appear. They depend on following application of production rules. In graph grammars, these rules traditionally symbolize the addition of software components. Similarly, graph attributes have to be handled in a very different way whether they only depend on attributes belonging to already existing entities or not. The first case can easily be addressed with attributes inheritance in graph grammars. For example, the depth of an LA could easily be derived from the depth of the entity managing it.

This does not apply in the second case. In fact, the set of services offered by an LA, for example, cannot be known in advance since they depends on children nodes that will be added or striped later on. There exist two potential solutions to this problem. Firstly, the attribute may be defined through its analytic expression. This last is either evaluated on demand or systematically re-evaluated after each transformation. Such an evaluation can be time consuming. It may also be unnecessary, for example when the attribute value has not changed. Furthermore, evaluation after each graph transformation is not to be taken lightly. These lasts are not only applied in a deployment step. They also characterize dynamic evolution of the system. Secondly, the attribute may be directly associated to its value and updated when necessary. This last solution is directly related to the modification of an existing attribute discussed in the next sub-subsection.

Modification of an existing attribute

As discussed in 2.2.2, classical approaches allow a graph rewriting rule to modify attributes within its scope only. When considering interdependency of attributes, a modification has to be propagated to dependant attributes. This may lead to a vast number of rule applications. For example, when deploying a SeD on a LA, its set of carried out services have to be updated accordingly. In fact, this update has to be recursively impacted on the ancestor of the updated entity until reaching the MA or a LA that already did carried out each services provided by the new SeD. In this scenario, there are as many rule applications as modified LAs. This phenomena leads to a loss of efficiency and scalability.

Configuration evaluation: handling constraints

Soft and hard constraints can be used to reflect functional and non-functional requirements of a system. Their fulfilment or dissatisfaction enable configuration evaluation.

It is crucial to make the distinction between integrating constraints within the architectural style, building a constrained style, and restraining the architectural style. Existing graph-based approaches are often restricted to the second case, where constraints are used to narrow the scope of correctness only. They are integrated to the model of the style, e.g. to the type graph in [START_REF] Baresi | Stylebased modeling and refinement of service-oriented architectures[END_REF], but not in the configurations themselves.

These constraints, closely related to the system and its components, are similar to attributes; they depend on attributes, are evolving, and components of the same type have analogous requirements. Hence, their integration in the model as any attributes is relevant. In particular, we wish, while constructing, deploying, or reconfiguring a configuration, to construct an easily evaluable set of constraints. Their violation could be detected and automatically handled by a manager without requiring complex decision and without analyzing the whole application. Firstly, approaches from the literature consider unknown and variable attribute in rules only, but discard their existence from a graph. Thus, classical constraints do not handle such attributes. Secondly, constraints are tackled by post-condition checking or evaluated after each rule application. Each constraints is then evaluated after a graph transformation even though it may not be changed. This concern is very similar to attribute interdependency.

These three points put under the spotlight the limits of classical graph-based formalism and the need for its expansion described in this paper.

Introducing Constraints and Mutators within Graph Rewriting Systems

Attributes, Constraints and Attributes Rewriting

Attributes

The proposed formalism conserves the simplicity and the computational efficiency of "listing" attributes as labels [START_REF] Rodriguez | A rule-driven approach for architectural self adaptation in collaborative activities using graph grammars[END_REF] while granting the possibility of flexibly applying algebraic operators. An attribute is represented as a couple, whose first element represents its value. The second element is its domain of definition. We assume the canonic notation where Y X is the set of function from X to Y. An interval of integer is noted [a..b].

Definition 1 (Attribute) An attribute is a couple Att = (Att A , Att D ) where -Att A is called value and is either a variable in Att D , a constant or an expression of a (S, OP)-algebra [START_REF] Ehrig | Fundamental theory for typed attributed graphs and graph transformation based on adhesive hlr categories[END_REF], where (S, OP) is an infinite algebraic signature with S a set of sorts including Att D and OP a set of function symbols such as OP = (Att D ) S + . and Att D is its domain of definition.

An attributed structure or system is a couple composed of the structure and a set of indexed attributes or sequence of attributes. By convention, the first member of an attribute will be noted within quotation marks if and only if its current value is a constant.

Constraints

Attributes are entirely aimed at providing information on an algebraic structure. Constraints can be seen as a specific kind of attributes.

Definition 2 (Constraint) A constraint Cons is an attribute (Cons C , Cons D ) with Cons D ={"true", "false", "unknown"}.

Considering that constraints share the same domain of definition, it will be implicit from now on. A constraint Cons = (Cons C , Cons D ) may be simply referred to as Cons C . In the following, the principles of Kleene's strong logic [START_REF] Kleene | On notation for ordinal number[END_REF][START_REF] Kleene | Introduction to metamathematics[END_REF] are adopted, in particular its basic logic operations (∨, ∧, ¬,⇒) and the fact that the only truth value is "true". The uniqueness of this truth value means that evaluations are pessimistic, i.e. "unknown" is supposed to be false.

Remark 1 A constraint can be seen as a classical expression of a predicate ternary logic. Considering a ternary logic rather than a binary one implies that unlike attributes, constraints can always be evaluated. Any minimal logic expression that can not be evaluated, due for example to an attribute implied in its expression being un-evaluable or variable, is "unknown".

In order to lighten the notation, an attributed object with constraints, i.e. a triple composed by the object, a set of indexed attributes, and a set of indexed constraints, is called an AC-object or structure. Whenever defining an AC-object containing AC-objects, rather than separating each sets of attributes (resp. constraints), a single family of sequence of attributes (resp. constraints) indexed by the sets of attributed (resp. constrained) elements is considered.

Definition 3 (AC-object) An object ob j alongside a set of attributes ATT and constraints CONS is called an AC-object and noted (ob j, ATT, CONS).

Attributes Rewriting

One of the issues evoked in section 3 is the fact that attributes are prone to evolve. A reconfiguration may thus impact the attributes of the system, the addition of a SED may for example modify the set of services carried out by some LAs. In the literature, classical string rewriting theory [START_REF] Parr | Ll(*): the foundation of the antlr parser generator[END_REF] tackles this issue by using mutators. A similar approach is adopted here.

Definition 4 (A mutator on an AC-object) A mutator on an AC-object is an arbitrary algorithm updating the value(s) of none, one or some of its attributes and constraints.

According to this definition, the scope of mutators remains limited to modification of values. They can not be used neither to add or suppress an attribute nor to modify the domain of definition of an attribute.

Attributed Constrained Graph Modelling a Configuration

Definition

An AC-graph, modeling a software snapshot or configuration at a given time, consists in an AC-couple of two AC-sets of vertexes and edges where an edge is a couple of vertexes (source, destination). Following the commonly used conventions for standard graphical descriptions, one considers that vertexes represent services or architectural components and edges correspond to their related interdependencies. Note that vertexes, edges and the graph itself are AC-systems. For any set S, the cardinality of S is represented as |S|.

Definition 5 (AC-graph) An AC-graph is defined by the system G = (V, E, ATT, CONS) where -V and E ⊆ V 2 correspond to the set of vertexes and edges of the graph respectively, -ATT (resp. CONS) is a family of sets ATT el (resp.

CONS el ), where el is a vertex, an edge or the graph itself. Consequently, ATT (resp. CONS) is indexed by a subset of V ∪ E ∪ {G}. ATT el is a set of attributes (resp. constraints) of arbitrary length and containing the sequence of attributes

(ATT i el = (A i el , D i el )) i∈[1..|ATT el |] (resp. (CONS i el = (C i el , D i el ) ) i∈[1..|CONS el |]
) of the element el.

-For any attributes (A i el , D i el ), A i el is a constant, a variable or an expression of a (S,OP el,i )-algebra where S =

e∈{ ẽ:AT T e ∈AT T } j∈[1..|AT T e |]
D j e and OP el,i = (D i el ) S + . For any graph (V, E, ATT, CONS), an element el ∈ V ∪ E is said to be attributed (res. constrained) if ATT el ∈ ATT. The graph is partially attributed and constrained since ATT and CONS are indexed by a subset of V ∪ E ∪ {G}. In this way, an empty set of attributes or constraint is not required if an element is wished not to be attributed or constrained. Now that AC-graphs are defined, it is possible to represent a configuration of DIET as presented in section 3.

Modelling a Constrained Configuration of DIET

This subsection is dedicated to the definition of a DIET configuration. Concerns expressed in Sec.3 are mapped into the theoretical concepts previously introduced in this Section. For sake of clarity, before formally introducing architectural styles, we show in Figure 2 what a DIET configuration would look like, once represented using an AC-graph.

Notations are reported in Table 2.

In the case of a DIET architecture :

-Nat, the set of possible natures of a software component, is equal to {"OMNI", "MA", "LA", "SED"} . -Link, the set of possible relationships between entities, equals {"ma2la", "ma2sed", "la2sed", "la2la", "registered"} Red and Loc, the redundancy and constraints, are further described in the dedicated paragraph. Description of the configuration At this time, the software is composed by eight components symbolized by eight vertexes and theirs corresponding relations modeled by some edges, both attributed to reflect their properties and natures. A notable fact is that components of the same nature have the same number of attributes, theirs attributes being the one identified in Sect. 3. This is ensured by the definition of the rewriting system that will be presented later in this paper. Some components as well as the graph itself are constrained to reflect the concerns stated in the same section.

Constraints are represented within doted frames, and related to their targeted object by a doted line, except for those linked to the graph itself.

Attributes The first attributes of each vertex states the nature of the modeled entity, in Nat. The configuration comprises a MA managing 2 entities and deployed on a machine noted m 1 , as represented by its second and third attribute, respectively.

Each LA possesses three more attributes, related to its depth, the number of entities it managed, the machine it is deployed on and its provided set of services. In the example, three LAs are deployed, represented by v 2 , v 3 and v 4 , of depth 1, 1 and 2, managing 2, 1 and 2 entities, and placed on machine m 2 , m 3 and m 4 , respectively. The first one, v3, manages directly or indirectly SEDs providing the set of services s 1 ∪ s 2 ∪ s 3 , the second one, v 4 , provides s 4 and v 5 , the third one, s 1 ∪ s 2 . Finally, four SEDs deployed on m 5 , m 6 , m 7 and m 8 carry out the services s 1 , s 2 , s 3 and s 4 . Note that machines and proposed services are represented by variable, and their actual value is not currently know.

Constraints The MA should not manage more that 10 entities, underlining a fundamental property of the architectural style. Load balancing is not represented since it is tackled by conditional deployment, as stated previously.

To cope with robustness, the graph is constrained by two clauses Loc(S,2) and Red(S,3), taking into account the needs for redundancy and multiple locations over the offered services. ∀ S ⊆ S, ∀x s ∈ N , let the redundancy constraint Red( S,x s ) be "There are at least x s SEDs carrying each service s in S". Red( S,

x s ) = ∀s ∈ S, ∃(v i ) i∈[1..x s ] ∈ V x s , ( ∀(i, j) ∈ [1..x s ] 2 , i = j ⇒ v i = v j ) ∧ (∀k ∈ [1..x s ], ATT 1 v k = "SED" ∧ s ∈ AT T 2 v k ).
∀s ∈ S, ∀x s ∈ N , let the location constraint Loc( S,x s ) be "For each service in S, there are at least x s different machines on which at least a SED carrying out the service s is deployed".

Loc( S,x s ) = ∀s ∈ S, ∃(v i ) i∈[1..x s ] ∈ V x s , ( ∀(i, j) ∈ [1..x s ] 2 , i = j ⇒ (v i = v j ∧ AT T 3 V i = AT T 3 V j )) ∧ (∀k ∈ [1..x s ], AT T 1 v k = "SED" ∧s ∈ AT T 2 V k .
This means that each service should be carried out by at least 3 SEDs located on at least two different machines.

In addition, a notion of location balance within sub-trees is introduced to re-enforce robustness. It is specified that a LA and a component managed by the same entity should not be deployed on the same machine or that they should have disjoint set of carried services. This constraint avoids, within a sub-tree, that SED providing similar services, and deployed in different location thanks to the clause Loc, are managed by entities deployed on the same machine. Hence the number of devices that have to breakdown in order for a service to be disrupted is increased.

Formal definition

The graph in the Fig. 2 is defined as follow. G = (V, E, ATT, CONS) where V ={v 1 , v 2 ,. . . , v 8 }, E ={ e 1 = (v 1 , v 2 ), e 2 = (v 1 , v 3 ), e 3 = (v 2 , v 4 ), e 4 = (v 2 , v 7 ), e 5 = (v 3 , v 8 ), e 6 = (v 4 , v 5 ), e 7 = (v 4 , v 6 )}, ATT ={ATT G , ATT v 1 , ATT v 2 ,. . . , ATT e 8 }, ATT v 1 ={("MA", Nat), ("2", N), (m 1 ,Mach)}. ATT v 2 ={("LA", Nat), ("1", N), ("2", N), (m 2 , Mach), (s 1 ∪ s 2 ∪ s 3 , Serv)}, ATT v 3 ={("LA", Nat), ("1", N), ("1", N), (m 3 , Mach), (s 4 , Serv)}, ATT v 4 ={("LA", Nat), ("2", N), ("2", N), (m 4 , Mach), (s 1 ∪ s 2 , Serv)}. ATT v 5 ={("SED",Nat), (s 1 , Serv), (m 5 , Mach)}, ATT v 6 ={("SED",Nat), (s 2 , Serv), (m 6 , Mach)}, ATT v 7 ={("SED",Nat), (s 3 , Serv), (m 7 , Mach)}, ATT v 8 ={("SED",Nat), (s 4 , Serv), (m 8 , Mach)}.

CONS ={CONS

G , CONS v 1 , CONS v 2 , CONS v 3 , CONS v 4 }, CONS G ={Loc(S,2), Red(S,3)}, CONS v 1 ={ATT 2 v 1 ≤ 10}, CONS v 2 ={ATT 4 v 2 = ATT 4 v 3 ∨ (ATT 5 v 2 ∩ ATT 5 v 3 = / 0)}, CONS v 3 ={ATT 4 v 3 = ATT 4 v 2 ∨ (ATT 5 v 3 ∩ ATT 5 v 2 = / 0)} and CONS v 4 ={ATT 4 v 4 = ATT 3 v 7 ∨ (ATT 5 v 4 ∩ ATT 2 v 7 = / 0)}.
From now on, notions allowing to characterize the corresponding architectural style are introduced, ensuring in particular that attributes are correctly updated and that components have the required constraints.

Graph Rewriting Rules and Grammars

An architectural style can be formalized using a graph grammar. The production rules of such systems require to identify sub-structures by the means of homomorphisms. An unattributed graph homomorphism h between two graphs is defined as an injective function f from the set of vertexes of the first one to the set of vertexes of the second graph so that if there is an edge between two vertexes of the first one there is an edge between their image in the second one. By notational abuse, the image of a vertex v by f is noted

h(v), the image of an edge (v, v ′ ) is noted h((v, v ′ )) instead of ( f (v), f (v ′ )), and the image of a subgraph G = ( Ṽ , Ẽ) of G is noted h( G).
To tackle attributes, we impose firstly that two vertexes or two edges associated through a homomorphism have the same number of attributes. Attributes of two associated elements are themselves correlated with regard to the order of their occurrences. Identified attributes should have the same domain of definition. Secondly, identifications of attributes should be consistent, e.g. a variable should not be identified with two different constants. Therefore, a system of equations is built and the existence of an attributed induced subgraph isomorphism is conditioned by its resolvability.

Definition 6 (AC-graph homomorphism)

A homomorphism between two AC-graphs G = (V, E, ATT, CONS) and G' = (V', E', ATT', CONS'), noted G→G', is a homomorphism h from (V, E) to (V', E') such as

1. ∀ el ∈ V ∪ E, |ATT el | = |ATT h(el) |. 2. ∀ el ∈ V ∪ E, ∀ i ∈ [1..|ATT el |], D i el = D i h(el) . 3. The system of equations S ={ A = A' : ∃ el ∈ V ∪ E, ∃ i ∈ [1..|ATT v |], A = A i el ∧ A' = A i h(el) } has at least one solution.
Remark 2 -Constraints do not impact the definition of a homomorphism. It will be shown that they intervene in the rewriting process in a different way. Similarly, attributes on vertexes and edges are the only one that are considered whereas attributes on the graph itself are not. -The existence of a homomorphism is conditioned by the resolvability of a system of equations on attributes. As stated in the introduction, in attributed graphs [START_REF] Hoffmann | Graph transformation with variables[END_REF][START_REF] Ehrig | Fundamental theory for typed attributed graphs and graph transformation based on adhesive hlr categories[END_REF], the existence of a morphism is also conditioned by equalities between attributes, potentially through morphism between attributes spaces. However, this is often the only clause relying on attributes that impact the applicability of a graph rewriting rule.

Solving the system of equations S results in identifying the value of some attributes with some constants in their domains of definitions and/or with the value of some other attributes. Integrating the affectation obtained by solving the systems refers to the update of the value of the attribute to reflect these identifications. For example, if ((x,y), (x,"2")) ∈ S 2 , meaning that x has been identified to the variable y and the constant "2", integrating the affectation obtained by solving S will lead to replacing each occurrence of x and y by "2".

There exists a vast number of approaches handling graph rewriting based on attributed graphs [START_REF] Hoffmann | Graph transformation with variables[END_REF][START_REF] Ehrig | Fundamental theory for typed attributed graphs and graph transformation based on adhesive hlr categories[END_REF]. Their applicability depends on various factors, always including the existence of a homomorphism between an element of the graph rewriting rule and the graph to rewrite. Inspired by string grammar theory [START_REF] Parr | Ll(*): the foundation of the antlr parser generator[END_REF], these factors are expanded herein to include the satisfaction of a set of constraints on attributes, namely the set of constraints of the AC-rewriting rule. This potentially empty set can be seen as a set of semantic predicates.

Applying a rewriting rule on a graph consists in suppressing a part of the graph and extending it by adding some vertexes and edges. In addition to classical modifications induced by the application of a rule, a set of actions is performed at the end of said application. For any AC-graph G = (V, E, AT T,CONST ) and any of its subgraph G = ( Ṽ , Ẽ, ÃT T , CONST ), the notation G\ G refers to G deprived of G, i.e. the graph Ḡ = ( V , Ē, ĀT T , CONST ) where :

-V = V \ Ṽ , -Ē = E ∩ V 2 , -ĀT T = {AT T el ∈ AT T : el ∈ V ∪ Ē} ∪AT T G , -ĀT T = {AT T el ∈ AT T : el ∈ V ∪ Ē} ∪AT T G .
Virtually, any attributed graph rewriting formalism could be extended to include semantic predicates, constraints and mutators. In order to fix the idea, the classical double push out formalism defined in [START_REF] Rozenberg | Handbook of Graph Grammars and Computing by Graph Transformations[END_REF] has been chosen, alongside with the attribute management presented previously.

Definition 7 (AC-rewriting rule of AC-graph) An AC rewriting rule of an AC graph is a 5-tuple (L, K, R, ATT, CONS, ACT) where

-ATT = ATT rule ∪ ATT L ∪ ATT R is
(L = (V L , E L ), ATT L , / 0) and (R = (V R , E R ), ATT R , CONS R\K ) are AC-graphs, -K = (V K , E K ) is a sub-graph of both L and R, -ACT is a set of actions.
A rule is applicable on a AC-graph G if :

1. there is a homomorphism h : (L, ATT L , CONS L ) → G, implying in particular that the system of equations S ={ A = A' :

(∃ v ∈ V L , ∃ i ∈ [1..|ATT v |], A = A i v ∧ A' = A i h(v) ) ∨ (∃ e = ( v, ṽ) ∈ E, ∃ i ∈ [1..|ATT e |], A = A i e ∧ A' = A i (h( v),h( ṽ))
)} has at least a solution, 2. the application of the rule would not lead to the apparition of any dangling edge, 3. each Cons ∈ CONS rule is evaluated to "true" by integrating the affectations obtained by solving S and by evaluating each elementary logic expression containing variable attributes to "unknown" as stated in remark 1.

Its application consists in :

1. erasing h(L\K) including CONS h(L\K) , 2. integrating the affectations obtained by solving S to the remaining graph, 3. adding an isomorph copy of R\K, including CONS R\K , integrating the affectations obtained by solving S, 4. performing each action Act ∈ ACT.

Graph rewriting rules treat vertex and edge constraints much like attributes. They are added and suppressed alongside the element they target.

Efficient access to attribute values : evaluation on demand or update on modification Note that, thanks to mutators, this formalism enforces several ways of considering and evaluating attributes or constraints. These lasts can be explicitly characterized by their analytic expression. However, this expression has to be calculated whenever its value is required or after each transformation. To avoid frequent evaluations, the attribute value can be stored and be updated whenever it has to be, using mutators. The choice between these two options rely on the relative complexities and frequencies of updates and evaluations.

Inspired from Chomsky's generative grammars [START_REF] Chomsky | Three models for the description of language[END_REF], graph grammars are defined as a classical grammar or rewriting system, and formally characterize an architectural style.

Definition 8 (Graph Grammar)A graph grammar is defined by the 4-tuple (AX, NT, T, P) where -AX is the axiom, an AC-graph with a single vertex AX -NT is a set of AC-vertexes, called non-terminal term of the grammar, -T is a set of AC-vertexes terminal term, named terminal term of the grammar, -P is the set of AC-rewriting rules, or production rules, belonging to the graph grammar.

Each vertex occurring in a graph rewriting rule in P or in a graph obtained by applying a sequence of productions ∈ P to the axiom is then isomorph to at least one arch-vertex in NT or T .

Terminal terms define archetype of vertexes with corresponding pattern of attributes and constraints. On the other hand, production rules grant constraint management and system updates. Terminal terms and productions guarantee that each component, at any time, of the system is correctly constrained and attributed according to its type. Definition 9 (Instance belonging to the graph grammar) An instance belonging to the graph grammar (AX, NT, T, P) is a graph obtained by applying a sequence of productions in P to AX.If an instance does not contain any vertex isomorph to an arch-vertex from NT it is said to be consistent.

Correct-by-Construction Reconfigurations.

Correct by construction reconfigurations based on the generative aspect of graph grammars is one of theirs key advantages. A transformation is considered correct if its application to an instance of the grammar produce another one. Productions of the grammar are correct by definition. Thanks to operations on graph rewriting rules that preserve their correctness, correct transformations can be built starting from productions rules. Applicability restriction, for example, is such an operator.

Let r be a rewriting rule whose application is equivalent to the application of a production p. It is immediate that r preserves consistency if its applicability conditions are equivalent to or stronger than those of p, e.g. if r requires a larger pattern to be found meaning that L r is a sub-graph of L p . This still holds in presence of mutators and constraints. In addition to classical requirements, the application of two rules is equivalent if they have the same mutators. If the application conditions of a rule are stronger than those of a rule p, they still are if the first is as least as constrained as the second, e.g. if CONS p ⊆ CONS r .

Summary of the Proposed Contribution

In the previous Sub-Sections, a complete description of the proposed formalism has been detailed. Here, for sake of clarity, we highlight its pivotal features and advantages in a concise form.

-Attributes are enriched to cover their interdependencies and potentially unknown values. Their definition, rather than being restricted to predefined operators and dependencies, is based on the characterization of every admissible relationships. -Constraints are defined as a special kind of attributes, so as to benefit from their evolution and dependencies mechanisms. Being elements of a ternary logic system, they cope with unknown attributes. -Graph rewriting rules are expanded with the consideration of constraints and mutators. Firstly, constraints on the rule itself constitute semantic predicates that allow decision making in presence of unknown attributes. Constraints are added and deleted alongside the element they target. Secondly, mutators, adapted from classical string theory, manage efficiently and flexibly attribute modifications.

Accordingly, it is possible to extend graph grammar approaches in order to embrace these new features, capitalize their strengths, and enable the effective management of dynamic software architectures subordinate to functional and non-functional requirements.

Exploitation and Illustration of the New Formalism : DIET Characterization, Evaluation and Management

This Section illustrates the potential of the elaborated formalism by first describing DIET, taking into account each consideration introduced in Sect. 3. Then, the fitness of this description to appropriateness evaluation and performance aware management is demonstrated using concrete examples.

DIET Characterization.

This section is dedicated to the characterization of the DIET application described in Sect. 3 using the new formalism presented in this contribution. To this end, we design axioms, terminal terms, and production rules of the Graph Grammar that unambiguously define DIET. Also, we formally demonstrate the termination of the resulting grammar.

Axiom

Considering the definition of graph rewriting rules and systems, instances of the such systems are graphs that inherit the attributes and constraints of the axiomatic graph. In the case of DIET, attributes and constraints shared by all possible software configurations are:

1. the largest number of entities that a LA may manage (the minimum being directly granted by production rules), 2. the largest number of entities that a MA may manage (idem), 3. the threshold value intervening in the balancing condition discussed in Sec. 3, 4. the maximum of total agents and 5. the current number of agents.

Common constraints, instead, refers to redundancy and location conditions each configuration has to satisfy.

Therefore, let AX DIET be (v AX , ATT AX = ((maxSonsLA, N), (maxSonsMA, N), (maxσ , R + ), (maxAgents, N), (curAgents, N)), CONS AX = (Loc(S,2),Red(S,3))), where curAgents = 0 and, arbitrarily, maxSonsMA = maxSonsLA = 10 and maxAgents = 100. Throughout this section, the graph on which production rules will be attempted to be applied to is noted G = (V, E, ATT, CONS). Attribute and constraint inheritance ensure that if G is an instance of the architectural style defined here, ATT G = ATT AX and CONS G ⊆ CONS AX .

Terminal Terms

These terms characterize types of AC-vertexes, defining a pattern of attributes and constraints shared by vertexes of the same kind.

The naming system itself is not constrained, and its attributes are limited to its nature and the machine it is deployed on. Therefore, let T Omni be (v Omni , ATT Omni = (("Omni", Nat), (m, Mach)), / 0). Similarly, let T SED = (v SeD , ATT SED = (("SED", Nat), (s, Serv), (m, Mach)), / 0).

The MA shall not manage more than 10 entities. Accordingly, let T MA be (v MA , ATT MA = (("MA", Nat), (Nsons, N),

(m, Mach)), CONS MA = ((Nsons < A 2 AX ))).
Finally, a LA and a component managed by the same entity should not be deployed on the same machine or they should have disjoint set of carried services. Let v be the entity managing v, i.e. v ∈ V such that ( v,v) ∈ E, and sib(v) = { v:( v, v) ∈E G } \{v} the set of components managed by v, excluding v, i.e. the siblings of v. T LA is (v LA , ATT LA = (("LA", Nat), (depth, N), (Nsons, N), (m, Mach), (s, Serv)),

CONS LA = (c(v LA )), where c(v) = (c(v) i ) i∈[1..|sib(v)|] , ∀ ṽ ∈ sib(v), !∃ i ∈ [1..|sib(v)|], (A 1 v = "LA" ∧ c(v) i = (A 4 v = A 4 ṽ ) ∨ (A 5 v ∩ A 5 ṽ = / 0)) ∨ (A 1 v = "SED" ∧ c(v) i = (A 4 v = A 2 ṽ ) ∨ (A 5 v ∩ A 3 ṽ = / 0))

Productions of the Grammar

Production rules of the graph grammar formalize the construction of its instances by defining when and how an entity may be deployed and the consequences of such a deployment.

The first rule (p 1 ) to define is the initialization consuming the axiomatic vertex (Del). The naming service and the MA are deployed, as well as a non-terminal vertex granting that the MA manages at least an entity (Add). This vertex will be later on instantiated into a LA or a SED. Finally, the MA registers to the naming service and the current number of agents is updated accordingly. Let p 1 = (L p 1 , K p 1 , R p 1 , / 0, / 0, µ registering (pv2), µ inc (G, 5, 3) ), where µ registering (v) is the action of registering the object represented by the vertex v to the naming service. µ inc (e, i, 1), defined in Fig. 3, represent the incrementation of the i-th attribute of v by n. Graphical parts of the rewriting rules are illustrated here using the format L←K→R. This graphical representation is illustrated in Fig. 4, where L p 1 , K p 1 , R p 1 and pv2 are defined.

Productions rules p 2 and p 3 model the addition of a nonterminal vertex, managed by the MA or a LA, respectively. This temporary vertex will later on be instantiated into a LA or a SED. To deploy a new entity, three condition should be met. This addition should respect (1) the balancing condition, (2) the maximal number of agents manageable by its superior and (3) the maximum number of total agents. The application of these productions leads to the incrementation of the numbers of total agents and of sons of the entity managing the added vertex.

µ inc (e, i, n) A i v ← A i v + n
Let p 2 = (L p 2 , K p 2 , R p 2 , / 0, A 4 G > A 5 G , (µ inc (pv2MA, 2, 1),
µ inc (G, 5, 1))) and p 3 = (L p 3 , K p 3 , R p 3 , / 0, (balancing(pv2LA), Nsons < ATT 1 G , A 4 G > A 5 G ), (µ inc (pv2LA, 3, 1), µ inc (G, 5, 1)), where L p 2 , K p 2 , R p 2 , pv2LA, L p 3 , K p 3 , R p 3 , and pv2MA are defined in Fig. 5. balancing

(v) = σ ((A 3 la ) la∈LA(A 2 v )\{v} , A 3 v +1) < A 3
G , where σ (s) is the standard deviation of the sequence s.

The instantiation of a temporary vertex managed by the MA or a LA into a SED is described by p 4 and p 5 , respectively. After deploying the SED, it has to register to the naming service and, if it is managed by a LA, update the set of its carried out services. Let p 4 = (L p 4 , K p 4 , R p 4 , / 0, / 0, µ registering (pv4)) and p 5 = (L p 5 , K p 5 , R p 5 , / 0, / 0, (µ registering (pv4), µ updateServ (pv2,pv4,2)), where L p 4 , K p 4 , R p 4 , L p 5 , K p 5 , R p 5 , pv2, and pv4 are defined in Fig. 7. µ updateServ (v, ṽ, ind), de- scribed in Fig. 6, impact a change in A ind ṽ , the set of carried out services by ṽ, on v, the component managing ṽ, by updating the set of services it proposes. This update is conducted only if v is a LA, and, if there is indeed a change, it is propagated to the entity managing v. ( v, v) Fig. 6 µ updateServ (v, ṽ, ind), A change of A ind ṽ , the set of services carried out by ṽ, impacts v, the entity it is managed by.

µ updateServ (v, ṽ, ind) if A 1 v = "LA" oldServ ← A 5 v A 5 v ← oldServ ∪ A ind ṽ if A 5 v = oldServ v ← v ∈ V G , ( v, v) ∈ V E µ updateServ
The two last productions of the grammar, p 6 and p 7 , describe the instantiation of non-terminal term into a LA managed by the MA and a LA, respectively. Since a LA has to manage at least one entity, such an instantiation can be conducted only if an entity can be later on deployed without exceeding the maximum number of agents. Let p 6 = (L p 6 , K p 6 , R p 6 , / 0, A 4 G > A 5 G , (µ registering (pv4),µ inc (G, 5, 1))) and p 7 = (L p 7 , K p 7 , R p 7 , / 0, A 4 G > A 5 G , (µ registering (pv4),µ inc (G, 5, 1))), where L p 6 , K p 6 , R p 6 , L p 7 , K p 7 , R p 7 , and pv4 are defined in Fig. 8.

The Constrained Attributed Graph Grammar Characterizing DIET

Considering the sets introduced in this section, GRS DIET , the graph rewriting system formally characterizing DIET, introduced in Sect. 3, is defined as GRS DIET =(AX DIET , NT DIET , T DIET , P DIET ), where NT DIET = (v temp , ATT temp = ("temp",{"temp"}), CONS temp Note that the limitation of entities that can be managed by the MA or a LA are not tackled in the same way. A con-straint reflecting this restriction is added on the MA, whereas the satisfaction of this limitation is granted for the LAs by a semantic predicate. Said predicate restricts the applicability of p 3 by imposing, before making a LA manage a new component, that said LA as not reach the limit of component it can manage. Since p 3 is the only production of the grammar increasing the number of entities managed by a LA, this limit can not be overpassed. A brief summary of the mapping between the concerns expressed in Sec. 3 and formal concepts is presented in Table 3.

Loc(S,2),Red(S,3) ∀s ∈ S, ∀x s ∈ N , let the location constraint Loc( S,x s ) be "For each service in S, there are at least x s different machines on which at least a SED carrying out the service s is deployed".

Loc( S,x s ) = ∀s ∈ S, ∃(v i ) i∈[1..x s ] ∈ V x s , ( ∀(i, j) ∈ [1..x s ] 2 , i = j ⇒ (v i = v j ∧ AT T 3 V i = AT T 3 V j ) ∧ (∀k ∈ [1..x s ], AT T 1 v k = "SED" ∧s ∈ AT T 2 V k .
Guaranteeing theoretical properties of the grammar: Termination. A generative grammar is said to be terminating if there can not be an infinite sequence of its production rules. Theoretically, this property ensures that the set of instances of the grammar is finite and that its exploration or the construction of an instance can be represented by a terminating algorithm. Practically, this property is consistent with the finiteness of the available resources, like machines and theirs computing powers.

Theorem 1 GRS DIET is terminating.

Proof Let S be a non-empty sequence of elements in P DIET and |S| its size. Let's prove that ∃ N ∈ N, |S| ≤ N.

For p ∈ P DIET , let Occ(p) be the number of occurrences of p in S p . Accordingly, Occ(p).

|S| = Σ p∈P DIET
(

Let's consider the following system of tokens :

-Token A : G 4 -G 5 , the number of agents that still can be deployed. -Token B : the number of temporary vertexes in the graph.

Applying p 2 , p 3 , p 6 or p 7 decrease the number of token A by 1, whereas p 1 requires 3. Hence, 3 * Occ(p 1 ) + Occ(p 2 ) + Occ(p 3 )+ Occ(p 6 ) + Occ(p 7 ) ≤ maxAgents.

(

The application of p 4 or p 5 consumes 1 token B, whose number is increased when applying p 1 , p 2 or p 3 . Hence,

p 3 σ ((A 3 la ) la∈LA(A 2 v )\{v} , A 3 v +1) < A 3 G
Incrementing the number of entities managed by v = balancing(v) respect the balancing condition

sib(v) { v:( v, v) ∈E G } \{v} Siblings of v where v ∈ V such that ( v,v) ∈ E CONS LA = c(v) (c(v) i ) i∈[1..|sib(v)|] , ∀ ṽ ∈ sib(v), !∃ i ∈ [1..|sib(v)|],
A LA and each of its siblings

(A 1 v = "LA" ∧ c(v) i = (A 4 v = A 4 ṽ ) ∨ (A 5 v ∩ A 5 ṽ = / 0)) ∨
should not be deployed on the same machine or

(A 1 v = "SED" ∧ c(v) i = (A 4 v = A 2 ṽ ) ∨ (A 5 v ∩ A 3 ṽ = / 0)) they should have disjoint set of carried services CONS 1 AX Red( S,x s ) = ∀s ∈ S, ∃(v i ) i∈[1..xs] ∈ V xs , ( ∀(i, j) ∈ [1..x s ] 2 , Each service is carried out by at least 3 SEDs Red(S, 3) i = j ⇒ v i = v j ) ∧ (∀k ∈ [1..x s ], ATT 1 v k = "SED" ∧ s ∈ AT T 2 v k ) CONS 2 AX Loc( S,x s ) = ∀s ∈ S, ∃(v i ) i∈[1..xs] ∈ V xs , ( ∀(i, j) ∈ [1..x s ] 2 , i = j ⇒
The set of SEDs offering a service Loc(S, 2)

(v i = v j ∧ AT T 3 V i = AT T 3 V j )) ∧ (∀k ∈ [1..x s ], AT T 1 v k = "SED" ∧s ∈ AT T 2 V k is dispatched on at least 2 different machines Occ(p 4 ) + Occ(p 5 ) ≤ Occ(p 1 ) + Occ(p 2 ) + Occ(p 3 ). (3)
Since p 1 consumes the axiom, it is obvious that

Occ(p 1 ) = 1. (4)
Equation ( 2) thus becomes :

Occ(p 2 ) + Occ(p 3 ) + Occ(p 6 ) + Occ(p 7 ) ≤ maxAgents -3. (5)
By definition, ∀ p ∈ P DIET , Occ(p) ≥ 0. Accordingly, equations (3), ( 4) and [START_REF] Baresi | Stylebased modeling and refinement of service-oriented architectures[END_REF] give

Occ(p 4 ) + Occ(p 5 ) ≤ maxAgents -2. ( 6
)
According to equation (1), |S| = Occ(p 1 ) + (Occ(p 2 ) + Occ(p 3 ) + Occ(p 6 ) + Occ(p 7 )) + (Occ(p 4 ) + Occ(p 5 )). Thanks to equations (4), ( 5) and ( 6), this translates into |S| ≤ 1 + (maxAgents -3) + (maxAgents -2).

Finally, |S| ≤ 2*maxAgents-4. With maxAgents = 100, we have |S| ≤ 196. QED.

Appropriateness Evaluation

To enable the evaluation of DIET configurations, constraints are herein assigned a, potentially infinite, weight. In this way, the appropriateness of a configuration is reflected by calculating its opposite, i.e. the configuration cost. Said cost is calculated as the sum of the costs of its energy consumption and of the violated constraints. The violation of a constraint in a configuration implies that every defined criteria is not respected. In this case, the configuration is not robust enough and its cost is therefore increased depending on the weight of the violated constraint. A configuration of infinite weight is considered incorrect, so that strong constraints are still enforced.

Notations Let ξ be the function of evaluation; ∀ cons ∈ CONS, ∀ c ∈ cons, ξ (c) = 1 if c is "true" and 0 else.

Energy Consumption In Sec. 3, it has been presumed that energy consumption depends on the used machines and the number of deployed components only. In the following, this relation is (realistically according to [START_REF] Borgetto | Energy-aware service allocation[END_REF]) assumed to be linear, and weighted by λ mach and λ entity for used machine and deployed component, respectively. Note that the number of current deployed component is already an attribute of the graph. For an easier evaluation, the number of used machines can be added as attribute of the graph as well, and updated whenever necessary, i.e. when applying production p 1 , p 4 , p 5 , p 6 or p 7 . The energy consumed by a configuration is then:

λ mach • A 5 G + λ entity • |V |.
Constraint violations It is clear that the constraint reflecting the limitation on the number of entities managed by the MA should not be violated and therefore has an infinite weight.

Constraints reflecting the robustness of the system are, however "soft" and are given arbitrary finite weight. The cost of violating the constraint stating that "a LA and a component managed by the same entity should not be deployed on the same machine or they should have disjoint set of carried services", c(v), is weighted by the depth of the LA. Redundancy and location constraints are weighted by λ R and λ L respectively.

The cost related to the violation of constraints is :

λ L ξ (CONS 1 G ) + λ R ξ (CONS 2 G ) + λ MA Σ ma∈V,A 1 ma ="MA" ξ (CONS 1 ma ) + Σ la∈V,A 1 la ="LA" λ LA (A 2 la ξ (CONS 1 la ).
Part of the configuration illustrated in Fig. 2 is arbitrarily instantiated to be totally evaluable and presented in Fig. 9. S, the set of services that may be carried out by a SED, is {S 1 , S 2 , S 3 }. This configuration does not meet the redundancy constraint, since there are only two SEDs that can carry out the services S1 and S2. Hence, its cost is equal to its energy consumption plus the cost of violating said constraint: 3λ mach + 7λ entity + λ R .

This natural and immediate way to deal with soft and hard requirements derives from the new formalism proposed in this paper. In fact, the model has been explicitly conceived to embed constraints, that may assume the role of performance indicator, and their admissible soft bounds by means of attributes. In this way, once the software architecture properly described, its appropriateness can be easily evaluated on a dynamical basis.

Non-Functional Requirements and Software Management

Thanks to the eased manipulation of system attributes and constraints, the introduced formalism can be fruitfully exploited in software management systems. Semantic predicates and restrictions on rules' applicability grant more flexibility on transformations, allowing to face specific aims on the fly.

Remark 3

Considering a new rule resulting of the restriction of another can ensure guarantees with regard to the preservation of the architectural style. However, it is worth noticing that properties of the graph rewriting system, e.g. confluence, are not necessarily invariant with regard to the addition of a new rule.

Let's consider the DIET configuration previously evaluated (see Fig. 9). In this case, we can suppose that a SED is to be deployed to meet the redundancy constraint and improve the quality of the configuration.

The first thing to do is to apply p 2 , and by doing so choosing the component that will manage the SED. To find an optimum solution, one should consider each possibility, i.e. apply p 2 on v 2 , v 3 or v 4 , find in each case an optimal solution, and then compare the costs of each solutions. Arbitrarily assuming that p 2 has been applied on v 2 , an optimal solution can be found as follows. The temporary vertex is to be instantiated into a SED using the production p 5 . Since the motivation of this reconfiguration is to meet the redundancy constraint, p 5 should be restricted in order for its application to be relevant. Firstly, the deployed SED should be able to provide the services S1 and S2. Assuming the notation introduced when defining p 5 , see Fig. 7, {S1, S2} ⊆ A 2 pv4 . Furthermore, the constraint ("M2" != A 3 pv4 ) ∨( "{S1,S2,S3}" ∩ A 2 pv4 = / 0 ) will appear on v 3 . In order for this constraint to be met, the transformation should verify that A 3 pv4 = "M2". Besides, for energy consumption reason and so as not to use a new machine, it is imposed that A 3 pv4 ∈ {M1, M3}.

According to the style constraints, the graph presented in Fig. 10 is a possible optimal result of such a reconfiguration.

Every constraints are met and the cost of the configuration is now limited to its energy consumption, 3λ mach + 8λ entity . Hence, this evolution is relevant if and only if λ entity < λ R .

Transformational Scenario

The transformation conducted in the experiments consists in the addition of a SeD on a LA of maximal depth. This transformation implies two attribute updates. Firstly, the attribute representing the number of entities managed by the LA has to be incremented. Secondly, the introduction of a SeD may impact the services carried out by its ancestors. The appended SeD provides a formerly un-carried service. As a consequence, the set of services carried out by each of its ancestors has to effectively be modified.

Following the method introduced in this paper, this transformation is a sequential composition of the rules p 3 and p 5 presented in Sec. 5.1.3. Attribute updates are realized through µ inc and µ updateServ .

Manipulated Configurations

In this experimental part, we now consider a non-simplified DIET architecture. The corresponding type graph is repre- sented in Fig. 11. A configuration may contain several connected MAs. As a result, a configuration may exhibit cycles. The manipulated graphs possess the following characteristics :

-Each of them has several MAs and at least one cycle.

-Trees composed by sub-graphs induced by a MA alongside the LAs and SeDs it manages do not have the same height. Within such a tree, SeDs do not necessarily have the same depth. -There exists no n such as any of these trees is n-ary.

-Each non-intermediary LA manages at least 100 SeDs.

Considered configurations have various sizes and heights. The size of a configuration is the total number of components it is composed by. Its height is the greatest number of LAs between a MA and a SeD. The smallest transformed graph is illustrated in Fig. 12. In this figure, blue and red circle represent LAs and MAs, respectively. The OMNI is illustrated as a red rounded rectangle.

Size and height of graphs significantly influence the scenario execution. In native methods, the height of a graph is equal to the number of rule applications. The complexity of a rule application is strongly related to the size of the graph. In a more superficial way, it does also depend on the topology of the graph and, thus, on its number of MAs. Here, the effect of the graph topology on rule application is not relevant for our study. Therefore, configurations intervening in the experimentations have a fixed number of MAs, set to 3.

Tested Tools and Methods

Experimentations are conducted using two different tools : AGG and GMTE. Both enable the modification of any attribute belonging to the right hand side of a rule. For each engine, experiments are conducted using three methods :

-A referential that does not include attribute modifications. It allows the estimation of time required to carry attribute modifications. -The native method of the engine. This last consists in a sequence of rule applications. Firstly, the SeD is added to a LA whose set of carried out services is updated. Then, a rule is successively applied to impact this update on each of its ancestors. Each application updates a single LA since modified attributes have to be within the scope of the rule. -The method proposed in this paper. To this end, we have implemented two overlays relying on AGG and GMTE that carry out the execution of rules p 3 and p 5 with mutators.

Considering two different tools show that the proposed method and the conclusion drawn from experiments are engineagnostic.

Experimental Results

Figures 13 and 15 illustrate, for GMTE and AGG respectively, the execution times of the transformational scenario using native methods and mutators. They are represented alongside a referential time computed in absence of attribute modification. Figures 14 and16 show the evolution of these times for bigger graphs. Illustrated execution times are the median result on 100 executions. Experimentations have been conducted on a computer possessing a quad core processor Each configuration is characterized by its size and its height.

h = 2 0 , s = 1 7 5 0 h = 2 0 , s = 2 0 0 0 h = 2 0 , s = 2 2 5 0 h = 2 0 , s = 2 5 0 0 h = 2 0 , s = 2 7 5 0 h = 2 5 , s = 1 0 0 0 h = 2 5 , s = 1 2 5 0 h = 2 5 , s = 1 5 0 0 h = 2 5 , s = 1 7 5 0 h = 2 5 , s = 2 0 0 0 h = 2 5 , s = 2 2 5 0 h = 3 0 , s = 1 0 0 0 h = 3 0 , s = 1 2 5 0 h = 3 0 , s = 1 5 0 0 h = 3 0 , s = 1
Firstly, experimental results show that the overhead implied by attribute modifications through mutators is small in regard of the total transformational time. For example, attribute modifications represent 7 of the 325ms required to conduct the scenario on a configuration of size 1000 and height 5 for GMTE, and 1.2 of the 24.8 ms in the case of AGG. This value increases linearly in height and remains roughly invariant with regard to size. For a configuration of size 2250 and height 30 it amounts to 58 out of 3010ms and 2.7 out of 36.5ms, using GMTE and AGG respectively. Secondly, mutators significantly ameliorate the efficiency and scalability of system modifications with respect to classic methodologies. Figure 17 depicts the evolution of the the execution time ratio of natives methods to mutators. Considering a configuration of size 1750 and height 20, for example, this ratio is roughly equal to 14 for GMTE (from 16952 to 1192 ms) and 5.3 for AGG (from 154 to 28.9 ms). It increases with height and logarithmically decreases with size. For example, the considered ratio goes up to 27 for the GMTE (from 103796 to 3807 ms) and 8.3 for AGG (from 330 to 39.6 ms) when considering a configuration of height 30 and size 2500. Unlike the considered ratio, the net gain, i.e. the difference of execution times, is strictly increasing These results can be explained by the fact that the proposed method requires a single rule application followed by the execution of a mutator that is linear with regard to depth. The native methods require d rule applications to update attributes within a graph of height d. A rule application itself has a polynomial executional complexity with regard to the size of the graph for AGG, while it is exponential for GMTE. The net gain increases with the application time of a rule.

h = 5 , s = 1 2 5 0 h = 1 0 , s = 1 0 0 0 h = 1 0 , s = 1 2 5 0 h = 1 0 , s = 1 5 0 0 h = 1 0 , s = 1 7 5 0 h = 1 5 , s = 1 0 0 0 h = 1 5 , s = 1 2 5 0 h = 1 5 , s = 1 5 0 0 h = 1 5 , s = 1 7 5 0 h = 1 5 , s = 2 0 0 0 h =
The results are not independent from the chosen scenario. Here occurs a propagating modification of attributes that is a typical example of the domino effect evoked in Sec. 2. However, the scenario also comprised the worst comparison case, namely the incrementation of the number of managed components. Since this last impacts attribute within the scope of the rewriting rule solely, mutators are in this case equivalent to classical, native, methods.

Conclusion

Dynamic software architectures enable adaptation in evolving distributed systems. They focus on two particular aspects which are usually considered separately: correctness and appropriateness with regard to functional and non-functional requirements. Graph and graph rewriting based methodologies are appropriate for designing correct-by-construction reconfigurations of dynamic systems, effectively guaranteeing their consistency by requiring little or no verification in run-time. Their genericness allows the representation of a vast range of systems in different fields, including dynamic software architectures.

With reference to DIET, an industrial application contributing in federating and managing hybrid HPC environment, this article first shows that currently available graph based methods exhibit limitations in handling varying attributes and constraints. Then, an extension of graph grammars is proposed so as to lift the highlighted restrictions. The pivotal features of this new formalism are: mutators, admissible relationships specification, and constraint oriented encoding. The firsts are introduced within graph rewriting rules as a lightweight approach to attribute and constraint modifications. On the other hand, attribute interdependencies are expressed through algebraic operators that allow to characterize admissible relationships. Finally, to ease application management operations, the appropriateness of a configuration in accordance to functional and non-functional requirements is reflected by constraints. Noticeably, to cope also with unknown attributes, constraints are defined as elements of a ternary logic systems.

The application of the resulting formalism to the specification of DIET demonstrates its fitness for the management of systems subordinate to functional and non-functional requirements. Experimental results show that reconfiguring a graph of size 2500 with mutators rather than existing methods is up to 27 times quicker on GMTE and 8.3 times quicker on AGG. This improvement allows to efficiently asses characteristics of the system by combining evaluation on demand and/or update on modification. In turn, this allows to quickly grasp the appropriateness of a configuration, identify objectives that can be ameliorated, and component implying constraints violation.

The initiated extension of AGG is currently being further developed so as to hide the complexity of the formalism within a graphical and user-friendly automated tool. In parallel, mechanisms to take advantage of this new model are being integrated within FRAMESELF [START_REF] Alaya | Frameself: A generic context-aware autonomic framework for selfmanagement of distributed systems[END_REF], a multi-model framework for self-management of distributed systems. Also, ongoing research is exploring the suitability of the proposed formalism to time-constraints. Another interesting future development would be the consideration of infinite logic systems. These lasts provide a more precise way of transforming qualitative properties into quantitative one, by linking, for example, robustness to failure probability.

Fig. 1

 1 Fig. 1 Logical view of a DIET configuration, with and without an OMNI

Fig. 2

 2 Fig. 2 An AC-graph modeling a configuration of DIET

Fig. 3 µFig. 4 Fig. 5

 345 Fig. 3 µ inc(v, i, n), Incrementation of the i-th attribute of the element e by n

Fig. 7 Fig. 8

 78 Fig. 7 Instantiation of a non-terminal term into a SED

Fig. 9

 9 Fig. 9 Instantiated AC-graph modelling a configuration of DIET

Fig. 10 A

 10 Fig. 10 A configuration satisfying every style-defined constraints

Fig. 11

 11 Fig. 11 Experimental DIET style

Fig. 12

 12 Fig. 12 Smallest experimental graph: A DIET configuration of size 1000 and height 5.

  Fig. 13 GMTE : execution times

Fig. 14

 14 Fig. 14 GMTE : scalability comparison

Fig. 16

 16 Fig. 15 AGG : execution times

Fig. 17 Fig. 18

 1718 Fig. 17 Native methods vs. mutators : ratio of execution times

Table 1

 1 Main Notations for the DIET use-case.

	Notation	Meaning
	LA(d)	the set of LA of depth d
	M(c)	the number of entities managed by the component c
	maxSonsMA the maximum number of entities managed
	maxSonsLA	by the MA or a LA, respectively
	minSonsMA	the minimum number of entities managed
	minSonsLA	by the MA or a LA, respectively
	maxσ	threshold value of the balancing condition

  a set of attributes, ATT rule being the set of attributes of the graph rewriting rule itself, -CONS = CONS rule ∪ CONS R\K is a set of constraints, CONS rule being the set of constraints of the graph rewriting rule itself and CONS R\K set of constraints on E R\K ∪V R\K , -

Table 3

 3 Informal considerations and their formal translationNotationFormal expression DescriptionTemporary vertexes in R p 1 , R p 6 and R p 7The MA and LAs are deployed alongside with minSonsMA and minSonsLA temporary vertexes, respectively

	CONS MA	Nsons < A 2 AX

  36. Selonen P, Xu J (2003) Validating uml models against architectural profiles. SIGSOFT Software Engineering Notes 28:pp.58-67 37. Sharrock R, Monteil T, Stolf P, Hagimont D, Broto L (2011) Non-intrusive autonomic approach with selfmanagement policies applied to legacy infrastructures for performance improvements. Int J Adapt Resilient Auton Syst 2(1):pp. 58-76 38. Simalatsar A, Guo L, Bozga M, Passerone R (2012) Integration of correct-by-construction bip models into the metroii design space exploration flow. In: 30th IEEE International Conference on Computer Design (ICCD), pp 490-491 39. Tahar BM, Taoufik SR, Mourad K (2013) Checking non-functional properties of uml2.0 components assembly. In: 22nd IEEE International Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp 278-283 40. Wermelinger M, Fiadeiro JL (2002) A graph transformation approach to software architecture reconfiguration. Science of Computer Programming 44(2):pp. 133 -155, special Issue on Applications of Graph Transformations (GRATRA 2000)

http://groove.cs.utwente.nl/

AGG: http://tfs.cs.tu-berlin.de/agg.

GMTE: http://homepages.laas.fr/khalil/GMTE

http://www.sysfera.com/sysfera-ds.html

context of SOP project ANR-11-INFR-001