Jobs/M2 2017 MC Spot demo
|Interactive Spot demonstration|
M2 2016 MC Spot demo
5-6 months in 2016
|General presentation of the field||
The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. It also provides support to build a 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 counter-example).
This internship targets students who:
We wish to build an interactive 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.
|Benefit for the candidate|
|Place||LRDE: How to get to us|
1000 € gross / month
|Future work opportunities|