PADEC - Coq Library

Library Padec.MessagePassing.Self_StabilizationMP

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Streams.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import AlgorithmMP.
From Padec Require Import RelModelMP.
From Padec Require Import ExecMP.

Set Implicit Arguments.
Open Scope signature_scope.

Specifications for self-stabilizing algorithms and

silent self-stabilizing algorithms

Section Self_StabilizationMP.

Context {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork} {Algo: MPAlgorithm}.

Assumption made on read-only variables of the algorithm

Hypothesis assume: Stable_Assumption.

In the sequel, we use:

Daemon_fairness: Exec -> Prop = specification of the Daemon Fairness

(e.g. unfair daemon, weakly fair daemon, synchronous daemon ...)

SPEC: Exec -> Prop = specification of the algorithm
LEG_STATE: Env -> Prop = legitimate states for stelf-stabilization

Self-stabilization: Closure w.r.t. legitimate states Definition closure (LEG_STATE: Env -> Prop): Prop := forall (env env': Env), Assume env -> LEG_STATE env -> Step env' env -> LEG_STATE env'.

  Definition closure (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop): Prop :=
    forall (e: Exec),
      Assume (fst (hd e)) -> is_exec e -> Daemon_fairness e ->
      LEG_STATE (fst (hd e)) -> ForAll (fun e => LEG_STATE (fst (hd e))) e.

Self-stabilization: Convergence to legitimate states

  Definition convergence (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop): Prop :=
    forall (e: Exec),
      Assume (fst (hd e)) -> is_exec e -> Daemon_fairness e ->
      Exists (fun suf: Exec => LEG_STATE (fst (hd suf))) e.

Self-stabilization: Meets specification when initialized in legitimate states

  Definition spec_ok (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop) (SPEC: Exec -> Prop): Prop :=
    forall (e: Exec),
      Assume (fst (hd e)) -> is_exec e -> Daemon_fairness e ->
      LEG_STATE (fst (hd e)) -> SPEC e.

Self-stabilization: full property

  Definition self_stab (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop) (SPEC: Exec -> Prop): Prop :=
    closure Daemon_fairness LEG_STATE /\ convergence Daemon_fairness LEG_STATE
    /\ spec_ok Daemon_fairness LEG_STATE SPEC.

  Definition self_stabilization (Daemon_fairness: Exec -> Prop)
             (SPEC: Exec -> Prop): Prop :=
    exists (LEG_STATE: Env -> Prop), self_stab Daemon_fairness LEG_STATE SPEC.

  Lemma self_stabilization_alt:
    forall Daemon_fairness SPEC LEG_STATE,
      self_stab Daemon_fairness LEG_STATE SPEC <->
      forall e, Assume (fst (hd e)) -> is_exec e -> Daemon_fairness e ->
                ( LEG_STATE (fst (hd e)) ->
                  ForAll (fun e => LEG_STATE (fst (hd e))) e )

                /\
                Exists (fun suf: Exec => LEG_STATE (fst (hd suf))) e

                /\
                ( LEG_STATE (fst (hd e)) -> SPEC e ) .

End Self_StabilizationMP.

Close Scope signature_scope.
Unset Implicit Arguments.