Manamiary Bruno Andriamiarina
email: manamiary.andriamiarina@loria.fr

Dominique Méry
email: dominique.mery@loria.fr

Neeraj Kumar Singh
email: singhn10@mcmaster.ca

Analysis of Self-⋆ and P2P Systems using Refinement ⋆

Keywords: Distributed systems, self-⋆, self-healing, self-stabilization, P2P, EVENT B, liveness, service-as-event

Distributed systems and applications require efficient and effective techniques (e.g. self-(re)configuration, self-healing, etc.) for ensuring safety, security and more generally dependability properties, as well as convergence. The complexity of these systems is increased by features like dynamic (changing) topology, interconnection of heterogeneous components or failures detection. This paper presents a methodology for verifying protocols and satisfying safety and convergence requirements of the distributed self-⋆ systems. The self-⋆ systems are based on the idea of managing complex infrastructures, software, and distributed systems, with or without minimal user interactions. Correct-by-construction and service-as-event paradigms are used for formalizing the system requirements, where the formalization process is based on incremental refinement in EVENT B. Moreover, this paper describes a fully mechanized proof of correctness of the self-⋆ systems along with an interesting case study related to the P2P-based self-healing protocol.

Introduction

Nowadays, our daily lives are affected by various advanced technologies including computers, chips, and smart-phones. These technologies are integrated into distributed systems with different types of complexities like mobility, heterogeneity, security, faulttolerance, and dependability. Distributed systems are largely used in many applications and provide required functionalities from the interactions between a large collection of possibly heterogeneous and mobile components (nodes and/or agents). Within the domain of distributed computing, there is an increasing interest in the self-stabilizing systems, which are able to autonomically recover from occurring the faults [START_REF] Dolev | Self-Stabilization[END_REF]. The autonomous property of the self-⋆ systems tends to take a growing importance in the analysis and development of distributed systems. It is an imperative that we need to get a better understanding of the self-⋆ systems (emergent behaviours, interactions between agents, etc.), if we want to reason about their security, correctness and trustworthiness.

Fortunately, the formal methods community has been analysing a similar class of systems for years, namely distributed algorithms.

In this study, we use the correct by construction approach [START_REF] Leavens | Roadmap for enhanced languages and methods to aid verification[END_REF] for modelling the distributed self-⋆ systems. Moreover, we also emphasize the use of the service-asevent [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF] paradigm, that identifies the phases of self-stabilization mechanism, which can be simplify into more stable and simple coordinated steps. We consider that a given system S (see in Fig. 1) is characterized by a set of events (procedures modelling either phases or basic actions according to an abstraction level) that modifies the state of the system. Legal states (correct states) satisfying a safety property P are defined by a subset C L of possible events of the system S. The events of C L represent the possible big or small computation steps of the system S and introduce the notion of closure [START_REF] Berns | Dissecting self-* properties[END_REF],

Legal States

e∈C L Ù Ù f ∈F A A Illegal States r∈S T Õ Õ Recovery States f ∈F s s r∈C V r∈S T v v
where any computation starting from a legal state satisfying the property P leads to another legal state that also satisfies the property P. The occurrence of a fault f leads the system S into an illegal state (incorrect state), which violates the property P. The fault f is defined as an event f that belongs to a subset F of events. When considering the hypothesis of having a self-⋆ system, we assume that there are procedures (protocols or actions) which implement the identification of current illegal states and recovery for legal states. There is a subset ST of events modelling recovery phases for demonstrating the stabilization process. The system recovers using a finite number of stabilization steps (r). The process is modelled as an event r of C V (⊆ ST ) eventually leading to the legal states (convergence property) from recovery states. During the recovery phase, a fault may occur (see dotted transitions in Fig. 1).

The system S can be represented by a set of events M = C L ∪ ST ∪ F , where the model M contains a set (C L) of events for representing the computation steps of the system S. When a fault occurs, a set (S T ) of events simulates the stabilization process that is performed by S. The formal representation expresses a closed model but we do not know what is the complete set of events modelling faults/failures. We characterise the fault model in a very abstract way and it may be possible to develop the fault model according to the assumptions on the environment, but we do not consider this in the current study. We restrict our study by making explicit the events of ST modelling the stabilization of the system from illegal/failed states. We ensure that the convergence is always possible: a subset C V of ST eventually leads S into the legal states satisfying the invariant P of the system. Whenever the system S is in a legal state, we consider that the events of ST are either not operative or simply preserve the invariant P of the system.

In the previous paragraph, we name procedures ( protocols or actions) by the term events. An event is modelling a process which is defined by its pre and post specifications or a state transformation belonging to a larger process. It means that we need to play with abstraction levels to develop a self-⋆ system. For instance, one can state that an event called stabilise is ensuring the functionality of getting a stable system (the what) without giving details of the detailed process itself (the how). Hence, the notion of event is identified to an abstraction level and can be either modelling a global process (the what) or a local update of a variable (the how). We formalise the system S using the EVENT B modelling language [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF], dealing with events and invariant properties including convergence properties by using a temporal framework. The service-asevent paradigm [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF] helps to express this concretisation process: the procedures (1) leading from the illegal states to the recovery states, and (2) leading from the recovery states to the legal states are stated by (abstract) events, during the first stages of the EVENT B development. The next step is to unfold each (abstract procedure) event, by refinement, to a set of coordinated and concrete events, which form the body of the procedure.

This paper is organised as follows. Section 2 presents related works. Section 3 introduces the EVENT B modelling framework including service-as-event paradigm and a formal definition of self-⋆ systems. Section 4 presents the formal verification approach and illustrates the proposed methodology with the study of the self-healing P2P-based protocol [START_REF] Marquezan | Self-* and P2P for Network Management -Design Principles and Case Studies[END_REF]. Section 5 discusses on approaches for studying temporal properties for EVENT B models. Finally, Section 6 concludes the paper along with future work.

2 Related Works on Formal Modelling for Self-⋆ Systems Systems usually run in intricate environments, with frequent and unexpected changes. This feature increases interest towards autonomous and self-⋆ architectures, as they are able to adapt themselves according to the changes that may occur in the systems (faults, etc.) or in the environment. Applying formal methods to self-⋆ systems originates from the needs of understanding how these systems behave and how they meet their specifications. A self-⋆ system relies on emergent behaviours, resulting from interactions between components of the system [START_REF] Smith | Formal development of self-organising systems[END_REF].

Traditionally, the correctness of self-⋆ and autonomous systems is validated through the simulation and testing [START_REF] Puviani | A method fragments approach to methodologies for engineering self-organizing systems[END_REF][START_REF] Sudeikat | Design and simulation of a wave-like self-organization strategy for resource-flow systems[END_REF]. However, simulation and testing are not sufficient to cover the whole set of possible states of a system [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF]. Therefore, formal methods appear as a promising land for validating self-⋆ systems, as long as formal techniques can assert the correctness of these systems and certify target properties, like trustworthiness, security, efficiency, etc. under the rigorous mathematical reasoning [START_REF] Calinescu | Formal methods for the development and verification of autonomic it systems[END_REF][START_REF] Güdemann | Safety and dependability analysis of self-adaptive systems[END_REF][START_REF] Weyns | A survey of formal methods in self-adaptive systems[END_REF].

Smith et al. [START_REF] Smith | Formal development of self-organising systems[END_REF] have applied the stepwise refinement using Z to study a case of selfreconfiguration, where a set of autonomous robotic agents is able to assemble and to reach a global shape. They do not validate models using an adequate tool (e.g. proof checker, proof assistant, etc.) and models are not localized. Calinescu et al. [START_REF] Calinescu | Formal methods for the development and verification of autonomic it systems[END_REF] have used Alloy to demonstrate the correctness of the autonomic computing policies (ACP). However, Alloy does not provide a mechanism for expressing the correct-by-construction paradigm. Méry et al. [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] have also investigated a self-reconfiguring system (Network-on-Chip: adaptative XY routing) using the EVENT B framework and the correct-by-construction approach.

State exploration approaches such as model-checking are also used to study self-⋆ systems. Model-checkers like SPIN, PRISM, SMV, UPPAAL are used for properties specification and getting evidences that properties, such as flexibility, robustness of the self-⋆ systems hold [START_REF] Calinescu | Formal methods for the development and verification of autonomic it systems[END_REF][START_REF] Güdemann | Safety and dependability analysis of self-adaptive systems[END_REF][START_REF] Iftikhar | A case study on formal verification of self-adaptive behaviors in a decentralized system[END_REF][START_REF] Weyns | A survey of formal methods in self-adaptive systems[END_REF]. Moreover, these tools allow users to obtain the metrics for the self-⋆ systems, such as performance, and quantitative evaluations [START_REF] Calinescu | Formal methods for the development and verification of autonomic it systems[END_REF][START_REF] Güdemann | Safety and dependability analysis of self-adaptive systems[END_REF][START_REF] Iftikhar | A case study on formal verification of self-adaptive behaviors in a decentralized system[END_REF][START_REF] Weyns | A survey of formal methods in self-adaptive systems[END_REF]. Model-checking and state-space evaluation can be used during the conception of self-⋆ systems, but they are especially used for runtime verification [START_REF] Iftikhar | A case study on formal verification of self-adaptive behaviors in a decentralized system[END_REF][START_REF] Weyns | A survey of formal methods in self-adaptive systems[END_REF]. The limit of model checking is clearly the size of models.

Other formal techniques like static analysis and design by contract are also applied for the formal specification of self-⋆ systems [START_REF] Tosi | Research perspectives in self-healing systems[END_REF]. These techniques are mainly used for runtime verification. Graphical approaches, such as Petri Nets, are used to model the temporal aspects and communication flows between different components of a self-⋆ system, and helped to study the cases like self-reconfiguration (replacement of a component, removal of a link between two components, etc.) [START_REF] Weyns | A survey of formal methods in self-adaptive systems[END_REF].

Finally, graphical notations (e.g. UML) help to represent self-⋆ systems with understandable figures [START_REF] Weyns | Forms: Unifying reference model for formal specification of distributed self-adaptive systems[END_REF]. Their general purpose is to provide users an insight of a self-⋆ system by describing its architecture, the relationships between agents of the system (OperA methodology [START_REF] Penserini | Adaptivity within an organizational development framework[END_REF], ADELFE [START_REF] Puviani | A method fragments approach to methodologies for engineering self-organizing systems[END_REF]) or by presenting the system as a composition of extendable/instantiable primitives (FORMS [START_REF] Weyns | Forms: Unifying reference model for formal specification of distributed self-adaptive systems[END_REF]). These notations are generally graphical front-ends for the more complex representations of self-⋆ systems, where the source code [START_REF] Puviani | A method fragments approach to methodologies for engineering self-organizing systems[END_REF], and formal models [START_REF] Weyns | Forms: Unifying reference model for formal specification of distributed self-adaptive systems[END_REF] can be generated from the notations.

Our proposed methodology integrates the EVENT B method and elements of temporal logics. Using the refinement technique, we gradually build models of self-⋆ systems in the EVENT B framework. Moreover, we use the service-as-event paradigm to describe the stabilization and convergence from illegal states to legal ones. Self-⋆ systems require the expression of traces properties like liveness properties and we borrow a minimal set of inference rules for deriving liveness properties. The concept of refinement diagrams intends to capture the intuition of the designer for deriving progressively the target self-⋆ system. The RODIN platform provides a laboratory for checking, animating and validating the formal models.

3 Modelling Framework

EVENT B

We advocate the use of correct-by-construction paradigm for modelling the self-⋆ systems. The key concept is the incremental refinement (simulation) which provides link between discrete models by preserving properties. The EVENT B modelling language designed by Abrial [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] is based on set theory and the refinement of models: an abstract model expressing the requirements of a given system can be verified and validated easily; a concrete model corresponding to the actual system is constructed progressively by refining the abstraction. EVENT B is supported by a complete toolset RODIN [START_REF]Rigorous open development environment for complex systems[END_REF] providing features like refinement, proof obligations generation, proof assistants and model-checking.

Modelling Actions over States

The EVENT B modelling language can express safety properties, which are either invariants or theorems in a model corresponding to the system. Two main structures are available in EVENT B : (1) Contexts express static informations about the model (for instance, graph properties as connectivity); (2) Machines express dynamic informations about the model, safety properties, and events. An EVENT B model is defined by a context and a machine. A machine organises events (or actions) modifying state variables and uses static informations defined in a context. An EVENT B model is characterised by a (finite) list x of state variables possibly modified by a (finite) list of events. An invariant I(x) states properties that must always be satisfied by the variables x and maintained by the activation of the events. The general form of an event e is as follows: ANY t WHERE G(t, x) THEN x : |P(t, x, x ′ ) END and corresponds to the transformation of the state of the variable x, which is described by a before-after predicate BA(e)(x, x ′ ): the predicate is semantically equivalent to ∃t • G(t, x) ∧ P(t, x, x ′ ) and expresses the relationship linking the values of the state variables before (x) and just after (x ′ ) the execution of the event e. Proof obligations are produced by RODIN, from events: INV1 and INV2 state that an invariant condition I(x) is preserved; their general form follows immediately from the definition of the before-after predicate BA(e)(x, x ′ ) of each event e; FIS expresses the feasibility of an event e, with respect to the invariant I. By proving feasibility, we achieve that BA(e)(x, z) provides a next state whenever the guard grd(e)(x) holds: the guard is the enabling condition of the event.

Model Refinement The refinement of models extends the structures described previously, and relates an abstract model and a concrete model. This feature allows us to develop EVENT B models of the self-⋆ approach gradually and validate each decision step using the proof tool. The refinement relationship is expressed as follows: a model AM is refined by a model CM, when CM simulates AM (i.e. when a concrete event ce occurs in CM, there must be a corresponding enabling abstract event ae in AM). The final concrete model is closer to the behaviour of a real system that observes events using real source code. The relationships between contexts, machines and events are illustrated by the following diagrams (Fig. 2) , which consider refinements of events and machines.

Fig. 2: Machines and Contexts relationships

The refinement of a formal model allows us to enrich the model via a step-by-step approach and is the foundation of our correct-by-construction approach [START_REF] Leavens | Roadmap for enhanced languages and methods to aid verification[END_REF]. Refinement provides a way to strengthen invariants and to add details to a model. It is also used to transform an abstract model to a more concrete version by modifying the state description. This is done by extending the list of state variables (possibly suppressing some of them), by refining each abstract event to a set of possible concrete versions, and by adding new events. We suppose (see Fig. 2) that an abstract model AM with variables x and an invariant I(x) is refined by a concrete model CM with variables y. The abstract state variables, x, and the concrete ones, y, are linked together by means of a, so-called, gluing invariant J(x, y). Event ae is in abstract model AM and event ce is in concrete model CM. Event ce refines event ae. BA(ae)(x, x ′ ) and BA(ce)(y, y ′ ) are predicates of events ae and ce respectively; we have to discharge the following proof obligation: I(x) ∧ J(x, y) ∧ BA(ce)(y, y ′ ) ⇒ ∃x ′ • (BA(ae)(x, x ′ ) ∧ J(x ′ , y ′ ))

Due to limitations on the number of pages, we have briefly introduced the EVENT B modelling language and the structures proposed for organising the formal development. However, more details are available in [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] and on the Internet 1 . In fact, the refinementbased development of EVENT B requires a very careful derivation process, integrating possible tough interactive proofs. For assisting the development of the self-⋆ systems, we use the service description and decomposition that is provided by the service-as-event [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF] paradigm (derived from the call-as-event approach [START_REF] Méry | Refinement-based guidelines for algorithmic systems[END_REF]).

The Service-as-Event Paradigm

This section introduces the refinement diagrams [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF][START_REF] Méry | Refinement-based guidelines for algorithmic systems[END_REF] and presents the service-as-event paradigm. A brief overview on the usage of these formalisms for modelling the self-⋆ systems is given.

Objectives The service-as-event paradigm [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF][START_REF] Méry | Refinement-based guidelines for algorithmic systems[END_REF] is a semantical extension of EVENT B and introduces a way to deal with liveness properties and traces, for modelling the self-⋆ systems.

A Definition of Self-⋆ Mechanism We characterize a self-stabilizing system S (more generally a self-⋆ system) by its ability to recover autonomously from an illegal (faulty) state (violating the invariant P of the system) to a legal (correct) state statisfying the invariant property P of system S. Temporal logic [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF][START_REF] Lamport | The temporal logic of actions[END_REF][START_REF] Méry | Refinement-based guidelines for algorithmic systems[END_REF][START_REF] Prasetya | Formal design of self-stabilizing programs: Theory and examples[END_REF] can be used to describe such mechanism, using the liveness properties: we represent the stabilization (especially the convergence) property as a service where a system S, in an illegal state (characterized by ¬P), reaches eventually a legal state (satisfying P). This service is expressed, with the leads to ( ) operator, as follows: (¬P) P. This leads to property (equivalently ((¬P) ⇒ ⋄P)) states that every illegal state (satisfying ¬P) will eventually (at some point in the future) lead to a legal state (satisfying P).

We define a temporal framework for the EVENT B model M of the studied system S by the following TLA specification: S pec(M): Init(y) ∧ [Next] y ∧ L, where Init(y) is the predicate specifying initial states; Next ≡ ∃e ∈ E.BA(e)(y, y ′ ) is an action formula representing the next-state relation; and L is a conjunction of formulas W F y (e) : we express a weak fairness assumption over each event e modelling a step of the recovery process (we do not add any fairness on events leading to illegal states (faults)).

