Jobs/M2 2017 MC Spot demo
From LRDE
Interactive Spot demonstration | |
---|---|
Reference id |
M2 2016 MC Spot demo |
Dates |
5-6 months in 2016 |
Research field |
Model checking |
Related project | |
Advisor | |
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 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). |
Prerequisites |
This internship targets students who:
|
Objectives |
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:
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 | |
References | |
Place | LRDE: How to get to us |
Compensation |
1000 € gross / month |
Future work opportunities | |
Contact |