Jobs/M2 2017 MC Spot demo
|Interactive Spot demonstration|
M2 2017 MC Spot demo
5-6 months in 2018
Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange
|General presentation of the field||
The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.
The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample).
This internship targets students who:
We wish to build an interactive, web-based demonstration prototype for Spot, to illustrate the interest of model checking. The targeted use-case is the verification of a controller for lifts.
The prototype should provide several functionalities, among which:
Such a prototype is intended to be used in the communication of the LRDE, for example during the Journées Portes Ouvertes.
|Benefit for the candidate|
|Place||LRDE: How to get to us|
1000 € gross / month
|Future work opportunities|
colange <at> lrde.epita.fr