Refinement Diagrams We express the self-⋆ mechanism using EVENT B , together ¬P with liveness properties under fairness assumptions. Refinement diagrams (see in Fig. 3), introduced by Méry et al in [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF][START_REF] Méry | Refinement-based guidelines for algorithmic systems[END_REF], allow to develop EVENT B models and add control inside these models. They are also used for stating (proofs of) liveness properties (under fairness assumptions), and for supporting refinement. Therefore, these diagrams are suitable for representing the models of self-⋆ systems. A refinement diagram D = PD(M) for a machine M is defined as follows: PD(M) = (A, M, G, E), where A is a set of assertions, G a set of assertions for M called conditions/guards of the form g(x), E is the set of events of M. The diagram PD(M) is a labelled directed graph over A, with labels from G or E , satisfying the following rules:

(1) if an assertion R is related to another assertion S, by an unique non-dotted arrow labelled e ∈ E (where e does not model a fault), then the property R S is satisfied; [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] if R is related to S 1 , . . . S p , then each arrow from R to S i is labelled by a guard g i ∈ G. The diagram D possesses proved properties:

1. If M satisfies P Q and Q R, it satisfies P R. [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF]. If M satisfies P Q and R Q, it satisfies (P ∨ R) Q. [START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF]. If I is invariant for M and if M satisfies P ∧ I Q, then M satisfies P Q. [START_REF] Andriamiarina | Analysis of self-* and p2p systems using refinement[END_REF]. If I is invariant for M and if M satisfies P ∧ I ⇒ Q, then M satisfies P Q. [START_REF] Berns | Dissecting self-* properties[END_REF]. If P e -→ Q is a link of D for the machine M, then M satisfies P Q. [START_REF] Calinescu | Formal methods for the development and verification of autonomic it systems[END_REF]. If P and Q are two nodes of D such that there is a path in D from P to Q and any path from P can be extended in a path containing Q, then M satisfies P Q. [START_REF] Dolev | Self-Stabilization[END_REF]. If I, U, V , P, Q are assertions such that I is the invariant of M; P ∧ I ⇒ U; V ⇒ Q; and there is a path from U to V and each path from U leads to V ; then M satisfies P Q.

These refinement diagrams are attached to EVENT B models and are used for deriving liveness properties. As an example, the diagram in Fig. 3 represents a model of a self-stabilizing system: the diagram relates a pair of assertions (¬P, P), where ¬P is a precondition stating that the studied system is in an illegal state (P does not hold); and P is the post-condition, describing the desired legal state. We observe that the leads to property (¬P) P, demonstrating the stabilization and convergence, is satisfied by the diagram and the model linked to it.

following property: (¬P) P. An abstract event (e) is used for describing the service/procedure represented by (¬P) P: (¬P) e -→ P; where (¬P) is a pre-condition for triggering event (e); and P is a post-condition defined by the actions of event (e), which should be satisfied by the "execution" of event.

2. Decomposing stabilization and convergence into simple steps. We decompose the abstract service stated by (¬P) P into simple sub-procedures/steps, using the inference rules [START_REF] Lamport | The temporal logic of actions[END_REF] related to the leads to properties: Fig. 4: Proof Tree -Usage of Inference Rules This process is similar to refinement (see Fig. 5), since we add, at each level of the proof tree, a new state R k (0 ≤ k ≤ n) leading from (¬P) to P. The initial property (¬P) P is decomposed, until the identification of the stabilization steps is satisfactory. The stabilization phase is expressed by the property Fig. 5: Decomposition and Refinement

(¬P) R 0 ∧ R 0 R 1 ∧ . . . ∧ R n-1
R n ∧ R n P, which states the convergence leading to the desired legal states. Each level of the proof tree corresponds to a level of refinement (see Fig. 5) in the formal development. Each leads to property demonstrates a service of stabilization, which is defined by an event in the model. [START_REF] Andriamiarina | Analysis of self-* and p2p systems using refinement[END_REF] Stepwise Design of the Self-Healing Approach The development of self-healing P2P-based approach is proposed by Marquezan et al. [START_REF] Marquezan | Self-* and P2P for Network Management -Design Principles and Case Studies[END_REF], where system reliability is the main concern. The self-healing process ensures the maintenance of proper functioning of the system services. If a service fails then it switches from a legal state to a faulty state. The self-healing/recovery procedure ensures that the service switches back to the legal state. The services run in a distributed (P2P) system composed of agents/peers executing instances of tasks. The services and peers notions are introduced as: (1) Management Services: Tasks/Services are executed by the peers; (2) Instances of Management Services: Peers executing a certain type of management service; (3) Management Peer Group (MPG): Instances of the same management service. The self-healing property can be described as follows: (1) Selfidentification triggers to detect the failure of service. This mechanism identifies running or failed instances of a management service. (2) Self-activation is started, whenever a management service will be detected fail by the self-identification. Self-activation evaluates if the management service needs a recovery, based on the criticality of the failure: if there are still enough instances for running the service, the recovery procedure is not started; otherwise, the self-configuration mechanism is triggered for repairing the service. (3) Self-configuration is activated if the failure of service is critical: the role of this mechanism is to instantiate the failed management service, and to return the service into a legal state.

The Formal Design

Figure 6 depicts the formal design of self-healing P2P-based approach. The model M0 abstracts the self-healing approach. The refinements M1, M2, M3 introduce step-bystep the self-detection, self-activation and self-configuration phases, respectively. The remaining refinements, from M4 to M20, are used for localisation of the system: each step of the algorithm is made local to a node. The last refinement M21 presents a local model that describes a set of procedures for recovering process of P2P system. Fig. 6: Architecture Abstracting the Self-Healing Approach (M0) This section presents an abstraction of the self-healing procedure for a failed service. Each service (s) is described by two states: RUN (legal/running state) and FAIL (illegal/faulty state). A variable serviceState is defined as s → st ∈ serviceState, where s denotes a service and st denotes a possible state. A property P expresses that a service (s) is in a legal running state that is formalised as P = (s → RUN ∈ serviceState). An event FAIL-URE models a faulty behaviour, where service (s) enters into a faulty state (FAIL), satisfying ¬P. The self-healing of management service (s) is expressed as (¬P) P. The recovery procedure is stated by an event HEAL ((¬P) HEAL ---→ P), where service (s) recovers from an illegal faulty state (FAIL) to a legal running state (RUN). The refinement diagram1 (see Fig. 7) and events sum up the abstraction of a recovery procedure.

= (s → RUN_1 ∈ serviceState_1) and ¬P = (s → FAIL_1 ∈ serviceState_1).
The intermediate steps of self-detection are introduced according to the refinement diagram (see Fig. 8) and proof tree.

Fig. 8: Self-Detection

(¬P) R 0 R 0 P trans (¬P) P
The event FAIL_DETECT is introduced to express the self-detection: the failure state (FAIL_1) of a service (s) is detected (state FL_DT _1).

The property (¬P) R 0 is expressed by the event FAIL_DETECT, where the failure (FAIL_1) of service (s) is identified (FL_DT _1). R 0 P is defined by the event HEAL, where the service (s) is restored to a legal running state (RUN_1) after failure detection. The same method is applied to identify all the phases of self-healing algorithm. Due to limited space, we focus on the interesting parts of models and liveness properties. The complete formal development of models can be downloaded from web 3 .

Introducing the Self-Activation (M2) and Self-Configuration (M3) The self-activation is introduced in this refinement M2 (see Fig. 9), where a failure of a service (s) is evaluated in terms of critical or non-critical using a new state FL_ACT _2 and an event FAIL_ACTIV. The self-configuration step is introduced in the next refinement M3 (see Fig. 10), which expresses that if the failure of service (s) is critical, then the self-configuration procedure for a service (s) will be triggered (state FL_CONF_3), otherwise, the failure will be ignored (state FL_IGN_3). The Global Behaviour (M4) The developed models are refined and decomposed into several steps (see Fig. 11) [START_REF] Marquezan | Self-* and P2P for Network Management -Design Principles and Case Studies[END_REF]. These steps are: (1) Self-Detection, (2) Self-Activation, and (3) Self-Configuration. Self-Detection phase is used to detect any failure in the autonomous system using two events FAIL_DETECT and IS_OK. The event FAIL_DETECT models the failure detection; and the event IS_OK states that if a detected failure of a service (s) is a false alarm, then the service (s) returns to a legal state (RUN_4).

Self-Activation process is used to evaluate when actual failures are identified, using the following events: FAIL_ACTIV, FAIL_IGN, IGNORE, and FAIL_CONF. The events FAIL_IGN and IGNORE are used to ignore the failure of service (s) when failure is not in critical state (FL_IGN_4). The event FAIL_CONF is used to evaluate the failure of service (s) when failure is critical (FL_CONF_4). The last phase Self-Configuration presents the healing procedure of a failed service using an event REDEPLOY.

From model M5 to M20, we localise the events (we switch from a service point of view to the instances/peers point of view) and detail the macro (global) steps by Fig. 11: Self-Healing steps adding new events, variables, and constraints. The refinements M5, M6, M7 introduce the running (run_peers(s)),faulty ( f ail_peers [{s}]), suspicious (susp_peers(s)) and deployed peers/instances (dep_inst[{s}]) for a service (s). A function (min_inst) associates each service (s) with the minimal number of instances that is required for running service (s), and helps to detail the self-activation phase: if the number of running instances of service (s) is below than minimum, then the failure is critical. The models M8, M9, M10 detail the self-detection and self-configuration phases to introduce the token owners for the services. Models from M11 to M20 localise gradually the events (to switch from a service point of view to the instances/peers point of view). The detailed formal development of various steps from M5 to M20 are given in the archive 3 . Due to limited space, in the following section, we present only the local model M21.

The Local Model (M21) This model details locally the self-healing procedure of a service (s). The peers instantiating management service (s) are introduced, as well as the notion of token owner. The token owner is a peer instance of service (s) that is marked as a token owner for the Management Peer Group (MPG). It can perform the self-healing procedure using self-detection, self-activation, and self-configuration steps.

(1) Self-Detection introduces an event SUSPECT_INST that states that the token owner for service (s) is able to suspect a set (susp) of unavailable peers instances of service (s). Other events RECONTACT_INST_OK and RECONTACT_INST_KO are used to specify the successful recontact, and failed recontact, respectively, of the unavailable instances for ensuring the failed states. Moreover, the token owner is able to monitor the status of service (s) using two events FAIL_DETECT, and IS_OK. If there are unavailable instances after the recontacting procedure, the token owner informs the safe members of MPG of failed instances using the event FAIL_DETECT, otherwise, the token owner indicates that service is running properly. (2) Self-Activation introduces an event FAIL_ACTIV that states that if there are failed instances of service (s), then the token owner evaluates if the failure is critical. Another event FAIL_IGNORE specifies that the failure is not critical. An event IGNORE can ignore the failure if several instances (more than minimum) are running correctly. If the number of instances for the running service (s) will be less than the minimum required services, then the failure will be declared critical, and the self-healing process will be triggered using an event FAIL_CONFIGURE. (3) Self-Configuration introduces three events REDEPLOY_INSTC, REDEPLOY_INSTS and REDEPLOY that specify that if the failure of service (s) is critical, then new instances of running service (s) can be deployed until to reach the minimal number of instances, and after the event HEAL can be triggered corresponding to the convergence of the self-healing process.

It is noticeable that the architectural decomposition of the self-healing process is emphasized in this model, by the events related to the algorithm. There is also a set of events describing actions related to the environment. MAKE_PEER_UNAVAIL: a set of peers (prs) becomes unavailable (can not be contacted); MAKE_PEER_AVAIL: a formerly unavailable instance (p) becomes available; UNFAIL_PEER: a failed instance re-enters a legal running state. This model M21 describes locally the Self-Healing P2P-Based Approach, where we have formulated hypotheses for ensuring the correct functioning of the self-healing process: (1) Event MAKE_PEER_AVAIL: If the token owner of a service (s) becomes unavailable,at least one peer, with the same characteristics as the disabled token owner (state, local informations about running, failed peers, etc.) can become the new token owner of service (s); (2) Event REDEPLOY_INSTC: There is always a sufficient number of available peers that can be deployed to reach the legal running state of a service (s).

In a nutshell, we say that our methodology allows users to understand the self-⋆ mechanisms and to gain insight into their architectures (components, coordination, etc.); and gives evidences of the correctness of self-⋆ systems under some assumptions/hypotheses.

Analysis of Temporal Properties for Event-B Models

Leuschel et al. [START_REF] Leuschel | ProB: A model checker for B[END_REF] developed a tool ProB for animating, model-checking, and verifying the consistency of Event-B models. ProB provides two ways for analysing Event-B models : constraint-based checking and temporal model-checking. We focus on temporal model-checking, since we are interested in liveness properties. Temporal model-checking [START_REF] Leuschel | ProB: A model checker for B[END_REF] allows ProB to detect problems with a model (invariants violation, deadlocks, etc.) and to verify if the model satisfies LTL properties: ProB explores the state space of the model and tries to find a counter-example (i.e. a sequence of events) leading to the violation of invariants or LTL properties.

A difference with TLC (model-checker for TLA + ) is that ProB does not support fairness [START_REF] Hansen | Translating B to TLA+ for validation with TLC: There and back again[END_REF], allowing unfair traces to be analysed during model-checking. Therefore, the TLA + framework is more suited to our work, since we are verifying liveness properties, in Event-B models, under fairness assumptions.

Discussion, Conclusion and Future Work

We present a methodology based on liveness properties and refinement diagrams for modelling the self-⋆ systems using EVENT B. We characterize the self-⋆ systems by three modes (abstract states): 1) legal (correct) state, 2) illegal (faulty) state, and 3) recovery state. We have proposed a generic pattern for deriving correct self-⋆ systems (see Fig. 1). The service-as-event and call-as-event paradigms provide a way to express the relationships between modes for ensuring required properties as convergence. The correct-by-construction principle gives us the possibility to refine procedures from events and to link modes. The key idea is to identify the modes (considered as abstract states) and the required abstract steps to allow the navigation between modes, and then to gradually enrich abstract models, using refinement to introduce the concrete states and events. We have illustrated our methodology by the self-healing approach [START_REF] Marquezan | Self-* and P2P for Network Management -Design Principles and Case Studies[END_REF].

The complexity of the development is measured by the number of proof obligations (PO) which are automatically/manually discharged (see Table 1). It should be noted that a large majority (∼ 70%) of the 1177 manual proofs is solved by simply running the provers. The actual summary of proof obligations is given by Table 2. The manually discharged POs (327) require analysis and skills: searching and adding premises, simplifying the complex predicates, and even transforming goals are needed to discharge these POs. Examples of difficult POs are related to proving the finiteness of Management Peer Groups (MPG), during the redeployment operation of the self-configuration phase. [START_REF] Méry | Automatic code generation from event-b models[END_REF]. Moreover, further case studies will help us to discover new patterns; these patterns will be added to a catalogue of patterns that could be implemented in the Rodin platform. Finally, another point would be to take into account dependability properties in our methodology.

