Supervised by : Karine Altisen, Pierre Corbineau, Stéphane Devismes
Verimag Lab
Contacts : Karine.AltisenATuniv-grenoble-alpes.fr, Pierre.CorbineauATuniv-grenoble-alpes.fr, Stephane.DevismesATu-picardie.fr
Keywords : distributed algorithms, self-stabilization, Coq.
Scientific Context.
Modern distributed systems can be large-scale (e.g., Internet), dynamic (e.g., Peer-to-Peer systems), and / or resource constrained (e.g., wireless sensor networks — WSNs). Those characteristics increase the number of faults which may hit the system. For instance, in WSNs, processes are subject to crash failures because of their limited battery. Moreover, their communications use radio channels which are subject to intermittent loss of messages. Due to their large-scale and the adversarial environment where they may be deployed, intervention to repair them cannot be always envisioned. In this context, fault-tolerance, (the ability of a distributed algorithm to endure the faults by itself) is mandatory.
Self-stabilization (see Dijkstra74) is a versatile lightweight technique to withstand transient faults in a distributed system. After transient faults hit and place the system into some arbitrary global state, a self-stabilizing algorithm returns, in finite time, to a correct behavior without external intervention. Self-stabilization makes no hypotheses on the nature or extent of transient faults that could hit the system, and recovers from the effects of those faults in a unified manner.
Today’s researches on self-stabilizing algorithms focus on more and more complex problems and adversarial environments. This makes the proof that an algorithm actually achieves self-stabilization even more complex and subtle to establish. Those proofs are usually performed by hand, using informal reasoning. Such methods are clearly pushed to their limits and this justifies the use of a proof assistant.
Proof assistants are environments in which a user can express programs, state theorems, and develop proofs interactively, those ones being mechanically checked (that is machine-checked). In particular, the Coq proof assistant, which is targeted by this project, has been successfully used for various tasks such as mathematical developments as involved as the 4-colors or Feit-Thompson theorems, formalization of programming language semantics leading to the certification of a C compiler, certified numerical libraries, and verification of cryptographic protocols.
Project.
We propose a framework, based on Coq, to (semi-) automatically construct certified proofs of self-stabilizing algorithms called PADEC. The framework imports into Coq the computational model in which the algorithms are designed, formalizes the algorithms themselves and their specifications. Then the algorithms are proved using Coq including safety, convergence. The current development of the framework includes performance studies and complexity proofs but also connection with other formal tools.
In this internship, we propose to contribute to further developments of the framework under one of the following directions
- Development of compositional results : the design of self-stabilizing algorithms is usually compositional (two simple algorithms can be used together (composed) to create a more complex one) in order to deduce the complexity of a composed algorithm using the cost of each brick.
- Connection of the PADEC framework to the SASA simulator, a simulator dedicated to distributed self-stabilizing algorithms so that the algorithms under test and the algorithms that are mechanically proved share the same definition.
Precisely, the subject requires :
- A bibliographical study and a deep understanding of the PADEC framework. This may require learning some Coq skills, if necessary.
- To develop further the existing Coq libraries about tools in one or the other direction.
Required Skills. An important background about sequential algorithmic, in particular proof of algorithms, is mandatory. Background about distributed systems and formal methods is a plus.
Working context. The internship is part of ANR project SkyData. The student will be integrated in the lab Verimag.
Possible extension into a PhD thesis.
References
- Coq The Coq Development Team. The Coq Proof Assistant Documentation, http://coq.inria.fr/refman/.
- PADEC Karine Altisen, Corbineau Pierre, and Stéphane Devismes. Padec : A framework for certified self-stabilization, http://www-verimag.imag.fr/ altisen....
- Dijkstra74 E.W. Dijkstra. Self-Stabilizing Systems in Spite of Distributed Control. Commun. ACM, 17:643—644, 1974.
