Difference between revisions of "Jobs/M2 2017 MC Spot demo"
From LRDE
Line 23: | Line 23: | ||
Such a prototype is intended to be used in the communication of the LRDE, for example during the Journées Portes Ouvertes. |
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. |
||
|References=http://spot.lrde.epita.fr |
|References=http://spot.lrde.epita.fr |
||
|Contact=colange@lrde.epita.fr |
|Contact=colange@lrde.epita.fr |
||
Line 28: | Line 33: | ||
|Type=Master Internship |
|Type=Master Internship |
||
|Language=en |
|Language=en |
||
− | |Published= |
+ | |Published=Yes |
}} |
}} |
Revision as of 16:55, 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. 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. |
Benefit for the candidate | |
References | |
Place | LRDE: How to get to us |
Compensation |
1000 € gross / month |
Future work opportunities | |
Contact |