A Appendix : EVENT-B models ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E (srv) = token_owner(srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd10: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ⇒ E (srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ failr_peers(srv) ∪ suspc_peers (token_owner(srv) ↦ srv)) not theorem ›if the owner of the token for a service becomes unavailable, and the service possess suspicious instances, then a new token owner among available and not suspicious peers is chosen grd11: dom(i_s) = E∼ ∧ dom(p_s) = dom(i_s) ∧ dom(s_i) = dom (i_s) ∧ dom(rc_s) = dom(i_s) ∧ dom(rt_s) = dom(i_s) not theorem › grd12: ∀ srv • srv ∈ SERVICES ⇒ ((E(srv) ↦ srv) ↦ i_state (token_owner(srv) ↦ srv) ∈ i_s ∧ (E(srv) ↦ srv) ↦ suspc_peers(token_owner(srv) ↦ srv) ∈ p_s) not theorem › grd13: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ ((E (srv) ↦ srv) ↦ suspc_inst(E(srv) ↦ srv) ∈ s_i) ∧ ((E(srv) ↦ srv) ↦ rctt_inst(E (srv) ↦ srv) ∈ rt_s) ∧ ((E(srv) ↦ srv) ↦ rect_inst(E(srv) ↦ srv) ∈ rc_s) not

C00 CONTEXT C00 › SETS SERVICES › STATES › CONSTANTS RUN › FAIL › InitState › AXIOMS axm1: SERVICES ≠ ∅ not theorem › axm2: STATES = {RUN, FAIL} not theorem › axm3: RUN ≠ FAIL not theorem › axm4: InitState ∈ SERVICES ↔ STATES not theorem › axm5: ∀ s • s ∈ SERVICES ⇒ s ↦ RUN ∈ InitState not theorem › axm6: ∀ s, st1, st2 • s ∈ SERVICES ∧ st1 ∈ STATES ∧ st2 ∈ STATES ∧ s ↦ st1 ∈ InitState ∧ s ↦ st2 ∈ InitState ⇒ st1 = st2 not theorem › END C01 CONTEXT C01 › EXTENDS C00 SETS STKTES_1 › CONSTKNTS RUN_1 › FKIL_1 › FKIL_DETECT_1 › InitState_1 › KXIOMS aam1T partition(STKTES_1, {RUN_1},{FKIL_1},{FKIL_DETECT_1}) not theorem › aam2T InitState_1 ∈ SERVICES ↔ STKTES_1 not theorem › aam3T ∀ s • s ∈ SERVICES ⇒ s ↦ RUN_1 ∈ InitState_1 not theorem › aam4T ∀ s, st1, st2 • s ∈ SERVICES ∧ st1 ∈ STKTES_1 ∧ st2 ∈ STKTES_1 ∧ s ↦ st1 ∈ InitState_1 ∧ s ↦ st2 ∈ InitState_1 ⇒ st1 = st2 not theorem › END C02 CONTEXT C02 › EXTENDS C0H SETS STATES_2 › CONSTANTS RUN_2 › FAIL_2 › FAIL_DETECT_2 › FAIL_ACTIV_2 › InitState_2 › AXIOMS axmH: partition(STATES_2, {RUN_2},{FAIL_2},{FAIL_DETECT_2}, {FAIL_ACTIV_2}) not theorem › axm2: InitState_2 ∈ SERVICES ↔ STATES_2 not theorem › axm3: ∀ s • s ∈ SERVICES ⇒ s ↦ RUN_2 ∈ InitState_2 not theorem › axm4: ∀ s, stH, st2 • s ∈ SERVICES ∨ stH ∈ STATES_2 ∨ st2 ∈ STATES_2 ∨ s ↦ stH ∈ InitState_2 ∨ s ↦ st2 ∈ InitState_2 ⇒ stH = st2 not theorem › END C03 CONTEXT C03 › EXTENDS C02 SETS STATES_3 › CONSTANTS RUN_3 › FAIL_3 › FAIL_DETECT_3 › FAIL_ACTIV_3 › FAIL_CONFIG_3 › FAIL_IGN_3 › InitState_3 › AXIOMS axm1: partition(STATES_3, {RUN_3},{FAIL_3},{FAIL_DETECT_3}, {FAIL_ACTIV_3},{FAIL_CONFIG_3},{FAIL_IGN_3}) not theorem › axm2: InitState_3 ∈ SERVICES ↔ STATES_3 not theorem › axm3: ∀ s • s ∈ SERVICES ⇒ s ↦ RUN_3 ∈ InitState_3 not theorem › axm4: ∀ s, st1, st2 • s ∈ SERVICES ∨ st1 ∈ STATES_3 ∨ st2 ∈ STATES_3 ∨ s ↦ st1 ∈ InitState_3 ∨ s ↦ st2 ∈ InitState_3 ⇒ st1 = st2 not theorem › END C04 CONTEXT C04 › EXTENDS C03 SETS STATES_4 › CONSTANTS RUN_4 › FAIL_4 › FAIL_DETECT_4 › FAIL_ACTIV_4 › FAIL_CONFIG_4 › FAIL_IGN_4 › DPL_4 › InitState_4 › AXIOMS axm1: partition(STATES_4, {RUN_4},{FAIL_4},{FAIL_DETECT_4}, {FAIL_ACTIV_4},{FAIL_CONFIG_4},{FAIL_IGN_4},{DPL_4}) not theorem › axm2: InitState_4 ∈ SERVICES ↔ STATES_4 not theorem › axm3: ∀ s • s ∈ SERVICES ⇒ s ↦ RUN_4 ∈ InitState_4 not theorem › axm4: ∀ s, st1, st2 • s ∈ SERVICES ∧ st1 ∈ STATES_4 ∧ st2 ∈ STATES_4 ∧ s ↦ st1 ∈ InitState_4 ∧ s ↦ st2 ∈ InitState_4 ⇒ st1 = st2 not theorem › END C05 CONTEXT C05 › EXTENDS C04 CONSTANTS min_inst › init_inst › AXIOMS axm1: min_inst ∈ SERVICES → ℕ1 not theorem › axm2: init_inst ∈ SERVICES → ℕ1 not theorem › axm3: ∀ s • s ∈ SERVICES ⇒ min_inst(s) ≥ 2 not theorem › axm4: ∀ s • s ∈ SERVICES ⇒ init_inst(s) ≥ min_inst(s) not theorem › axm5: ∀ s • s ∈ SERVICES ⇒ init_inst(s) ≥ 2 theorem › END C06 CONTEXT C06 › EXTENDS
: ∀ s1, s2 • s1 ⊆ VEERS ∧ s2 ⊆ VEERS ∧ s1 ≠ ∅ ∧ s2 ≠ ∅ ∧ finite(s1) ∧ finite(s2) ∧ s1 ⊂ s2 ⇒ carU(s1) ≤ carU(s2)-1 not theorem › axm5: ∀ s1 • s1 ⊆ VEERS ∧ s1 ≠ ∅ ∧ finite(s1) ⇒ carU(s1) > 0 theorem › axm6: ∀ s1, s2 • s1 ⊆ VEERS ∧ s2 ⊆ VEERS ∧ finite(s1) ∧ finite(s2) ∧ s1 ⊆ s2 ⇒ carU(s2) -carU(s1) = carU(s2∖s1) not theorem › END Vage 1 C07 CONTEXT C07 › EXTENDS C06 CONSTANTS deplo_inst › AXIOMS axm1: ∀ set, s1, s2 • set ⊆ SERVICES×PEERS ∧ s1 ∈ SERVICES ∧ s2 ∈ SERVICES ∧ s1 = s2 ⇒ ({s1} ⩤ set)[{s2}] = ∅ theorem › axm2: ∀ set, s1, s2 • set ⊆ SERVICES×PEERS ∧ s1 ∈ SERVICES ∧ s2 ∈ SERVICES ∧ s1 ≠ s2 ⇒ ({s1} ⩤ set)[{s2}] = set[{s2}] theorem › axm3: ∀ set, s1, s2, p • set ⊆ SERVICES×PEERS ∧ s1 ∈ SERVICES ∧ s2 ∈ SERVICES ∧ p ∈ PEERS ∧ s1 = s2 ⇒ (set = {s1 ↦ p})[{s2}] = set[{s2}]={p} theorem › axm4: ∀ set, s1, s2, p • set ⊆ SERVICES×PEERS ∧ s1 ∈ SERVICES ∧ s2 ∈ SERVICES ∧ p ∈ PEERS ∧ s1 ≠ s2 ⇒ (set = {s1 ↦ p})[{s2}] = set[{s2}]
¢ ∀ ¢ : SE RVI CES ∧ ¢ ∧ RUN_ G : ¢erviceState_ G ⇒ ¢ ∧ RUN_ 2 : ¢erviceSt ate_ 2 n↔t toe↔reh › mglinm_rln 2 : u ¢ ∀ ¢ : SE RVI CES ∧ ¢ ∧ RUN_ 2 : ¢erviceState_ 2 ⇒ ¢ ∧ RUN_G : ¢erviceSt ate_G n↔t toe↔reh › mglinm_⇒aigG1 u ¢ ∀ ¢ : SER VI CES ∧ ¢ ∧ FAIL_ G : ¢erviceState_ G ⇒ ¢ ∧ FAIL_ 2 : ¢erviceS tate_ 2 n↔t toe↔reh › mglinm_⇒aig 2 : u ¢ ∀ ¢ : SER VI CES ∧ ¢ ∧ FAIL_ 2 : ¢erviceState_ 2 ⇒ ¢ ∧ FAIL_G : ¢erviceS tate_G n↔t toe↔reh › mglinm_ftctG1 u ¢ ∀ ¢ : SER VI CES ∧ ¢ ∧ FAIL_ d E£EC£_G : ¢ervic eState_G ⇒ ¤¢ ∧ FAIL_A C£I V_ 2 : ¢erviceStat e_ 2 ¥ ¢ ∧ FAIL_d E £EC£_ 2 : ¢erviceS tate_ 2) n↔t toe↔reh › mglinm_ftct 2 : u ¢O ¢t ∀ ¢ : SERVI CES ∧ ¢t : S£A£ES_ 2 ∧ ¢t : GFAIL_A C£IV_ 2OFAI L_d E£EC£_ 2) ∧ ¢ ∧ ¢t : ¢erviceStat e_ 2 ⇒ ¢ ∧ FAIL_d E£EC£_G : ¢erviceState_G n↔t toe↔reh › mglinm_state1 u ¢O ¢t¡O ¢t2 ∀ ¢ : SERVI CES ∧ ¢t¡ : S£A£ES_ 2 ∧ ¢t2 : S£A£ES_ 2 ∧ ¢ ∧ ¢t ¡ : ¢erviceState_ 2 ∧ ¢ ∧ ¢t2 : ¢er viceState_ 2 ⇒ ¢t ¡ = ¢t2 n↔t toe↔reh › EV EN£S INITIALISATION: n↔t extenfef orfinar} › £HEN ¦ctG1 serviceState_2 ≔ InitState_ 2 › ENd FAIL1 n↔t extenfef orfinar} › REFINES FAIL ANx s › yH ERE mrfG1 s : SERVI CES n↔t toe↔reh › mrf 2 : ¢ ∧ RUN_ 2 : ¢ erviceState_ 2 n↔t toe↔reh › £HEN ¦ctG1 serviceState_2 ≔ ¤¢erviceState _ 2≔Gs ∧ RUN_ 2)) Y Gs ∧ FAIL_ 2) › ENd FAIL_DETECT1 n↔t extenfef orfinar} › REFINES Wame ¡ M02 FAIL_d E §EC § ANx s › yH ERE mrfG1 s : SERVI CES n↔t toe↔reh › mrf 2 : ¨ ∧ FAIL_ 2 : ¨erviceState_ 2 n↔t toe↔reh › §HEN ©ctG1 serviceState_2 ≔ ¨erviceState _ 2≔Gs ∧ FAIL_ 2)) Y Gs ∧ FAIL_d E §EC §_ 2) › ENd IS_O1 n↔t extenfef orfinar} › REFINES HEAL ANx s › yH ERE mrfG1 s : SERVI CES n↔t toe↔reh › mrf 2 : ¨ ∧ FAIL_d E §E C §_ 2 : ¨erviceSta te_ 2 n↔t toe↔reh › §HEN ©ctG1 serviceState_2 ≔ ¨erviceState _ 2 ≔ Gs ∧ FAIL_d E §EC §_ 2)) Y Gs ∧ RUN_ 2) › ENd FAIL_ACTIS1 n↔t extenfef orfinar} › ANx s › yH ERE mrfG1 s : SERVI CES n↔t toe↔reh › mrf 2 : ¨ ∧ FAIL_d E §E C §_ 2 : ¨erviceSta te_ 2 n↔t toe↔reh › §HEN ©ctG1 serviceState_2 ≔ ¨erviceState _ 2 ≔ Gs ∧ FAIL_d E §EC §_ 2)) Y Gs ∧ FAIL_A C §IV _ 2) › ENd GEAL1 n↔t extenfef orfinar} › REFINES HEAL ANx s › yH ERE mrfG1 s : SERVI CES n↔t toe↔reh › mrf 2 : ¨ ∧ FAIL_A C §I V_ 2 : ¨erviceStat e_ 2 n↔t toe↔reh › §HEN ©ctG1 serviceState_2 ≔ ¨erviceState _ 2 ≔ Gs ∧ FAIL_A C §IV_ 2)) Y Gs ∧ RUN_ 2) › ENd Wame 2 M02 ENd Wame ∖ M03 MACHINE M03 › REFINES M0G SEES C03 VA RIABL ES erviceState_ 3 › INVA RIANS inv1: serviceState_3 ∈ SERVI CES ↔ S AES_ 3 not theorem › gluing_run1: ∀ • ∈ SE RVI CES ∧ RN_ G ∈ erviceState_ G ⇒ RN_ 3 ∈ erviceSt ate_ 3 not theorem › gluing_runG: ∀ • ∈ SE RVI CES ∧ RN_ 3 ∈ erviceState_ 3 ⇒ RN_G ∈ erviceSt ate_G not theorem › gluing_fail1: ∀ • ∈ SER VI CES ∧ FAIL_ G ∈ erviceState_ G ⇒ FAIL_ 3 ∈ erviceS tate_ 3 not theorem › gluing_failG: ∀ • ∈ SER VI CES ∧ FAIL_ 3 ∈ erviceState_ 3 ⇒ FAIL_G ∈ erviceS tate_G not theorem › gluing_dtct1: ∀ • ∈ SER VI CES ∧ FAIL_ D EEC_G ∈ ervic eState_G ⇒ FAIL_D EEC _ 3 ∈ erviceStat e_ 3 not theorem › gluing_dtctG: ∀ • ∈ SER VI CES ∧ FAIL_ D EEC_ 3 ∈ ervic eState_ 3 ⇒ FAIL_D EEC _G ∈ erviceStat e_G not theorem › gluing_act1: ∀ • ∈ SE RVI CES ∧ FAIL _A CIV_G ∈ ervic eState_G ⇒ FAIL_A CI V_ 3 ∈ erviceStat e_ 3 FAIL_ CO NFIG_ 3 ∈ erviceS tate_ 3 FAIL_IGN_ 3 ∈ erv iceState_ 3) not theorem › gluing_actG: ∀ , t • ∈ SERVI CES ∧ t ∈ SAES_ 3 ∧ t ∈ {FAIL_A CIV_ 3,FAI L_ CONFIG_ 3,FAIL_I GN_ 3} ∧ t ∈ erviceState_ 3 ⇒ FAIL_A CIV_G ∈ e rviceState_G not theorem › gluing_state: ∀ , t1, tG • ∈ SERVI CES ∧ t1 ∈ SAES_ 3 ∧ tG ∈ SAES_ 3 ∧ t 1 ∈ erviceState_
! FAIL_ 3 ∈ "erviceState_ 3 not theorem › HEN #ct1: serviceState_3 ≔ $"erviceState _ 3∖{s ! FAIL_ 3}) ∪ {s ! FAIL_D E EC _ 3} › END IS_O%: not extended ordinary › REFINES IS_OK ANY s › WH ERE grd1: s ∈ SERVI CES not theorem › grdG: s ! FAIL_D E E C _ 3 ∈ "erviceSta te_ 3 not theorem › HEN #ct1: serviceState_3 ≔ $"erviceState _ 3 ∖ {s ! FAIL_D E EC _ 3}) ∪ {s ! R&N_ 3} › END FAIL_ACTIS: not extended ordinary › REFINES FAIL_A C IV ANY s › WH ERE grd1: s ∈ SERVI CES not theorem › grdG: s ! FAIL_D E E C _ 3 ∈ "erviceSta te_ 3 not theorem › HEN #ct1: serviceState_3 ≔ $"erviceState _ 3 ∖ {s ! FAIL_D E EC _ 3}) ∪ {s ! FAIL_A C IV _ 3}
: ∀ Y • Y ∈ SE R VICES ∧ s ↦ RUN_3 ∈ YHrvicHStatH_ 3 ⇒ Y ↦ RUN_4 ∈ YHrvicHSt atH_4 not thHorHm › gluing_run2: ∀ Y • Y ∈ SE R VICES ∧ s ↦ RUN_4 ∈ YHrvicHStatH_ 4 ⇒ Y ↦ RUN_3 ∈ YHrvicHSt atH_3 not thHorHm › gluing_fail1: ∀ Y • Y ∈ SERVICES ∧ s ↦ FAIL_3 ∈ YHrvicHStatH_ 3 ⇒ Y FAIL_4 ∈ YHrvicHS tatH_4 not thHorHm › gluing_fail2: ∀ Y • Y ∈ SERVICES ∧ s ↦ FAIL_4 ∈ YHrvicHStatH_ 4 ⇒ Y FAIL_3 ∈ YHrvicHS tatH_3 not thHorHm › gluing_dtct1: ∀ Y • Y ∈ SERVICES ∧ s ↦ FAIL_DETE C'_3 ∈ YHrvic HStatH_3 ⇒ Y ↦ FAIL_DETE C '_4 ∈ YHrvicHStat H_4 not thHorHm › gluing_dtct2: ∀ Y • Y ∈ SERVICES ∧ s ↦ FAIL_DETE C'_4 ∈ YHrvic HStatH_4 ⇒ Y ↦ FAIL_DETE C '_3 ∈ YHrvicHStat H_3 not thHorHm › gluing_act1: ∀ Y • Y ∈ SE R VICES ∧ s ↦ FAIL_ACTIV_3 ∈ YHrvic HStatH_3 ⇒ Y ↦ FAIL_A C'IV _4 ∈ YHrvicHStatH _4 not thHorHm › gluing_act2: ∀ Y • Y ∈ SE R VICES ∧ s ↦ FAIL_ACTIV_4 ∈ YHrvic HStatH_4 ⇒ Y ↦ FAIL_A C'IV _3 ∈ YHrvicHStatH _3 not thHorHm › gluing_ign1: ∀ Y • Y ∈ SE R VICES ∧ s ↦ FAIL_IGN_3 ∈ YHrvicHS tatH_3 ⇒ Y ↦ FAIL_IGN_4 ∈ YHrvicHStatH_4 not thHorHm › gluing_ign2: ∀ Y • Y ∈ SE R VICES ∧ s ↦ FAIL_IGN_4 ∈ YHrvicHS tatH_4 ⇒ Y ↦ FAIL_IGN_3 ∈ YHrvicHStatH_3 not thHorHm › gluing_conf1: ∀ Y • Y ∈ SERVICES ∧ s ↦ FAIL_CONFIG_3 ∈ YHrvic HStatH_3 ⇒ (Y ↦ FAIL_ CONF IG_4 ∈ YHrvicHSta tH_4 ∨ Y ↦ DPL_4 ∈ YHrvicHStatH _4) not thHorHm › gluing_conf2: ∀ Y, Yt • Y ∈ SER VICES ∧ st ∈ STATES_4 ∧ Yt ∈ {FAIL_ CONFIG_4,DP L_4} ∧ Y ↦ Yt ∈ Y HrvicHStatH_4 ⇒ Y ↦ FAIL _ CONFIG_3 ∈ YHrvicHStatH_3 not thHorHm › gluing_YtatH: ∀ Y, Yt1, Yt2 • Y ∈ SER VICES ∧ st1 ∈ STATES_4 ∧ Yt2 ∈ STATES_4 ∧ Y ↦ Yt 1 ∈ YHrvicHStatH_ 4 ∧ Y ↦ Yt2 ∈ YHr vicHStatH_4 ⇒ Yt 1 =
≔ fail_peers∖{s ↦ p} › END END M07 MACHINE M07 › REFINES M06 SEES C07 VARIABLES serviceState_4 › run_peers › susp_peers › fail_peers › dep_inst › INVARIANTS inv1: dep_inst ∈ SERVICES ↔ PEERS not theorem › inv2: ∀ s • s ∈ SERVICES ⇒ dep_inst[{s}] ∩ fail_peers[{s}] = ∅ not theorem › inv3: ∀ s, st • s ∈ SERVICES ∧ st ∈ STATES_4 ∧ s ↦ st ∈ serviceState_4 ∧ st ≠ FAIL_CONFIG_4 ⇒ dep_inst[{s}] = ∅ not theorem › inv4: ∀ s • s ∈ SERVICES ⇒ finite(dep_inst[{s}]) not theorem › inv5: ∀ s • s ∈ SERVICES ⇒ dep_inst[{s}] ∩ run_peers(s) = ∅
inv3: ∀ s • s ∈ SERVICES ⇒ token_owner(s) ∈ run_peers(s)∖unav_peers not theorem › inv4: ∀ s • s ∈ SERVICES ∧ s ∈ dom(susp_peers) ⇒ token_owner(s) ∉ susp_peers(s) not theorem › inv5: susp_inst ∈ PEERS ↔ (SERVICES×PEERS) not theorem › inv6: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(susp_inst[{ld}]) ⇒ ld = token_owner(s) not theorem › inv7: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(susp_inst[{ld}]) ∧ ld = token_owner(s) ⇒ ld ∉ susp_inst[{ld}][{s}] not theorem › inv8: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(susp_inst[{ld}]) ∧ ld = token_owner(s) ⇒ susp_inst[{ld}][{s}] ⊂ run_peers(s) not theorem › inv9: ∀ ld, s, stt • ld ∈ PEERS ∧ s ∈ SERVICES ∧ stt ∈ STATES_4 ∧ s ↦ stt ∈ serviceState_4 ∧ ld = token_owner(s) ∧ stt ≠ RUN_4 ⇒ susp_inst[{ld}][{s}] = ∅ not
∈ PEERS ↔ (SERVICES×PEERS) not theorem › inv2: rct_inst ∈ PEERS ↔ (SERVICES×PEERS) not theorem › inv3: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ rct_inst[{ld}][{s}] ≠ ∅ ⇒ rec_inst[{ld}][{s}] ≠ ∅ not theorem › inv4: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ rct_inst[{ld}][{s}] ≠ ∅ ⇒ rct_inst[{ld}][{s}] ⊆ rec_inst[{ld}][{s}] not theorem › inv5: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(rec_inst[{ld}]) ⇒ ld = token_owner(s) not theorem › inv6: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(rec_inst[{ld}]) ∧ ld = token_owner(s) ⇒ ld ∉ rec_inst[{ld}][{s}] not theorem › inv7: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(rct_inst[{ld}]) ⇒ ld = token_owner(s) not theorem › inv8: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(rct_inst[{ld}]) ∧ ld = token_owner(s) ⇒ ld ∉ rct_inst[{ld}][{s}] not theorem › inv9: dom(rct_inst) ⊆ dom(rec_inst) not theorem › inv10: ∀ ld • ld ∈ PEERS ∧ ld ∈ dom(rct_inst) ⇒ rct_inst[{ld}] ⊆ rec_inst[{ld}] theorem › inv11: ∀ s • s ∈ SERVICES ∧ s ∈ dom(
inv2: ∀ s, i • s ∈ SERVICES ∧ i ∈ PEERS ⇒ finite(actv_inst[{i}][{s}]) not theorem › inv3: ∀ ld, s • ld ∈ PEERS ∧ s ∈ SERVICES ∧ s ∈ dom(actv_inst[{ld}]) ⇒ ld = token_owner(s) not theorem › inv4: ∀ s, i • s ∈ SERVICES ∧ i ∈ PEERS ⇒ actv_inst[{i}][{s}] ∩ run_peers(s) = ∅ not theorem › inv5: ∀ s, i • s ∈ SERVICES ∧ i ∈ PEERS ⇒ actv_inst[{i}][{s}] ∩ dep_inst[{s}] = ∅ not theorem › inv6: ∀ s, i • s ∈ SERVICES ∧ i ∈ PEERS ⇒ actv_inst[{i}][{s}] ∩ fail_peers[{s}] = ∅ not theorem › inv7: ∀ ld, s, stt • ld ∈ PEERS ∧ s ∈ SERVICES ∧ stt ∈ STATES_4 ∧ s ↦ stt ∈ serviceState_4 ∧ ld = token_owner(s) ∧ stt ≠ FAIL_CONFIG_4 ⇒ actv_inst [{ld}][{s}] = ∅ not
M14 grd13: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ ((E (srv) ↦ srv) ↦ suspc_inst(E(srv) ↦ srv) ∈ s_i) ∧ ((E(srv) ↦ srv) ↦ rctt_inst(E (srv) ↦ srv) ∈ rt_s) ∧ ((E(srv) ↦ srv) ↦ rect_inst(E(srv) ↦ srv) ∈ rc_s) not theorem › grd14: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ⇒ ((E (srv) ↦ srv) ↦ ∅ ∈ s_i) ∧ ((E(srv) ↦ srv) ↦ ∅ ∈ rt_s) ∧ ((E(srv) ↦ srv) ↦ ∅ ∈ rc_s) not
∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd9: ac_i ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd10: dom(p_s) = E∼ ∧ dom(s_i) = E∼ ∧ dom(rc_s) = E∼ ∧ dom (rt_s) = E∼ ∧ dom(ac_i) = E∼ not theorem › grd11: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E(srv) = token_owner(srv) ∧ s_i(E(srv) ↦ srv) = suspc_inst(E(srv) ↦ srv) ∧ rt_s(E(srv) ↦ srv) = rctt_inst(E(srv) ↦ srv) ∧ rc_s(E(srv) ↦ srv) = rect_inst(E(srv) ↦ srv) ∧
ac_i(E(srv) ↦ srv) = actv_instc(E(srv) ↦ srv) not theorem ›If the token owner of a service srv does not belong to prs, the token M1R ac_i(E(srv) ↦ srv) = actv_instc(E(srv) ↦ srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd12: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ failr_peers (srv) ∪ suspc_peers(token_owner(srv suspct_peers(E(srv) ↦ srv) = suspct_peers(token_owner (srv) ↦ srv) not theorem ›if the owner of the token for a service becomes unavailable, A new token owner is chosen: the new token owner must have same characteristics as the previous one (state, list of suspicious neighbours, etc.), and it must not be an unavailable, suspicious, failed peer or a member of prs WITH p_s: p_s = E∼ ◁ suspct_peers › rc_s: rc_s = ((prs×SERVICES) ⩤ rect_inst)  (((E∖token_owner) ∼)×{∅}) › s_i: s_i = ((prs×SERVICES) ⩤ suspc_inst)  (((E∖token_owner) ∼)×{∅}) › rt_s: rt_s = ((prs×SERVICES) ⩤ rctt_inst)  (((E∖token_owner) ∼)×{∅}) › ac_i: ac_i = ((prs×SERVICES) ⩤ actv_instc)  (((E∖token_owner) ∼)×{∅}) › THEN act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new values for token owner per service act3: rect_inst ≔ ((prs×SERVICES) ⩤ rect_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore (1) M17 act3:

) ↦ srv)) ∧ E(srv) ↦ srv ∈ dom(inst_state) ∧ inst_state(E(srv) ↦ srv) = inst_state(token_owner(srv) ↦ srv) ∧ s_i(E(srv) ↦ srv) = ∅ ∧ rt_s(E(srv) ↦ srv) = ∅ ∧ rc_s(E(srv) ↦ srv) = ∅ ∧ ac_i(E(srv) ↦ srv) = ∅ not
rect_inst ≔ ((prs×SERVICES) ⩤ rect_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act4: rctt_inst ≔ ((prs×SERVICES) ⩤ rctt_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] act5: actv_instc ≔ ((prs×SERVICES) ⩤ actv_instc)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not activate instances anymore act6: suspct_peers ≔ (prs×SERVICES) suspct_peers ›the peers in prs can not suspect instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act7: suspc_inst ≔ ((prs×SERVICES) ⩤ suspc_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not suspect instances anymore ( 2 suspct_peers(E(srv) ↦ srv) = suspct_peers(token_owner (srv) ↦ srv) not theorem ›if the owner of the token for a service becomes unavailable, A new token owner is chosen: the new token owner must have same characteristics as the previous one (state, list of suspicious neighbours, etc.), and it must not be an unavailable, suspicious, failed peer or a member of prs THEN act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new values for token owner per service act3: rect_inst ≔ ((prs×SERVICES) ⩤ rect_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act4: rctt_inst ≔ ((prs×SERVICES) ⩤ rctt_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] act5: actv_instc ≔ ((prs×SERVICES) ⩤ actv_instc)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not activate instances anymore act6: suspct_peers ≔ (prs×SERVICES) ⩤ suspct_peers ›the peers in prs can not suspect instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act7: suspc_inst ≔ ((prs×SERVICES) ⩤ suspc_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not suspect instances anymore ( dep_instcs(E(srv) ↦ srv) = dep_instcs(token_owner(srv) ↦ srv) not theorem ›if the owner of the token for a service becomes unavailable, A new token owner is chosen: the new token owner must have same characteristics as the previous one (state, list of suspicious neighbours, etc.), and it must not be an unavailable, suspicious, failed peer or a member of prs THEN act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new values for token owner per service act3: rect_inst ≔ ((prs×SERVICES) ⩤ rect_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act4: rctt_inst ≔ ((prs×SERVICES) ⩤ rctt_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] act5: actv_instc ≔ ((prs×SERVICES) ⩤ actv_instc)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not activate instances anymore M20 act5: actv_instc ≔ ((prs×SERVICES) ⩤ actv_instc)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not activate instances anymore act6: suspct_peers ≔ (prs×SERVICES) ⩤ suspct_peers ›the peers in prs can not suspect instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act7: suspc_inst ≔ ((prs×SERVICES) ⩤ suspc_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not suspect instances anymore ( 2 dep_instcs(E(srv) ↦ srv) = dep_instcs(token_owner(srv) ↦ srv) not theorem ›if the owner of the token for a service becomes unavailable, A new token owner is chosen: the new token owner must have same characteristics as the previous one (state, list of suspicious neighbours, etc.), and it must not be an unavailable, suspicious, failed peer or a member of prs THEN act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new values for token owner per service act3: rect_inst ≔ ((prs×SERVICES) ⩤ rect_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act4: rctt_inst ≔ ((prs×SERVICES) ⩤ rctt_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not try to recontact instances anymore [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] act5: actv_instc ≔ ((prs×SERVICES) ⩤ actv_instc)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not activate instances anymore act6: suspct_peers ≔ (prs×SERVICES) ⩤ suspct_peers ›the peers in prs can not suspect instances anymore [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] act7: suspc_inst ≔ ((prs×SERVICES) ⩤ suspc_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not suspect instances anymore (2) M21 act7:

suspc_inst ≔ ((prs×SERVICES) ⩤ suspc_inst)  (((E∖token_owner)∼)×{∅}) ›the peers in prs can not suspect instances anymore [START_REF] Andriamiarina | Formal Verification of Fault Tolerant NoC-based Architecture[END_REF] act8

Fig. 1 :

 1 Fig. 1: Diagram for a Self-Stabilizing System S

Fig. 3 :

 3 Fig. 3: A Refinement Diagram

4. 1

 1 Introduction to the Self-Healing P2P-Based Approach

Fig. 9 :

 9 Fig. 9: Self-Activation Fig. 10: Self-Configuration

Table 1 :

 1 Summary of Proof Obligations

Total Auto Quasi-Auto Manual 1434 257 17.9% 850 59.3% 327 22.8%

Table 2

 2

	: Synthesis of POs
	Furthermore, our refinement-based formal-
	ization allows us to produce final local
	models close to the source code. Our fu-
	ture works include the development of tech-
	niques for generating applications from
	the resulting model extending tools like
	EB2ALL

  3 ∧ tG ∈ er viceState_ 3 ⇒ t

			M03
		END
		FAIL_DETECT: REFINES FAIL_D E EC ANY s › WH ERE grd1: ∈ SERVI CES not extended s grdG: s	ordinary › not theorem	›
	theorem › EV ENS INITIALISATION: HEN ct1: serviceState_3 ≔ InitState_ 3 › not extended ordinary › END	1 tG not
	FAIL_ 3}	FAIL: REFINES not extended FAIL ANY s › WH ERE grd1: s ∈ SERVI CES ordinary › not theorem grdG: s RN_ 3 ∈ erviceState_ 3 › HEN ct1: serviceState_3 ≔ erviceState not theorem 3∖{s RN_ 3}) ∪ › _ ›	{s

  = token_owner(srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd5: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ srv ∉ dom(susp_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers [{srv}]) not theorem ›if the owner of the token for a service becomes unavailable and the service is not suspicious, then a new token owner among available peers is chosen grd6: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ srv ∈ dom(susp_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ susp_peers(srv) ∪ fail_peers[{srv}]) not theorem ›if the owner of the token for a service becomes unavailable, and the service possess suspicious instances, then a new token owner among available and not

				M08 M08 M08 M08 M08 M09
	MACHINE	E THEN grd2: ›new values for token owner per service if needed s ↦ FAIL_DETECT_4 ∈ serviceState_4 not theorem › act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_ACTIV_4}) ∪ THEN
	WHERE act1: grd5: {s ↦ FAIL_IGN_4} › act1: M09 ›	susp_inst ≔ susp_inst ∪ ({token_owner(s)} × ({s}×susp)) susp_peers(s) = ∅ not theorem › serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_CONFIG_4})
	grd1: ›the members of susp become suspected instances for s by the token owner of s prs ⊆ PEERS not theorem › THEN END ∪ {s ↦ DPL_4} › REFINES
	grd2: grd3: owner per service if needed prs ⊈ unav_peers not theorem › E ∈ SERVICES → PEERS not theorem ›new value for token grd4: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E END not extended ordinary › act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_DETECT_4}) ∪ {s ↦ RUN_4} › END act2: run_peers(s) ≔ run_peers(s) ∪ dep_inst[{s}] › M08 IGNORE: extended ordinary › REFINES act3: dep_inst ≔ {s} ⩤ dep_inst › END SEES C08 FAIL: REFINES FAIL ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ RUN_4 ∈ serviceState_4 not theorem › grd3: susp_inst[{token_owner(s)}][{s}] ≠ ∅ not theorem › WITH fp: fp=susp_inst[{token_owner(s)}][{s}] › act2: susp_peers(s) ≔ susp_inst[{token_owner(s)}][{s}] › act3: susp_inst ≔ susp_inst ⩥ ({s} ◁ ran(susp_inst)) › END FAIL_DETECT: extended ordinary › REFINES FAIL_DETECT FAIL_ACTIV: extended ordinary › REFINES FAIL_ACTIV ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_DETECT_4 ∈ serviceState_4 not theorem › grd5: susp_peers(s) ≠ ∅ not theorem › act2: run_peers(s) ≔ run_peers(s) ∖ susp_peers(s) › act3: susp_peers(s) ≔ ∅ › act4: fail_peers ≔ fail_peers ∪ ({s}×susp_peers(s)) › END FAIL_CONFIGURE: extended ordinary › REFINES IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_IGN_4 ∈ serviceState_4 not theorem › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_IGN_4}) ∪ {s ↦ RUN_4} › END REDEPLOY_INST ANY s › dep › WHERE grd1: s ∈ SERVICES not theorem › grd2: dep ⊆ PEERS not theorem › VARIABLES HEAL: extended ordinary › REFINES HEAL ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ DPL_4 ∈ serviceState_4 not theorem › THEN UNFAIL_PEER: extended ordinary › REFINES UNFAIL_PEER ANY s › p › serviceState_4 › run_peers › susp_peers › fail_peers › dep_inst › token_owner › unav_peers › susp_inst › rec_inst ›instances that are tried to be recontacted (srv) suspicious peers is chosen THEN act1: serviceState_4 ≔ (serviceState_4∖{s ↦ RUN_4}) ∪ {s ↦ FAIL_4} › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_DETECT_4}) ∪ {s ↦ FAIL_ACTIV_4} › act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ DPL_4}) ∪ {s ↦ RUN_4} › rct_inst ›instances effectively recontacted after a try INVARIANTS REDEPLOY_INST: extended ordinary › REFINES END inv1: rec_inst
		THEN ANY grd3: FAIL_CONFIGURE finite(dep) not theorem › WHERE
		ANY	act1: s › grd4: grd1:	unav_peers ≔ unav_peers ∪ prs ›the peers in prs become dep ∩ run_peers(s) = ∅ not theorem › s ∈ SERVICES not theorem ›
	unavailable		sf s grd5: › › grd2:	dep ∩ fail_peers[{s}] = ∅ not theorem › p ∈ PEERS not theorem ›
		act2: WHERE WHERE grd6: grd3:	token_owner ≔ token_owner  E ›new value for token owner card(dep) = deplo_inst(s) not theorem › s ↦ p ∈ fail_peers not theorem ›
	per service is given if needed grd1: s ∈ SERVICES not theorem › grd1: s ∈ SERVICES not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) THEN
	theorem › act3: grd2: grd2: not theorem › act1:	susp_inst ≔ prs ⩤ susp_inst ›the peers in prs can not s ↦ FAIL_4 ∈ serviceState_4 not theorem › s ↦ FAIL_ACTIV_4 ∈ serviceState_4 not theorem › fail_peers ≔ fail_peers∖{s ↦ p} ›
	EVENTS suspect instances anymore grd5: susp_peers(s) ≠ ∅ not theorem › grd3: card(run_peers(s)) < min_inst(s) not theorem › grd8: s ↦ FAIL_CONFIG_4 ∈ serviceState_4 not theorem › END INITIALISATION: extended ordinary › THEN act1: serviceState_4 ≔ InitState_4 › act2: run_peers ≔ InitSrvcPeers › act3: susp_peers ≔ ∅ › act4: fail_peers ≔ ∅ › act5: dep_inst ≔ ∅ › END grd6: sf ⊆ PEERS not theorem › grd7: sf ⊆ susp_peers(s) not theorem › THEN THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_ACTIV_4}) ∪ {s ↦ FAIL_CONFIG_4} › THEN act1: dep_inst ≔ dep_inst ∪ ({s}×dep) › END MAKE_PEER_AVAIL: not extended ordinary › ANY SUSPECT_INST: not extended ordinary › ANY s ›a service s susp ›suspicious instances WHERE act1: serviceState_4 ≔ (serviceState_4∖{s ↦ FAIL_4}) ∪ {s ↦ FAIL_DETECT_4} › act2: susp_peers(s) ≔ susp_peers(s) ∖ sf › END END extended ordinary › p › REDEPLOY: extended ordinary › REFINES WHERE grd1: p ∈ PEERS not theorem › FAIL_IGNORE: REFINES REDEPLOY grd2: p ∈ unav_peers not theorem ›
	act6: act7: act8: grd1: grd2: grd3: FAIL_IGNORE token_owner ≔ init_tok › unav_peers ≔ ∅ › susp_inst ≔ ∅ › s ∈ SERVICES not theorem › susp ⊆ PEERS not theorem › susp = run_peers(s) ∩ unav_peers not theorem ›instances s › THEN ANY ANY act1: unav_peers ≔ unav_peers ∖ {p} › IS_OK: extended ordinary › REFINES s › WHERE END
	END in susp are suspicious if the peers running them becomes unavailable IS_OK WHERE grd1: s ∈ SERVICES not theorem ›
	not extended ordinary › member of susp have not yet been suspected for s by the token owner of s ANY grd5: s ↦ RUN_4 ∈ serviceState_4 not theorem ›the state of s s › WHERE grd2: s ↦ FAIL_ACTIV_4 ∈ serviceState_4 not theorem › grd3: card(run_peers(s)) ≥ min_inst(s) not theorem › grd6: dep_inst[{s}] ≠ ∅ not theorem › grd4: card(run_peers(s))+card(dep_inst[{s}]) ≥ min_inst(s) not MAKE_PEER_UNAVAIL: grd4: s ∉ dom(susp_inst[{token_owner(s)}]) not theorem ›the ANY grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_CONFIG_4 ∈ serviceState_4 not theorem › END
	is OK theorem ›	prs › grd1: THEN	s ∈ SERVICES not theorem ›

  fail_peers[{srv}]) not theorem ›if the owner of the token for a service becomes unavailable and the service is not suspicious, then a new token owner among available peers is chosen grd7: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ token_owner(srv) ↦ srv ∈ dom(suspc_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers[{srv}] ∪ suspc_peers(token_owner(srv) ↦ srv)) not theorem ›if the owner of the token for a service becomes unavailable, and the service possess suspicious instances, then a new token owner among available and not

	grd7:	M10 M10 M10 M10 M10 M10 M10 M11 M11 M11 M11 M11 M11 M11 M11 M12 M12 M12 M12 M12 M12 M12 M12 M13 M13 M13 M13 M13 rec_inst[{token_owner(s)}][{s}] ⊂ suspc_peers M13 M13 M13 M13 M14 M14
	END MAKE_PEER_UNAVAIL: REFINES ANY s ›a service s extended ordinary › susp ›suspicious instances WHERE grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the token owner of s has not yet tried to recontact i grd7: rec_inst[{token_owner(s)}][{s}] ⊂ susp_peers(s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious THEN act1: serviceState_4 ≔ (serviceState_4∖{s ↦ FAIL_4}) ∪ {s ↦ FAIL_DETECT_4} › act2: susp_peers(s) ≔ susp_peers(s) ∖ rct_inst[{token_owner grd3: card(run_peers(s)) < min_inst(s) not theorem › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_ACTIV_4}) ∪ {s ↦ FAIL_CONFIG_4} › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › THEN act1: actv_inst ≔ actv_inst ∪ {token_owner(s) ↦ (s ↦ i)} › END s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ DPL_4 ∈ serviceState_4 not theorem › MACHINE M11 › REFINES M10 prs › E ›new values for token owner per service if needed i_s › WHERE SUSPECT_INST: not extended ordinary › REFINES SUSPECT_INST ANY grd5: i ∈ susp_peers(s)∖unav_peers not theorem ›i is a suspicious instance of s and is available (can be contacted) grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the token owner of s has not yet tried to recontact i grd8: rec_inst[{token_owner(s)}][{s}] = susp_peers(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_DETECT_4 › grd2: i_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd3: card(run_peers(s)) < min_inst(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_CONFIG_4 › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › THEN act1: actv_inst ≔ actv_inst ∪ {token_owner(s) ↦ (s ↦ i)} › s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = DPL_4 not theorem › MACHINE M12 › REFINES M11 i_s › p_s › WHERE grd1: prs ⊆ PEERS not theorem › act6: actv_inst ≔ prs ⩤ actv_inst › act7: i_state ≔ i_s › act8: suspc_peers ≔ p_s › END grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS FAIL_DETECT ANY s › WHERE END extended ordinary › grd2: i ∈ PEERS not theorem › grd3: i ∉ run_peers(s) ∪ fail_peers[{s}] ∪ unav_peers ∪ dep_inst[{s}] not theorem ›i does not run s, is not failed for s, is not act1: i_state(token_owner(s) ↦ s) ≔ DPL_4 › act2: run_peers(s) ≔ run_peers(s) ∪ dep_inst[{s}] › act3: dep_inst ≔ {s} ⩤ dep_inst › MACHINE M13 › REFINES i_s › p_s › s_i › act2: token_owner ≔ token_owner  E ›new value for token owner per service is given if needed act3: rec_inst ≔ prs ⩤ rec_inst ›the peers in prs can not try RECONTACT_INST_OK: extended ordinary › REFINES (token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the grd5: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_ACTIV_4 › extended ordinary › grd1: s ∈ SERVICES not theorem › act1: unav_peers ≔ unav_peers ∖ {p} › MACHINE act8: suspc_inst ≔ InitSuspPeers › REDEPLOY_INSTC: REFINES REDEPLOY_INSTC grd2: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › END M14 › REFINES act10: rect_inst ≔ InitSuspPeers › act11: rctt_inst ≔ InitSuspPeers › FAIL_CONFIGURE: REFINES unavailable and is not already activated for s END M12 WHERE to recontact instances anymore RECONTACT_INST_OK token owner of s has tried to recontact i act2: run_peers(s) ≔ run_peers(s) ∖ suspc_peers(token_owner(s) ANY grd7: actv_inst[{token_owner(s)}][{s}]=∅ not theorem › END M13 act12: actv_inst ≔ ∅ ›
	theorem › finite(actv_inst) not theorem › INITIALISATION: inv8: EVENTS extended ordinary › THEN act1: serviceState_4 ≔ InitState_4 › act2: run_peers ≔ InitSrvcPeers › act3: susp_peers ≔ ∅ › act4: fail_peers ≔ ∅ › act5: dep_inst ≔ ∅ › act6: token_owner ≔ init_tok › act7: unav_peers ≔ ∅ › act8: susp_inst ≔ ∅ › act10: rec_inst ≔ ∅ › act11: rct_inst ≔ ∅ › act12: actv_inst ≔ ∅ › MAKE_PEER_UNAVAIL ANY prs › E ›new values for token owner per service if needed WHERE grd1: prs ⊆ PEERS not theorem › grd2: prs ⊈ unav_peers not theorem › grd3: E ∈ SERVICES → PEERS not theorem ›new value for token owner per service if needed grd4: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E (srv) = token_owner(srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd5: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ srv ∉ dom(susp_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers [{srv}]) not theorem ›if the owner of the token for a service becomes unavailable and the service is not suspicious, then a new token owner among available peers is chosen grd6: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ srv ∈ dom(susp_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ susp_peers(srv) ∪ fail_peers[{srv}]) not theorem ›if the owner of the token for a service becomes unavailable, and the service possess suspicious instances, then a new token owner among available and not suspicious peers is chosen THEN act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new value for token owner per service is given if needed act3: susp_inst ≔ prs ⩤ susp_inst ›the peers in prs can not suspect instances anymore act4: rec_inst ≔ prs ⩤ rec_inst › act5: rct_inst ≔ prs ⩤ rct_inst › act6: actv_inst ≔ prs ⩤ actv_inst › END grd1: s ∈ SERVICES not theorem › grd2: susp ⊆ PEERS not theorem › grd3: susp = run_peers(s) ∩ unav_peers not theorem ›instances in susp are suspicious if the peers running them becomes unavailable grd4: s ∉ dom(susp_inst[{token_owner(s)}]) not theorem ›the member of susp have not yet been suspected for s by the token owner of s grd5: s ↦ RUN_4 ∈ serviceState_4 not theorem ›the state of s is OK THEN act1: susp_inst ≔ susp_inst ∪ ({token_owner(s)} × ({s}×susp)) ›the members of susp become suspected instances for s by the token owner of s END FAIL: extended ordinary › REFINES FAIL ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ RUN_4 ∈ serviceState_4 not theorem › grd3: susp_inst[{token_owner(s)}][{s}] ≠ ∅ not theorem › THEN act1: serviceState_4 ≔ (serviceState_4∖{s ↦ RUN_4}) ∪ {s ↦ FAIL_4} › act2: susp_peers(s) ≔ susp_inst[{token_owner(s)}][{s}] › act3: susp_inst ≔ susp_inst ⩥ ({s} ◁ ran(susp_inst)) › END RECONTACT_INST_OK: extended ordinary › REFINES RECONTACT_INST_OK ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: s ↦ FAIL_4 ∈ serviceState_4 not theorem ›the state of s is SUSPICIOUS grd4: susp_peers(s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ susp_peers(s)∖unav_peers not theorem ›i is a suspicious instance of s and is available (can be contacted) instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i act2: rct_inst ≔ rct_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›i is recontacted by the token owner of s successfully END RECONTACT_INST_KO: extended ordinary › REFINES RECONTACT_INST_KO ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: s ↦ FAIL_4 ∈ serviceState_4 not theorem ›the state of s is SUSPICIOUS grd4: susp_peers(s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ susp_peers(s)∩unav_peers not theorem ›i is a suspicious instance of s and is unavailable (can not be contacted) grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the token owner of s has not yet tried to recontact i grd7: rec_inst[{token_owner(s)}][{s}] ⊂ susp_peers(s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i END REFINES FAIL_DETECT ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_4 ∈ serviceState_4 not theorem › grd5: susp_peers(s) ≠ ∅ not theorem › grd8: rec_inst[{token_owner(s)}][{s}] = susp_peers(s) not theorem › END FAIL_CONFIGURE: extended ordinary › REFINES FAIL_CONFIGURE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_ACTIV_4 ∈ serviceState_4 not theorem › grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i ∉ run_peers(s) ∪ fail_peers[{s}] ∪ unav_peers ∪ dep_inst[{s}] not theorem ›i does not run s, is not failed for s, is not unavailable and is not already activated for s grd4: token_owner(s) ↦ (s ↦ i) ∉ actv_inst not theorem › grd5: s ↦ FAIL_CONFIG_4 ∈ serviceState_4 not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) < deplo_inst(s) not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_CONFIG_4}) ∪ {s ↦ DPL_4} › act2: run_peers(s) ≔ run_peers(s) ∪ dep_inst[{s}] › act3: dep_inst ≔ {s} ⩤ dep_inst › END HEAL: extended ordinary › REFINES HEAL ANY act10: rec_inst ≔ ∅ › act11: rct_inst ≔ ∅ › act12: actv_inst ≔ ∅ › act13: i_state ≔ InitStatus › END MAKE_PEER_UNAVAIL: not extended ordinary › REFINES MAKE_PEER_UNAVAIL ANY act3: susp_inst ≔ prs ⩤ susp_inst ›the peers in prs can not suspect instances anymore act4: rec_inst ≔ prs ⩤ rec_inst ›the peers in prs can not try to recontact instances anymore act5: rct_inst ≔ prs ⩤ rct_inst ›the peers in prs can not recontact instances anymore act6: actv_inst ≔ prs ⩤ actv_inst › act7: i_state ≔ i_s › END ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS grd4: susp_peers(s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty FAIL_DETECT: not extended ordinary › REFINES FAIL_DETECT ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem › grd5: susp_peers(s) ≠ ∅ not theorem › act4: fail_peers ≔ fail_peers ∪ ({s}×susp_peers(s)) › END FAIL_CONFIGURE: not extended ordinary › REFINES FAIL_CONFIGURE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i ∉ run_peers(s) ∪ fail_peers[{s}] ∪ unav_peers ∪ dep_inst[{s}] not theorem ›i does not run s, is not failed for s, is not unavailable and is not already activated for s grd4: token_owner(s) ↦ (s ↦ i) ∉ actv_inst not theorem › grd5: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) < deplo_inst(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ DPL_4 › act2: run_peers(s) ≔ run_peers(s) ∪ dep_inst[{s}] › act3: dep_inst ≔ {s} ⩤ dep_inst › END not extended ordinary › REFINES HEAL ANY MAKE_PEER_UNAVAIL ANY prs › E ›new values for token owner per service if needed act4: rec_inst ≔ prs ⩤ rec_inst ›the peers in prs can not try to recontact instances anymore act5: rct_inst ≔ prs ⩤ rct_inst ›the peers in prs can not recontact instances anymore ANY s ›a service s i ›an instance i WHERE END not extended ordinary › REFINES (s) ↦ s)) › act4: suspc_peers(token_owner(s) ↦ s) ≔ ∅ › WHERE grd1: s ∈ SERVICES not theorem › theorem › THEN prs › E ›new values for token owner per service if needed act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act3: suspc_inst(token_owner(s) ↦ s) ≔ ∅ › END grd7: rec_inst[{token_owner(s)}][{s}] ⊂ suspc_peers (token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to grd2: i_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › END s › WHERE grd2: p ∈ unav_peers not theorem › THEN act6: token_owner ≔ init_tok › act7: unav_peers ≔ ∅ › FAIL_DETECT: ↦ s) › act3: fail_peers ≔ fail_peers ∪ ({s}×suspc_peers(token_owner s ›a service s i ›an instance i grd6: dep_inst[{s}] ≠ ∅ not theorem › grd4: card(run_peers(s))+card(dep_inst[{s}]) ≥ min_inst(s) not MAKE_PEER_UNAVAIL ANY (srv) ↦ srv) ↦ ∅ ∈ s_i not theorem › THEN act2: suspc_peers(token_owner(s) ↦ s) ≔ suspc_inst(token_owner (s) ↦ s) › grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the token owner of s has not yet tried to recontact i WHERE grd1: s ∈ SERVICES not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › REDEPLOY ANY WHERE grd1: p ∈ PEERS not theorem › act4: failr_peers ≔ InitFail › act5: dep_instc ≔ InitFail › HEAL: act12: actv_inst ≔ ∅ › act13: i_state ≔ InitStatus › END MAKE_PEER_UNAVAIL: not extended ordinary › REFINES act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new value for token owner per service is given if needed act3: susp_inst ≔ prs ⩤ susp_inst ›the peers in prs can not suspect instances anymore act3: susp_inst ≔ susp_inst ⩥ ({s} ◁ ran(susp_inst)) › END RECONTACT_INST_OK: not extended ordinary › REFINES RECONTACT_INST_OK grd7: rec_inst[{token_owner(s)}][{s}] ⊂ suspc_peers (token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i grd2: i_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd5: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_ACTIV_4 › act2: run_peers(s) ≔ run_peers(s) ∖ suspc_peers(token_owner(s) END REDEPLOY_INSTC: extended ordinary › REFINES REDEPLOY_INSTC ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd7: actv_inst[{token_owner(s)}][{s}]=∅ not theorem › grd2: p ∈ unav_peers not theorem › THEN act1: unav_peers ≔ unav_peers ∖ {p} › END END act12: actv_inst ≔ ∅ › act13: i_state ≔ InitStatus › END MAKE_PEER_UNAVAIL: not extended ordinary › REFINES grd13: s_i ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd14: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p ↦ s ∈ dom(s_i) ⇒ p = E(s) not theorem › grd15: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ (E (srv) ↦ srv) ↦ suspc_inst(E(srv) ↦ srv) ∈ s_i not theorem › grd16: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ⇒ (E WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = RUN_4 not theorem › grd3: suspc_inst(token_owner(s) ↦ s) ≠ ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_4 › state of s is SUSPICIOUS grd4: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ suspc_peers(token_owner(s) ↦ s)∩unav_peers not theorem ›i is a suspicious instance of s and is unavailable (can not be contacted) FAIL_ACTIV: extended ordinary › REFINES FAIL_ACTIV ANY s › IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_IGN_4 not theorem › [{s}]) › act2: actv_inst ≔ actv_inst ⩥ ({s} ◁ ran(actv_inst)) › END extended ordinary › REFINES ANY p › act2: run_peers ≔ InitSrvcPeers › act3: suspc_peers ≔ InitSuspPeers › REDEPLOY: extended ordinary › REFINES MAKE_PEER_AVAIL EVENTS THEN INITIALISATION: not extended ordinary › MAKE_PEER_AVAIL: theorem › FAIL_DETECT: extended ordinary › (s)}][{s}] › act3: rec_inst ≔ rec_inst ⩥ ({s} ◁ ran(rec_inst)) › act4: rct_inst ≔ rct_inst ⩥ ({s} ◁ ran(rct_inst)) › END IS_OK: extended ordinary › REFINES IS_OK ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_DETECT_4 ∈ serviceState_4 not theorem › grd5: susp_peers(s) = ∅ not theorem › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_DETECT_4}) ∪ {s ↦ RUN_4} › END FAIL_ACTIV: extended ordinary › REFINES FAIL_ACTIV ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_DETECT_4 ∈ serviceState_4 not theorem › grd5: susp_peers(s) ≠ ∅ not theorem › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_DETECT_4}) ∪ {s ↦ FAIL_ACTIV_4} › act2: run_peers(s) ≔ run_peers(s) ∖ susp_peers(s) › act3: susp_peers(s) ≔ ∅ › act4: fail_peers ≔ fail_peers ∪ ({s}×susp_peers(s)) › END FAIL_IGNORE: extended ordinary › REFINES FAIL_IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_ACTIV_4 ∈ serviceState_4 not theorem › grd3: card(run_peers(s)) ≥ min_inst(s) not theorem › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_ACTIV_4}) ∪ {s ↦ FAIL_IGN_4} › END IGNORE: extended ordinary › REFINES IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_IGN_4 ∈ serviceState_4 not theorem › THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ FAIL_IGN_4}) ∪ {s ↦ RUN_4} › END REDEPLOY_INSTC: not extended ordinary › ANY s ›a service s i ›an instance i WHERE REDEPLOY_INSTS: not extended ordinary › REFINES REDEPLOY_INST ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) = deplo_inst(s) not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › grd8: s ↦ FAIL_CONFIG_4 ∈ serviceState_4 not theorem › WITH dep: dep=actv_inst[{token_owner(s)}][{s}] › THEN act1: dep_inst ≔ dep_inst ∪ ({s}×actv_inst[{token_owner(s)}] [{s}]) › act2: actv_inst ≔ actv_inst ⩥ ({s} ◁ ran(actv_inst)) › END REDEPLOY: not extended ordinary › REFINES REDEPLOY ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: s ↦ FAIL_CONFIG_4 ∈ serviceState_4 not theorem › grd7: actv_inst[{token_owner(s)}][{s}]=∅ not theorem › grd6: dep_inst[{s}] ≠ ∅ not theorem › grd4: card(run_peers(s))+card(dep_inst[{s}]) ≥ min_inst(s) not theorem › THEN THEN act1: serviceState_4 ≔ (serviceState_4 ∖ {s ↦ DPL_4}) ∪ {s ↦ RUN_4} › END UNFAIL_PEER: extended ordinary › REFINES UNFAIL_PEER ANY s › p › WHERE grd1: s ∈ SERVICES not theorem › grd2: p ∈ PEERS not theorem › grd3: s ↦ p ∈ fail_peers not theorem › THEN act1: fail_peers ≔ fail_peers∖{s ↦ p} › END MAKE_PEER_AVAIL: extended ordinary › REFINES MAKE_PEER_AVAIL ANY p › WHERE grd1: p ∈ PEERS not theorem › grd2: p ∈ unav_peers not theorem › THEN act1: unav_peers ≔ unav_peers ∖ {p} › END END SEES C08 VARIABLES run_peers › susp_peers › fail_peers › dep_inst › token_owner › unav_peers › susp_inst › rec_inst ›instances that are tried to be recontacted rct_inst ›instances effectively recontacted after a try actv_inst ›instances activated by token ownes i_state › INVARIANTS inv1: i_state ∈ (PEERS × SERVICES) ⇸ STATES_4 not theorem › inv2: ∀ s • s ∈ SERVICES ⇒ token_owner(s) ↦ s ∈ dom(i_state) not theorem › gluing_state1: ∀ s, stt • s ∈ SERVICES ∧ stt ∈ STATES_4 ∧ s ↦ stt ∈ serviceState_4 ⇒ (token_owner(s) ↦ s) ↦ stt ∈ i_state not theorem › gluing_state2: ∀ s, stt • s ∈ SERVICES ∧ stt ∈ STATES_4 ∧ (token_owner (s) ↦ s) ↦ stt ∈ i_state ⇒ s ↦ stt ∈ serviceState_4 not theorem › inv3: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(i_state) ⇒ p = token_owner(s) not theorem › EVENTS THEN act2: run_peers ≔ InitSrvcPeers › act3: susp_peers ≔ ∅ › act4: fail_peers ≔ ∅ › act5: dep_inst ≔ ∅ › act6: token_owner ≔ init_tok › act7: unav_peers ≔ ∅ › act8: susp_inst ≔ ∅ › p = E(s) not theorem › grd9: ∀ srv • srv ∈ SERVICES ⇒ (E(srv) ↦ srv) ↦ i_state (token_owner(srv) ↦ srv) ∈ i_s not theorem › THEN act1: unav_peers ≔ unav_peers ∪ prs ›the peers in prs become unavailable act2: token_owner ≔ token_owner  E ›new value for token owner per service is given if needed act1: i_state(token_owner(s) ↦ s) ≔ FAIL_4 › act2: susp_peers(s) ≔ susp_inst[{token_owner(s)}][{s}] › act3: susp_inst ≔ susp_inst ⩥ ({s} ◁ ran(susp_inst)) › END RECONTACT_INST_OK: not extended ordinary › REFINES RECONTACT_INST_OK token owner of s has not yet tried to recontact i grd7: rec_inst[{token_owner(s)}][{s}] ⊂ susp_peers(s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i END grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd5: susp_peers(s) ≠ ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_ACTIV_4 › act2: run_peers(s) ≔ run_peers(s) ∖ susp_peers(s) › act3: susp_peers(s) ≔ ∅ › REDEPLOY_INSTC: not extended ordinary › REFINES REDEPLOY_INSTC ANY s ›a service s i ›an instance i WHERE WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd7: actv_inst[{token_owner(s)}][{s}]=∅ not theorem › grd6: dep_inst[{s}] ≠ ∅ not theorem › grd4: card(run_peers(s))+card(dep_inst[{s}]) ≥ min_inst(s) not theorem › THEN act1: unav_peers ≔ unav_peers ∖ {p} › END END act3: suspc_peers ≔ InitSuspPeers › act4: fail_peers ≔ ∅ › act5: dep_inst ≔ ∅ › act6: token_owner ≔ init_tok › act7: unav_peers ≔ ∅ › act8: susp_inst ≔ ∅ › act10: rec_inst ≔ ∅ › act11: rct_inst ≔ ∅ › grd9: ∀ srv • srv ∈ SERVICES ⇒ (E(srv) ↦ srv) ↦ i_state (token_owner(srv) ↦ srv) ∈ i_s not theorem › grd10: p_s ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd11: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p ↦ s ∈ dom(p_s) ⇒ p = E(s) not theorem › grd12: ∀ srv • srv ∈ SERVICES ⇒ (E(srv) ↦ srv) ↦ suspc_peers (token_owner(srv) ↦ srv) ∈ p_s not theorem › THEN WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = RUN_4 not theorem › grd3: susp_inst[{token_owner(s)}][{s}] ≠ ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_4 › act2: suspc_peers(token_owner(s) ↦ s) ≔ susp_inst[{token_owner (s)}][{s}] › state of s is SUSPICIOUS grd4: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ suspc_peers(token_owner(s) ↦ s)∩unav_peers not theorem ›i is a suspicious instance of s and is unavailable (can not be contacted) grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the token owner of s has not yet tried to recontact i FAIL_ACTIV: not extended ordinary › REFINES FAIL_ACTIV ANY s › WHERE grd1: s ∈ SERVICES not theorem › IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_IGN_4 not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › [{s}]) › act2: actv_inst ≔ actv_inst ⩥ ({s} ◁ ran(actv_inst)) › END REFINES REDEPLOY ANY p › WHERE grd1: p ∈ PEERS not theorem › act8: suspc_inst ≔ InitSuspPeers › act10: rec_inst ≔ ∅ › act11: rct_inst ≔ ∅ › p = E(s) not theorem › grd12: ∀ srv • srv ∈ SERVICES ⇒ (E(srv) ↦ srv) ↦ suspc_peers (token_owner(srv) ↦ srv) ∈ p_s not theorem › FAIL ANY s › grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END REFINES THEN act1: dep_inst ≔ dep_inst ∪ ({s}×actv_inst[{token_owner(s)}] act1: fail_peers ≔ fail_peers∖{s ↦ p} › END inv8: dep_instc ∈ SERVICES → ℙ(PEERS) not theorem › gluing_act_1: ∀ s • s ∈ SERVICES ⇒ dep_inst[{s}] = dep_instc(s) not IGNORE: extended ordinary › › THEN not theorem › REDEPLOY: extended ordinary › extended ordinary › REFINES MAKE_PEER_AVAIL ANY act4: fail_peers ≔ ∅ › act5: dep_inst ≔ ∅ › act6: token_owner ≔ init_tok › act7: unav_peers ≔ ∅ › grd9: ∀ srv • srv ∈ SERVICES ⇒ (E(srv) ↦ srv) ↦ i_state (token_owner(srv) ↦ srv) ∈ i_s not theorem › grd10: p_s ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd11: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p ↦ s ∈ dom(p_s) ⇒ END not extended ordinary › REFINES i ›an instance i WHERE › grd5: suspc_peers(token_owner(s) ↦ s) = ∅ not theorem › act1: i_state(token_owner(s) ↦ s) ≔ FAIL_IGN_4 › END not theorem › grd8: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem grd2: p ∈ PEERS not theorem › grd3: s ↦ p ∈ fail_peers not theorem › inv7: failr_peers ∈ SERVICES → ℙ(PEERS) not theorem › gluing_fail_1: ∀ s • s ∈ SERVICES ⇒ fail_peers[{s}] = failr_peers(s) FAIL: ANY s ›a service s grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem grd3: card(run_peers(s)) ≥ min_inst(s) not theorem › THEN not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) WHERE grd1: s ∈ SERVICES not theorem › gluing_tok_own_rct1: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(rctt_inst) ⇒ rct_inst[{p}][{s}] = rctt_inst(p ↦ s) not theorem › MAKE_PEER_AVAIL: act3: suspc_peers ≔ InitSuspPeers › p = E(s) not theorem › susp become suspected instances for s by the token owner of s RECONTACT_INST_KO WHERE grd2: i_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) = deplo_inst(s) p › s) ∈ dom(rctt_inst) not theorem › INITIALISATION: not extended ordinary › grd1: prs ⊆ PEERS not theorem › grd2: prs ⊈ unav_peers not theorem › grd3: E ∈ SERVICES → PEERS not theorem ›new value for token owner per service if needed grd4: i_s ∈ (PEERS×SERVICES) ⇸ STATES_4 not theorem › grd5: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E (srv) = token_owner(srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd6: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ srv ∉ dom(susp_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers [{srv}]) not theorem ›if the owner of the token for a service becomes unavailable and the service is not suspicious, then a new token owner among available peers is chosen grd7: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ srv ∈ dom(susp_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers[{srv}] ∪ susp_peers(srv)) not theorem ›if the owner of the token for a service becomes unavailable, and the service possess suspicious instances, then a new token owner among available and not suspicious peers is chosen grd8: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p ↦ s ∈ dom(i_s) ⇒ s ›a service s susp ›suspicious instances WHERE grd1: s ∈ SERVICES not theorem › grd2: susp ⊆ PEERS not theorem › grd3: susp = run_peers(s) ∩ unav_peers not theorem ›instances in susp are suspicious if the peers running them becomes unavailable grd4: s ∉ dom(susp_inst[{token_owner(s)}]) not theorem ›the member of susp have not yet been suspected for s by the token owner of s grd5: i_state(token_owner(s) ↦ s) = RUN_4 not theorem ›the state of s is OK THEN act1: susp_inst ≔ susp_inst ∪ ({token_owner(s)} × ({s}×susp)) ›the members of susp become suspected instances for s by the token owner of s END FAIL: not extended ordinary › REFINES FAIL ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = RUN_4 not theorem › grd3: susp_inst[{token_owner(s)}][{s}] ≠ ∅ not theorem › THEN grd7: rec_inst[{token_owner(s)}][{s}] ⊂ susp_peers(s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i act2: rct_inst ≔ rct_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›i is recontacted by the token owner of s successfully END RECONTACT_INST_KO: not extended ordinary › REFINES RECONTACT_INST_KO ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS grd4: susp_peers(s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ susp_peers(s)∩unav_peers not theorem ›i is a suspicious instance of s and is unavailable (can not be contacted) grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the act2: susp_peers(s) ≔ susp_peers(s) ∖ rct_inst[{token_owner (s)}][{s}] › act3: rec_inst ≔ rec_inst ⩥ ({s} ◁ ran(rec_inst)) › act4: rct_inst ≔ rct_inst ⩥ ({s} ◁ ran(rct_inst)) › END IS_OK: not extended ordinary › REFINES IS_OK ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd5: susp_peers(s) = ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END FAIL_ACTIV: not extended ordinary › REFINES FAIL_ACTIV ANY s › WHERE END FAIL_IGNORE: not extended ordinary › REFINES FAIL_IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd3: card(run_peers(s)) ≥ min_inst(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_IGN_4 › END IGNORE: not extended ordinary › REFINES IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_IGN_4 not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END END REDEPLOY_INSTS: not extended ordinary › REFINES REDEPLOY_INSTS ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) = deplo_inst(s) not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › grd8: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › THEN act1: dep_inst ≔ dep_inst ∪ ({s}×actv_inst[{token_owner(s)}] [{s}]) › act2: actv_inst ≔ actv_inst ⩥ ({s} ◁ ran(actv_inst)) › END REDEPLOY: not extended ordinary › REFINES REDEPLOY ANY s › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END extended ordinary › SEES C08 VARIABLES run_peers › suspc_peers › grd2: prs ⊈ unav_peers not theorem › grd3: E ∈ SERVICES → PEERS not theorem ›new value for token owner per service if needed grd4: i_s ∈ (PEERS×SERVICES) ⇸ STATES_4 not theorem › grd5: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E SUSPECT_INST: extended ordinary › REFINES SUSPECT_INST ANY grd4: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ suspc_peers(token_owner(s) ↦ s)∖unav_peers not theorem ›i is a suspicious instance of s and is available (can be contacted) grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem › grd5: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › grd8: rec_inst[{token_owner(s)}][{s}] = suspc_peers (token_owner(s) ↦ s) not theorem › FAIL_CONFIGURE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd4: token_owner(s) ↦ (s ↦ i) ∉ actv_inst not theorem › grd5: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) < deplo_inst(s) not theorem › SEES grd1: prs ⊆ PEERS not theorem › act4: rct_inst ≔ prs ⩤ rct_inst ›the peers in prs can not ANY END ↦ s) › s ›a service s grd6: dep_inst[{s}] ≠ ∅ not theorem › SEES act13: i_state ≔ InitStatus › HEAL: extended ordinary › REFINES HEAL ANY C08 VARIABLES run_peers › suspc_peers › grd2: prs ⊈ unav_peers not theorem › grd3: E ∈ SERVICES → PEERS not theorem ›new value for token owner per service if needed grd4: i_s ∈ (PEERS×SERVICES) ⇸ STATES_4 not theorem › recontact instances anymore act5: actv_inst ≔ prs ⩤ actv_inst › act6: i_state ≔ i_s › act7: suspc_peers ≔ p_s › s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › act3: fail_peers ≔ fail_peers ∪ ({s}×suspc_peers(token_owner i ›an instance i grd4: card(run_peers(s))+card(dep_inst[{s}]) ≥ min_inst(s) not C08 END FAIL_DETECT: extended ordinary › REFINES FAIL_DETECT (s) ↦ s)) › act4: suspc_peers(token_owner(s) ↦ s) ≔ ∅ › END WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ DPL_4 › VARIABLES run_peers › suspc_peers › MAKE_PEER_UNAVAIL: not extended ordinary › REFINES UNFAIL_PEER: REFINES UNFAIL_PEER ANY s › p › WHERE grd1: s ∈ SERVICES not theorem › grd2: p ∈ PEERS not theorem › grd3: s ↦ p ∈ fail_peers not theorem › THEN act1: fail_peers ≔ fail_peers∖{s ↦ p} › END MAKE_PEER_AVAIL: extended ordinary › REFINES MAKE_PEER_AVAIL ANY p › WHERE grd1: p ∈ PEERS not theorem › grd2: p ∈ unav_peers not theorem › fail_peers › dep_inst › token_owner › unav_peers › susp_inst › rec_inst ›instances that are tried to be recontacted rct_inst ›instances effectively recontacted after a try actv_inst ›instances activated by token ownes i_state › INVARIANTS inv1: suspc_peers ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › inv2: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(suspc_peers) ⇒ p = token_owner(s) not theorem › inv3: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p = token_owner(s) ⇒ (p ↦ s) ∈ dom(suspc_peers) not theorem › gluing_tok_own1: ∀ s • s ∈ SERVICES ∧ s ∈ dom(susp_peers) ⇒ susp_peers(s) = suspc_peers(token_owner(s) ↦ s) not theorem › EVENTS INITIALISATION: not extended ordinary › THEN act2: run_peers ≔ InitSrvcPeers › (srv) = token_owner(srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd6: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ token_owner(srv) ↦ srv ∉ dom(suspc_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers s ›a service s susp ›suspicious instances WHERE grd1: s ∈ SERVICES not theorem › grd2: susp ⊆ PEERS not theorem › grd3: susp = run_peers(s) ∩ unav_peers not theorem ›instances in susp are suspicious if the peers running them becomes unavailable grd4: s ∉ dom(susp_inst[{token_owner(s)}]) not theorem ›the member of susp have not yet been suspected for s by the token owner of s grd5: i_state(token_owner(s) ↦ s) = RUN_4 not theorem ›the state of s is OK THEN act1: susp_inst ≔ susp_inst ∪ ({token_owner(s)} × ({s}×susp)) token owner of s has not yet tried to recontact i grd7: rec_inst[{token_owner(s)}][{s}] ⊂ suspc_peers (token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i act2: rct_inst ≔ rct_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›i is recontacted by the token owner of s successfully END RECONTACT_INST_KO: not extended ordinary › REFINES THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_DETECT_4 › act2: suspc_peers(token_owner(s) ↦ s) ≔ suspc_peers (token_owner(s) ↦ s) ∖ rct_inst[{token_owner(s)}][{s}] › act3: rec_inst ≔ rec_inst ⩥ ({s} ◁ ran(rec_inst)) › act4: rct_inst ≔ rct_inst ⩥ ({s} ◁ ran(rct_inst)) › END IS_OK: not extended ordinary › REFINES IS_OK ANY s › grd2: i_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd3: card(run_peers(s)) < min_inst(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_CONFIG_4 END FAIL_IGNORE: extended ordinary › REFINES FAIL_IGNORE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › THEN act1: actv_inst ≔ actv_inst ∪ {token_owner(s) ↦ (s ↦ i)} › END REDEPLOY_INSTS: extended ordinary › REFINES REDEPLOY_INSTS ANY s › WHERE grd1: s ∈ SERVICES not theorem › s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = DPL_4 not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END UNFAIL_PEER: extended ordinary › REFINES UNFAIL_PEER ANY s › fail_peers › dep_inst › token_owner › unav_peers › suspc_inst › rec_inst ›instances that are tried to be recontacted rct_inst ›instances effectively recontacted after a try actv_inst ›instances activated by token ownes i_state › INVARIANTS inv1: suspc_inst ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › inv2: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(suspc_inst) ⇒ p = token_owner(s) not theorem › grd5: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E (srv) = token_owner(srv) not theorem ›If the token owner of a service srv does not belong to prs, the token owner is not changed grd6: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ token_owner(srv) ↦ srv ∉ dom(suspc_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers[{srv}]) not theorem ›if the owner of the token for a service becomes unavailable and the service is not suspicious, then a new token owner among available peers is chosen grd7: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs ∧ token_owner(srv) ↦ srv ∈ dom(suspc_peers) ⇒ E(srv) ∈ run_peers(srv)∖(unav_peers ∪ prs ∪ fail_peers[{srv}] ∪ suspc_peers(token_owner(srv) ↦ srv)) not theorem act8: suspc_inst ≔ s_i › END grd2: i ∈ PEERS not theorem › grd3: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS ANY s › WHERE extended ordinary › grd3: i ∉ run_peers(s) ∪ fail_peers[{s}] ∪ unav_peers ∪ dep_inst[{s}] not theorem ›i does not run s, is not failed for s, is not act2: run_peers(s) ≔ run_peers(s) ∪ dep_inst[{s}] › act3: dep_inst ≔ {s} ⩤ dep_inst › failr_peers › dep_instc › MAKE_PEER_UNAVAIL ANY FAIL_CONFIGURE: REFINES unavailable and is not already activated for s END token_owner › prs › SUSPECT_INST: not extended ordinary › REFINES SUSPECT_INST ANY s ›a service s susp ›suspicious instances WHERE grd1: s ∈ SERVICES not theorem › grd2: susp ⊆ PEERS not theorem › grd3: susp = run_peers(s) ∩ unav_peers not theorem ›instances grd4: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ suspc_peers(token_owner(s) ↦ s)∖unav_peers not theorem ›i is a suspicious instance of s and is available (can be contacted) grd6: token_owner(s) ↦ (s ↦ i) ∉ rec_inst not theorem ›the token owner of s has not yet tried to recontact i grd7: rec_inst[{token_owner(s)}][{s}] ⊂ suspc_peers (token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem › grd5: suspc_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › grd8: rec_inst[{token_owner(s)}][{s}] = suspc_peers (token_owner(s) ↦ s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_DETECT_4 › act2: suspc_peers(token_owner(s) ↦ s) ≔ suspc_peers (token_owner(s) ↦ s) ∖ rct_inst[{token_owner(s)}][{s}] › act3: rec_inst ≔ rec_inst ⩥ ({s} ◁ ran(rec_inst)) › FAIL_CONFIGURE ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd3: card(run_peers(s)) < min_inst(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_CONFIG_4 › END grd4: token_owner(s) ↦ (s ↦ i) ∉ actv_inst not theorem › grd5: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd6: card(actv_inst[{token_owner(s)}][{s}]) < deplo_inst(s) not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › THEN act1: actv_inst ≔ actv_inst ∪ {token_owner(s) ↦ (s ↦ i)} › END unav_peers › E ›new values for token owner per service if needed HEAL: extended ordinary › REFINES HEAL ANY s › WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = DPL_4 not theorem › THEN suspc_inst › rect_inst ›instances that are tried to be recontacted rctt_inst ›instances effectively recontacted after a try actv_inst ›instances activated by token ownes i_state › INVARIANTS inv1: rect_inst ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › inv2: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(rect_inst) ⇒ p = token_owner(s) not theorem › i_s › p_s › s_i › rc_s › rt_s › WHERE grd1: prs ⊆ PEERS not theorem › grd2: prs ⊈ unav_peers not theorem › grd3: E ∈ SERVICES → PEERS not theorem ›new value for token ∪ prs ∪ suspicious peers is chosen grd8: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p ↦ s ∈ dom(i_s) ⇒ p = E(s) not theorem › ›the members of susp become suspected instances for s by the token owner of s END FAIL: not extended ordinary › REFINES FAIL ANY s › RECONTACT_INST_KO ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the WHERE grd1: s ∈ SERVICES not theorem › grd2: i_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd5: suspc_peers(token_owner(s) ↦ s) = ∅ not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END grd2: i_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd3: card(run_peers(s)) ≥ min_inst(s) not theorem › THEN act1: i_state(token_owner(s) ↦ s) ≔ FAIL_IGN_4 › END IGNORE: extended ordinary › REFINES grd6: card(actv_inst[{token_owner(s)}][{s}]) = deplo_inst(s) not theorem › grd7: card(dep_inst[{s}]) + card(run_peers(s)) < min_inst(s) not theorem › grd8: i_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › THEN act1: dep_inst ≔ dep_inst ∪ ({s}×actv_inst[{token_owner(s)}] p › WHERE grd1: s ∈ SERVICES not theorem › grd2: p ∈ PEERS not theorem › grd3: s ↦ p ∈ fail_peers not theorem › THEN act1: fail_peers ≔ fail_peers∖{s ↦ p} › END inv3: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p = token_owner(s) ⇒ (p ↦ s) ∈ dom(suspc_inst) not theorem › gluing_tok_own1: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom (suspc_inst) ⇒ susp_inst[{p}][{s}] = suspc_inst(p ↦ s) not theorem › EVENTS ›if the owner of the token for a service becomes unavailable, and the service possess suspicious instances, then a new token owner among available and not in susp are suspicious if the peers running them becomes unavailable grd4: suspc_inst(token_owner(s) ↦ s) = ∅ not theorem ›the member of susp have not yet been suspected for s by the token owner of s grd5: i_state(token_owner(s) ↦ s) = RUN_4 not theorem ›the state of s is OK act1: rec_inst ≔ rec_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›the token owner of s has tried to recontact i act2: rct_inst ≔ rct_inst ∪ {token_owner(s) ↦ (s ↦ i)} ›i is recontacted by the token owner of s successfully END act4: rct_inst ≔ rct_inst ⩥ ({s} ◁ ran(rct_inst)) › END IS_OK: extended ordinary › REFINES FAIL_IGNORE: extended ordinary › REFINES FAIL_IGNORE ANY extended ordinary › act1: i_state(token_owner(s) ↦ s) ≔ RUN_4 › END inv3: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p = token_owner(s) ⇒ (p ↦ s) ∈ dom(rect_inst) not theorem › owner per service if needed grd4: i_s ∈ (PEERS×SERVICES) ⇸ STATES_4 not theorem › REDEPLOY_INSTS: REFINES REDEPLOY_INSTS ANY extended ordinary › gluing_tok_own_rec1: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(rect_inst) ⇒ rec_inst[{p}][{s}] = rect_inst(p ↦ s) not theorem › grd5: p_s ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd6: s_i ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › UNFAIL_PEER: REFINES inv4: rctt_inst ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › grd7: rt_s ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › INITIALISATION: not extended ordinary › THEN act2: run_peers ≔ InitSrvcPeers › suspicious peers is chosen grd8: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p ↦ s ∈ dom(i_s) ⇒ grd6: susp ≠ ∅ not theorem › THEN act1: suspc_inst(token_owner(s) ↦ s) ≔ susp ›the members of REFINES IS_OK s › s › grd1: s ∈ SERVICES not theorem › s › grd1: s ∈ SERVICES not theorem › UNFAIL_PEER s › inv5: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ (p ↦ s) ∈ dom(rctt_inst) ⇒ inv6: ∀ p, s • p ∈ PEERS ∧ s ∈ SERVICES ∧ p = token_owner(s) ⇒ (p ↦ grd8: rc_s ∈ (PEERS×SERVICES) ⇸ ℙ(PEERS) not theorem › RECONTACT_INST_KO: extended ordinary › ANY WHERE WHERE ANY p = token_owner(s) not theorem › grd9:
	not theorem › recontact all the suspecious instances of s

  (token_owner(s) ↦ s) ∪ failr_inst (token_owner(s) ↦ s) ∪ unav_peers ∪ dep_instcs(token_owner(s) ↦ s) not theorem ›i does not run s, is not failed for s, is not unavailable and is not already srv ∈ SERVICES ⇒ dom(dom(inst_state) ▷ {srv}) ∖prs ≠ ∅ not theorem ›for each service srv, there must always be at least 1

	M20 inst_state ≔ inst_state  ((prop×{s})×{FAIL_4}) › suspct_peers ≔ suspct_peers  ((prop×{s})×{suspc_inst (token_owner(s) ↦ s)}) › act1: act2: act3: suspc_inst(token_owner(s) ↦ s) ≔ ∅ › M20 grd5: i ∈ suspct_peers(token_owner(s) ↦ s)∩unav_peers not theorem ›i is a suspicious instance of s and is unavailable (can not be contacted) grd6: i ∉ rect_inst(token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact i grd7: rect_inst(token_owner(s) ↦ s) ⊂ suspct_peers(token_owner M20 grd3: inst_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd4: suspct_peers(token_owner(s) ↦ s) = ∅ not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › M20 END extended ordinary › M20 grd3: i ∉ run_instactivated for s M20 grd3: inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd4: actv_instc(token_owner(s) ↦ s)=∅ not theorem › grd5: dep_instcs(token_owner(s) ↦ s) ≠ ∅ not theorem › M20 M21 MACHINE M21 grd3: ∀ srv • peer available MAKE_PEER_AVAIL: extended ordinary › REFINES M21 › REFINES grd4: E ∈ SERVICES → PEERS not theorem ›Value for token owner per service FAIL_IGNORE: REFINES grd4: i ∉ actv_instc(token_owner(s) ↦ s) not theorem › grd6: card(run_inst(token_owner(s) ↦ s))+card(dep_instcs MAKE_PEER_AVAIL M20 grd5: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∉ prs ⇒ E
	END (s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all THEN FAIL_IGNORE grd5: inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not (token_owner(s) ↦ s)) ≥ min_inst(s) not theorem › ANY SEES (srv) = token_owner(srv) not theorem ›If the token owner of a service srv	)
	act8: prs can not monitor the state of the services provided anymore inst_state ≔ (prs×SERVICES) ⩤ inst_state ›the peers in act9: run_inst ≔ (prs×SERVICES) ⩤ run_inst › act10: failr_inst ≔ (prs×SERVICES) ⩤ failr_inst › act11: dep_instcs ≔ (prs×SERVICES) ⩤ dep_instcs › extended ordinary › the suspecious instances of s THEN act1: inst_state ≔ inst_state  ((prop×{s})×{RUN_4}) › END ANY s › theorem › grd6: card(actv_instc(token_owner(s) ↦ s)) < deplo_inst(s) not grd7: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › p › WHERE C09 VARIABLES does not belong to prs, the token owner is not changed grd6: ∀ srv • srv ∈ SERVICES ∧ token_owner(srv) ∈ prs RECONTACT_INST_OK: REFINES RECONTACT_INST_OK ANY act1: rect_inst(token_owner(s) ↦ s) ≔ rect_inst(token_owner(s) ↦ s) ∪ {i} ›the token owner of s has tried to recontact i END extended ordinary › prop › WHERE theorem › grd7: card(dep_instcs(token_owner(s) ↦ s)) + card(run_inst THEN act1: inst_state≔ inst_state  ((prop×{s})×{DPL_4}) › grd1: p ∈ PEERS not theorem › grd2: p ∈ unav_peers not theorem › run_inst › suspct_peers › ⇒ E(srv) ∈ run_inst(token_owner(srv) ↦ srv)∖(unav_peers ∪ FAIL_ACTIV: REFINES grd1: s ∈ SERVICES not theorem › (token_owner(s) ↦ s)) < min_inst(s) not theorem › act2: run_inst ≔ run_inst  ((prop×{s})× {run_inst(token_owner THEN failr_inst › prs ∪ failr_inst(token_owner(srv) ↦ srv) ∪ suspct_peers(token_owner(srv) ↦ srv))
	END WHERE s i FAIL_ACTIV ›a service s ›an instance i grd2: prop ⊆ PEERS not theorem › THEN (s) ↦ s) ∪ dep_instcs(token_owner(s) ↦ s)}) › act1: unav_peers ≔ unav_peers ∖ {p} › dep_instcs › ∧ FAIL_DETECT: extended ordinary › REFINES ANY s › grd3: inst_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › act1: actv_instc(token_owner(s) ↦ s) ≔ actv_instc(token_owner (s) ↦ s) ∪ {i} › act3: dep_instcs ≔ dep_instcs  ((prop×{s})×{∅}) › END END token_owner › unav_peers › E(srv) ↦ srv ∈ dom(run_inst) ∩ dom(suspct_peers) ∩ dom (failr_inst) ∩ dom(dep_instcs) ∧ SUSPECT_INST: extended ordinary › REFINES SUSPECT_INST ANY s ›a service s grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS FAIL_DETECT ANY s › prop › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd4: card(run_inst(token_owner(s) ↦ s)) ≥ min_inst(s) not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › END not extended ordinary › END suspc_inst › run_inst(E(srv) ↦ srv) = run_inst(token_owner(srv) ↦ HEAL: extended ordinary › REFINES rect_inst ›instances that are tried to be recontacted rctt_inst ›instances effectively recontacted after a try srv) ∧ inst_state(E(srv) ↦ srv) = inst_state(token_owner(srv) ↦ REDEPLOY_INSTS: REFINES HEAL actv_instc ›instances activated by token ownes srv) ∧
	susp grd4: susp grd3: THEN REDEPLOY_INSTS ›suspicious instances suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the › inst_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not ANY inst_state › suspct_peers(E(srv) ↦ srv) = suspct_peers(token_owner
	WHERE set of suspicious peers for s is not empty WHERE theorem › act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_IGN_4}) › ANY s › INVARIANTS (srv) ↦ srv) ∧
	END inv1:	grd1: grd5: grd1: grd4: s › prop dom(run_inst) ⊆ dom(inst_state) not theorem › s ∈ SERVICES not theorem › i ∈ suspct_peers(token_owner(s) ↦ s)∖unav_peers not s ∈ SERVICES not theorem › suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › › failr_inst(E(srv) ↦ srv) = failr_inst(token_owner(srv) ↦
	grd2: grd3: theorem ›instances in susp are suspicious if the peers running them becomes susp ⊆ PEERS not theorem › susp = run_inst(token_owner(s) ↦ s) ∩ unav_peers not theorem ›i is a suspicious instance of s and is available (can be contacted) grd6: i ∉ rect_inst(token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact i grd2: prop ⊆ PEERS not theorem › grd7: susp ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_4 not theorem › grd5: prop = run_inst(token_owner(s) ↦ s) ∖ (unav_peers ∪ suspct_peers(token_owner(s) ↦ s)) not theorem › THEN IGNORE: extended ordinary › REFINES prop › WHERE grd1: s ∈ SERVICES not theorem › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › EVENTS extended ordinary › THEN INITIALISATION: srv) ∧
	unavailable		grd7: grd4: act1: IGNORE grd2: grd3: act1:	rect_inst(token_owner(s) ↦ s) ⊂ suspct_peers(token_owner suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › inst_state ≔ inst_state  ((prop×{s})×{FAIL_ACTIV_4}) › prop ⊆ PEERS not theorem › inst_state(token_owner(s) ↦ s) = DPL_4 not theorem › run_inst ≔ InitRunPeers ›
	grd4: (s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all suspc_inst(token_owner(s) ↦ s) = ∅ not theorem ›the grd5: rect_inst(token_owner(s) ↦ s) = suspct_peers(token_owner act2: run_inst ≔ run_inst  ((prop×{s})×{run_inst(token_owner ANY grd3: card(actv_instc(token_owner(s) ↦ s)) = deplo_inst(s) not grd4: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not act2: suspct_peers ≔ InitSuspPrs ›
	member of susp have not yet been suspected for s by the token owner of s the suspecious instances of s (s) ↦ s) not theorem › (s) ↦ s)∖suspct_peers(token_owner(s) ↦ s)}) › s › theorem › theorem › act3: failr_inst ≔ InitSuspPeers ›
		grd5: THEN grd6: act3: prop grd4: THEN act4:	inst_state(token_owner(s) ↦ s) = RUN_4 not theorem ›the prop = ((run_inst(token_owner(s) ↦ s) ∖ suspct_peers failr_inst ≔ failr_inst  ((prop×{s})× {failr_inst › card(dep_instcs(token_owner(s) ↦ s)) + card(run_inst dep_instcs ≔ InitSuspPeers ›
	state of s is OK act1: (token_owner(s) ↦ s)) ∪ rctt_inst(token_owner(s)↦ s))∖unav_peers not theorem › rect_inst(token_owner(s) ↦ s) ≔ rect_inst(token_owner(s) (token_owner(s) ↦ s) ∪ suspct_peers(token_owner(s) ↦ s)}) › WHERE (token_owner(s) ↦ s)) < min_inst(s) not theorem › act1: inst_state≔ inst_state  ((prop×{s})×{RUN_4}) › act5: token_owner ≔ init_tok ›
	grd6: ↦ s) ∪ {i} ›the token owner of s has tried to recontact i susp ≠ ∅ not theorem › grd8: susp = suspct_peers(token_owner(s) ↦ s)∖rctt_inst act4: suspct_peers ≔ suspct_peers  ((prop×{s})×{∅}) › grd1: s ∈ SERVICES not theorem › grd5: inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not END act6: unav_peers ≔ ∅ ›
	THEN act1: susp become suspected instances for s by the token owner of s suspc_inst(token_owner(s) ↦ s) ≔ susp ›the members of END extended ordinary › act2: rctt_inst(token_owner(s) ↦ s) ≔ rctt_inst(token_owner(s) ↦ s) ∪ {i} ›i is recontacted by the token owner of s successfully END (token_owner(s)↦ s) not theorem › THEN act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_DETECT_4}) › END extended ordinary › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_IGN_4 not theorem › theorem › grd6: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › act7: suspc_inst ≔ InitSuspPeers › UNFAIL_PEER: extended ordinary › REFINES act8: rect_inst ≔ InitSuspPeers › act9: rctt_inst ≔ InitSuspPeers › FAIL_CONFIGURE: REFINES grd4: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not THEN UNFAIL_PEER act10: actv_instc ≔ InitSuspPeers › RECONTACT_INST_KO: extended ordinary › REFINES act2: suspct_peers ≔ suspct_peers  ((prop×{s})×{susp}) › act3: rect_inst(token_owner(s) ↦ s) ≔ ∅ › FAIL_CONFIGURE ANY theorem › THEN act1: dep_instcs ≔ dep_instcs  ((prop×{s})× {dep_instcs (token_owner(s)↦s) ∪ actv_instc(token_owner(s)↦s)}) › ANY s › act11: inst_state ≔ InitStateSrv › END FAIL: REFINES FAIL ANY s › prop › RECONTACT_INST_KO ANY s ›a service s i ›an instance i WHERE act4: rctt_inst(token_owner(s) ↦ s) ≔ ∅ › END IS_OK: extended ordinary › REFINES s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › act1: inst_state ≔ inst_state  ((prop×{s})×{RUN_4}) › END REDEPLOY_INSTC: not extended ordinary › REFINES act2: actv_instc(token_owner(s) ↦ s) ≔ ∅ › END not extended ordinary › p › prop › WHERE grd1: s ∈ SERVICES not theorem › not extended ordinary › MAKE_PEER_UNAVAIL: REFINES MAKE_PEER_UNAVAIL REDEPLOY: REFINES grd2: prop ⊆ PEERS not theorem › ANY
		WHERE grd1: IS_OK grd3: REDEPLOY_INSTC s ∈ SERVICES not theorem › inst_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not REDEPLOY grd3: p ∈ PEERS not theorem › prs ›Peers that will become unavailable
	theorem ›	ANY ANY ANY	grd1: grd2: grd4: E ›Values for token owner per service s ∈ SERVICES not theorem › i ∈ PEERS not theorem › p ∈ failr_inst(token_owner(s) ↦ s) not theorem ›
		grd2: grd3: s › grd4: s ›a service s prop ⊆ PEERS not theorem › inst_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the card(run_inst(token_owner(s) ↦ s)) < min_inst(s) not s › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not WHERE
	grd3: state of s is SUSPICIOUS inst_state(token_owner(s) ↦ s) = RUN_4 not theorem › prop › theorem › i ›an instance i prop › theorem › grd1: prs ⊆ PEERS not theorem ›
		grd4: grd4: WHERE grd5: WHERE WHERE THEN grd2:	suspc_inst(token_owner(s) ↦ s) ≠ ∅ not theorem › suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the prop = run_inst(token_owner(s) ↦ s)∖unav_peers not prs ⊈ unav_peers not theorem ›the peers in prs are not
	grd5: set of suspicious peers for s is not empty prop = run_inst(token_owner(s) ↦ s)∖(suspc_inst grd1: s ∈ SERVICES not theorem › theorem › grd1: s ∈ SERVICES not theorem › grd1: s ∈ SERVICES not theorem › act1: failr_inst ≔ failr_inst  ((prop×{s})×{failr_inst yet unavalaible
	(token_owner(s) ↦ s) ∪ unav_peers) not theorem › grd5: i ∈ suspct_peers(token_owner(s) ↦ s)∩unav_peers not grd2: prop ⊆ PEERS not theorem › THEN grd2: i ∈ PEERS not theorem › grd2: prop ⊆ PEERS not theorem › (token_owner(s) ↦ s) ∖ {p}}) › grd3: ∀ srv • srv ∈ SERVICES ⇒ dom(dom(inst_state) ▷ {srv})
	THEN theorem ›i is a suspicious instance of s and is unavailable (can not be grd3: inst_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_CONFIG_4}) › grd3: i ∉ run_inst(token_owner(s) ↦ s) ∪ failr_inst grd3: inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not END ∖prs ≠ ∅ not theorem ›for each service srv, there must always be at least 1
	contacted) theorem › (token_owner(s) ↦ s) ∪ unav_peers ∪ dep_instcs(token_owner(s) ↦ s) not theorem theorem › peer available

  : inst_state ≔ (prs×SERVICES) ⩤ inst_state ›the peers in prs can not monitor the state of the services provided anymore ↦ s) not theorem ›the token owner of s has not yet tried to recontact all M21 grd7: rect_inst(token_owner(s) ↦ s) ⊂ suspct_peers(token_owner (s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s

		M21 M21 M21 M21 M21 M21
	grd6:	card(run_inst(token_owner(s) ↦ s))+card(dep_instcs
	END THEN grd5: FAIL_IGNORE inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not (token_owner(s) ↦ s)) ≥ min_inst(s) not theorem › ANY
	act9: act10: failr_inst ≔ (prs×SERVICES) ⩤ failr_inst › run_inst ≔ (prs×SERVICES) ⩤ run_inst › act11: dep_instcs ≔ (prs×SERVICES) ⩤ dep_instcs › SUSPECT_INST: extended ordinary › END REFINES SUSPECT_INST ANY s ›a service s susp ›suspicious instances WHERE grd1: s ∈ SERVICES not theorem › grd2: susp ⊆ PEERS not theorem › grd3: susp = run_inst(token_owner(s) ↦ s) ∩ unav_peers not theorem ›instances in susp are suspicious if the peers running them becomes unavailable grd4: suspc_inst(token_owner(s) ↦ s) = ∅ not theorem ›the member of susp have not yet been suspected for s by the token owner of s grd5: inst_state(token_owner(s) ↦ s) = RUN_4 not theorem ›the state of s is OK grd6: susp ≠ ∅ not theorem › THEN act1: suspc_inst(token_owner(s) ↦ s) ≔ susp ›the members of susp become suspected instances for s by the token owner of s END FAIL: extended ordinary › REFINES FAIL ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = RUN_4 not theorem › grd4: suspc_inst(token_owner(s) ↦ s) ≠ ∅ not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖(suspc_inst (token_owner(s) ↦ s) ∪ unav_peers) not theorem › THEN act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_4}) › act2: suspct_peers ≔ suspct_peers  ((prop×{s})×{suspc_inst (token_owner(s) ↦ s)}) › act3: suspc_inst(token_owner(s) ↦ s) ≔ ∅ › act1: inst_state ≔ inst_state  ((prop×{s})×{RUN_4}) › ANY theorem › grd7: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not p › RECONTACT_INST_OK: extended ordinary › REFINES RECONTACT_INST_OK ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS grd4: suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ suspct_peers(token_owner(s) ↦ s)∖unav_peers not theorem ›i is a suspicious instance of s and is available (can be contacted) grd6: i ∉ rect_inst(token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact i grd7: rect_inst(token_owner(s) ↦ s) ⊂ suspct_peers(token_owner (s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact all the suspecious instances of s THEN act1: rect_inst(token_owner(s) ↦ s) ≔ rect_inst(token_owner(s) ↦ s) ∪ {i} ›the token owner of s has tried to recontact i act2: rctt_inst(token_owner(s) ↦ s) ≔ rctt_inst(token_owner(s) ↦ s) ∪ {i} ›i is recontacted by the token owner of s successfully END RECONTACT_INST_KO: extended ordinary › REFINES RECONTACT_INST_KO ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_4 not theorem ›the state of s is SUSPICIOUS grd4: suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem ›the set of suspicious peers for s is not empty grd5: i ∈ suspct_peers(token_owner(s) ↦ s)∩unav_peers not theorem ›i is a suspicious instance of s and is unavailable (can not be contacted) grd6: i ∉ rect_inst(token_owner(s) ↦ s) not theorem ›the token owner of s has not yet tried to recontact i grd7: rect_inst(token_owner(s) ↦ s) ⊂ suspct_peers(token_owner act1: rect_inst(token_owner(s) ↦ s) ≔ rect_inst(token_owner(s) ↦ s) ∪ {i} ›the token owner of s has tried to recontact i END FAIL_DETECT: extended ordinary › REFINES susp › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd7: susp ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_4 not theorem › grd4: suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › grd5: rect_inst(token_owner(s) ↦ s) = suspct_peers(token_owner (s) ↦ s) not theorem › grd6: prop = ((run_inst(token_owner(s) ↦ s) ∖ suspct_peers (token_owner(s) ↦ s)) ∪ rctt_inst(token_owner(s)↦ s))∖unav_peers not theorem › grd8: susp = suspct_peers(token_owner(s) ↦ s)∖rctt_inst (token_owner(s)↦ s) not theorem › THEN act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_DETECT_4}) › act2: suspct_peers ≔ suspct_peers  ((prop×{s})×{susp}) › act3: rect_inst(token_owner(s) ↦ s) ≔ ∅ › act4: rctt_inst(token_owner(s) ↦ s) ≔ ∅ › END IS_OK: extended ordinary › REFINES IS_OK ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd4: suspct_peers(token_owner(s) ↦ s) = ∅ not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › END FAIL_ACTIV: extended ordinary › REFINES FAIL_ACTIV ANY s › grd3: inst_state(token_owner(s) ↦ s) = FAIL_DETECT_4 not theorem › grd4: suspct_peers(token_owner(s) ↦ s) ≠ ∅ not theorem › grd5: prop = run_inst(token_owner(s) ↦ s) ∖ (unav_peers ∪ suspct_peers(token_owner(s) ↦ s)) not theorem › THEN act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_ACTIV_4}) › act2: run_inst ≔ run_inst  ((prop×{s})×{run_inst(token_owner (s) ↦ s)∖suspct_peers(token_owner(s) ↦ s)}) › act3: failr_inst ≔ failr_inst  ((prop×{s})× {failr_inst (token_owner(s) ↦ s) ∪ suspct_peers(token_owner(s) ↦ s)}) › act4: suspct_peers ≔ suspct_peers  ((prop×{s})×{∅}) › END FAIL_CONFIGURE: extended ordinary › REFINES FAIL_CONFIGURE ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › grd4: card(run_inst(token_owner(s) ↦ s)) < min_inst(s) not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › THEN act1: inst_state ≔ inst_state  ((prop×{s})×{FAIL_CONFIG_4}) › END FAIL_IGNORE: extended ordinary › REFINES s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_ACTIV_4 not theorem › THEN act1: ≔ inst_state  ((prop×{s})×{FAIL_IGN_4}) › END IGNORE: extended ordinary › REFINES IGNORE ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_IGN_4 not theorem › grd4: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › THEN act1: inst_state ≔ inst_state  ((prop×{s})×{RUN_4}) › END REDEPLOY_INSTC: extended ordinary › REFINES REDEPLOY_INSTC ANY s ›a service s i ›an instance i WHERE grd1: s ∈ SERVICES not theorem › grd2: i ∈ PEERS not theorem › grd3: i ∉ run_inst(token_owner(s) ↦ s) ∪ failr_inst (token_owner(s) ↦ s) ∪ unav_peers ∪ dep_instcs(token_owner(s) ↦ s) not theorem ›i does not run s, is not failed for s, is not unavailable and is not already activated for s grd4: i ∉ actv_instc(token_owner(s) ↦ s) not theorem › grd6: card(actv_instc(token_owner(s) ↦ s)) < deplo_inst(s) not theorem › grd7: card(dep_instcs(token_owner(s) ↦ s)) + card(run_inst (token_owner(s) ↦ s)) < min_inst(s) not theorem › THEN act1: actv_instc(token_owner(s) ↦ s) ≔ actv_instc(token_owner (s) ↦ s) ∪ {i} › REDEPLOY_INSTS ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: card(actv_instc(token_owner(s) ↦ s)) = deplo_inst(s) not theorem › grd4: card(dep_instcs(token_owner(s) ↦ s)) + card(run_inst (token_owner(s) ↦ s)) < min_inst(s) not theorem › grd5: inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd6: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › THEN act1: dep_instcs ≔ dep_instcs  ((prop×{s})× {dep_instcs (token_owner(s)↦s) ∪ actv_instc(token_owner(s)↦s)}) › act2: actv_instc(token_owner(s) ↦ s) ≔ ∅ › END REDEPLOY: extended ordinary › REFINES REDEPLOY ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = FAIL_CONFIG_4 not theorem › grd4: actv_instc(token_owner(s) ↦ s)=∅ not theorem › grd5: dep_instcs(token_owner(s) ↦ s) ≠ ∅ not theorem › grd6: card(run_inst(token_owner(s) ↦ s))+card(dep_instcs (token_owner(s) ↦ s)) ≥ min_inst(s) not theorem › theorem › THEN act1: inst_state≔ inst_state  ((prop×{s})×{DPL_4}) › act2: run_inst ≔ run_inst  ((prop×{s})× {run_inst(token_owner (s) ↦ s) ∪ dep_instcs(token_owner(s) ↦ s)}) › act3: dep_instcs ≔ dep_instcs  ((prop×{s})×{∅}) › END ANY s › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: inst_state(token_owner(s) ↦ s) = DPL_4 not theorem › grd4: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › THEN act1: inst_state≔ inst_state  ((prop×{s})×{RUN_4}) › END UNFAIL_PEER: extended ordinary › REFINES UNFAIL_PEER ANY s › p › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd3: p ∈ PEERS not theorem › grd4: p ∈ failr_inst(token_owner(s) ↦ s) not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › THEN act1: failr_inst ≔ failr_inst  ((prop×{s})×{failr_inst (token_owner(s) ↦ s) ∖ {p}}) › END MAKE_PEER_AVAIL: extended ordinary › REFINES MAKE_PEER_AVAIL WHERE grd1: p ∈ PEERS not theorem › grd2: p ∈ unav_peers not theorem › THEN act1: unav_peers ≔ unav_peers ∖ {p} › END (s) THEN FAIL_DETECT ANY s › prop › prop › WHERE grd1: s ∈ SERVICES not theorem › grd2: prop ⊆ PEERS not theorem › grd4: card(run_inst(token_owner(s) ↦ s)) ≥ min_inst(s) not theorem › grd5: prop = run_inst(token_owner(s) ↦ s)∖unav_peers not theorem › END REFINES HEAL REDEPLOY_INSTS: extended ordinary › extended ordinary › REFINES HEAL: END

⋆ The current report is the companion paper of the paper[START_REF] Andriamiarina | Analysis of self-* and p2p systems using refinement[END_REF] accepted for publication in the volume 8477 of the serie Lecture Notes in Computer Science. The Event-B models are available at the link http://eb2all.loria.fr. Processed on July 3, 2014.

http://lfm.iti.kit.edu/download/EventB_Summary.pdf

The assertions (s → st ∈ serviceState), describing the state (st) of a service (s), are shorten into (st), in the nodes of the refinement diagrams, for practical purposes.

⊕: to add elements to a model, ⊖: to remove elements from a model

http://eb2all.loria.fr/html_files/files/selfhealing/self-healing.zip