Difference between revisions of "Jobs/M2 2017 MC Spot demo"
From LRDE
(Created page with "{{Job |Reference id=M2 2016 MC Spot demo |Title=Interactive Spot demonstration |Dates=5-6 months in 2016 |Research field=Model checking |Related project=Spot |General presenta...") |
|||
Line 5: | Line 5: | ||
|Research field=Model checking |
|Research field=Model checking |
||
|Related project=Spot |
|Related project=Spot |
||
+ | |Advisor=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 |
+ | |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). |
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). |
||
Line 12: | Line 13: | ||
* would like to get familiar with the amazing world of model-checking |
* would like to get familiar with the amazing world of model-checking |
||
* would like to popularize model-checking and formal methods |
* would like to popularize model-checking and formal methods |
||
− | |||
|Objectives=We wish to build an interactive demonstration prototype for Spot, to illustrate the interest of model-checking. |
|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 targeted use-case is the verification of a controller for lifts. |
Revision as of 15:45, 28 November 2016
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: - 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 | |
References | |
Place | LRDE: How to get to us |
Compensation |
1000 € gross / month |
Future work opportunities | |
Contact |