Ph.D

Group : Parallelism

*Observing self-stabilization*
Starts on 09/01/2002

Advisor : ROZOY, Brigitte

[Joffroy BEAUQUIER]

**Funding :** MNRT

**Affiliation :** Université Paris-Saclay

**Laboratory :** LRI

**Defended** on 15/12/2005, committee :

Joffroy Beauquier

Véronique Benzaken

Béatrice Bérard

Yves Métivier

Brigitte Rozoy

André Schiper

**Research activities :**
- Verification

- Distributed algorithms

- Self-stabilisation

- Design

- Fault Tolerance

**Abstract :**
Distributed systems have two main characteristics: they are complex

and subject to failures. So, the verification and the study of fault

tolerance in such systems are two major issues. In this thesis, we

propose a model-checking verification technique for

distributed systems. We present and prove an algorithm, based on

partial orders, which builds a small subset of the whole set of states

of a distributed system. In the reduced generated graph, it is still

possible to verify stable properties of the considered system. We

then study self-stabilizing systems which are fault tolerant

distributed systems. Self-stabilizing systems are systems which, from

any initialization, eventually behaves correctly, regarding to their

specifications. The drawback of such systems is that they cannot

determine whether or not they verify their specifications. In this

thesis we propose a new model, in which the system can decide if it

verifies its specification by introducing a new abstraction called

observer. With this model, we prove that if there exists a synchronous

self-stabilizing distributed solution for some problem in a

distinguished network, then there exists a synchronous

self-stabilizing distributed solution for the same problem in the same

network which accepts an observer. Finally, we introduce the notion of

a probabilistic observer and we prove that such an observer allows to

decide for a larger class of self-stabilizing systems than

deterministic observers.

*More information: *http://info.iut-bm.univ-fcomte.fr/staff/pilard/publication/publication.php