]>
2020-12-02T22:25:25+01:00
Jobs/M2 2017 MC Spot demo
0
en
Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange
Alexandre Duret-Lutz
Étienne Renault
Maximilien Colange
1000 € gross / month
colange <at> lrde.epita.fr
5-6 months in 2018
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).
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:
* a graphical representation of the system and its evolution,
* a way to specify a controller and to check temporal properties by calling Spot.
* the capability to replay (graphically) a counter-example given by Spot.
* the ability to describe the characteristics of the lifts system (number of lifts, ranges etc.)
Such a prototype is intended to be used in the communication of the LRDE, for example during the Journées Portes Ouvertes.
Another module would consist in a game on LTL.
The game picks a LTL formula (at random, or among a list of pre-selected patterns), and displays a corresponding omega-automaton to the player.
The goal is to find the original LTL formula.
When the player makes a wrong guess, the game could help her with traces recognized by the secret formula but not by the player's formula.
This internship targets students who:
* have some experience in Web development and/or C++ and/or Python (conjunction is favored over disjunction)
* would like to get familiar with the amazing world of model-checking
* would like to popularize model-checking and formal methods
true
M2 2017 MC Spot demo
http://spot.lrde.epita.fr
Model checking
Interactive Spot demonstration
Master Internship
en
2018-04-12T14:01:54Z
2458221.0846528
Jobs/M2 2017 MC Spot demo
Jobs/M2 2016 MC Spot demo
0
en
Jobs/M2 2016 MC Spot demo