Contact: Wajeb Saab
Background:
Axo [1] is a fault-tolerance protocol, developed at LCA2, targeting crash and delay faults for real-time systems.
It achieves fault-masking, fault-detection, and fault-recovery, for asynchronous real-time control applications.
Its safety and availability guarantees have been proven to hold for its masking algorithm, and bounds on the performance of its detection and recovery algorithms have been derived.
Axo has been implemented in C/C++.
The Axo software is a thin fault-tolerance layer. Thus, it is necessary to model, validate, and verify desirable properties on its behavior.
We are looking for a motivated student that will take on this task.
Project Goals:
- Surveying possible tools that can be used for modeling Axo.
- Modeling the Axo components in a few modeling languages and theorem provers.
- Deriving some interesting properties concerning Axo.
- Proving / Model-Checking / Verifying such properties on the models.
Benefits:
The project gives the student a chance to gain an in-depth understanding of fault-tolerance techniques, with an emphasis on real-time control applications.
The project also helps the student gain experience in one or more modeling tools and theorem provers, which may be useful for many future projects.
Required skills:
- C/C++
- BIP / Alloy / Coq / Isabelle / NuSMV / Spin / Uppaal
The source code of Axo is in C/C++, so knowledge and experience in C/C++ or equivalent programming skills are essential.
The above are examples of modeling tools and theorem provers that may be used in the project. Knowledge or experience in such tools would be useful for the student.
References:
[1] http://infoscience.epfl.ch/record/217463
Supervisors: Wajeb Saab