Supervised by: Erwan Jahier, Karine Altisen, Stéphane Devismes
Verimag Lab
Contacts: Erwan.JahierATuniv-grenoble-alpes.fr, Karine.AltisenATuniv-grenoble-alpes.fr, Stephane.DevismesATu-picardie.fr
Keywords: distributed algorithms, self-stabilization, simulation, formal methods.
The design of distributed algorithms usually involves high-level models to describe the system and its semantics. The model abstracts away most of the very precise behavior of the system to rather focus on the main nature of distributed computations, that is: processes have local programs and memory and can only share information using message exchanges.
Distributed algorithms are developed and analyzed in such a (theoretical) model: usually their specification as well as their complexity are proven. Now, the distributed nature of the computation involves many situations and particular cases; furthermore, the design of distributed algorithms becomes harsher when in one hand the requirements are reinforced and in the other hand the environment becomes more intricate (how to obtain a fault-tolerant solution in a very highly dynamic environment?). This is why tools helping the design are mandatory.
We propose here a simulator, called SASA, that can be used as a debugging tool to interactively test the solution (i.e. the distributed algorithm) under development. The SASA simulator focuses on a family of fault-tolerant solutions called self-stabilizing algorithms. SASA has simulation campaign support: the tool allows to compute benchmarks where simulations can be launched as many times as necessary on various inputs. Recent developments include the connection of SASA to model-checking tools.
Further developments of SASA (written in OCAML) would include:
- connection to the Coq PADEC framework using an ad-hoc input algorithm language;
- perform a broad simulation campaign to evaluate search heuristics to find worst-case execution time scenarios
- study the average time complexity of a given self-stabilizing algorithm
The goal of the internship would be to work on one of those axis of development.
SASA Webpage: https://verimag.gricad-pages.univ-g...
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 (funded by the SkyData project).
