Difference between revisions of "Jobs/M2 2017 MC Spot demo"
From LRDE
(4 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
{{Job |
{{Job |
||
− | |Reference id=M2 |
+ | |Reference id=M2 2017 MC Spot demo |
|Title=Interactive Spot demonstration |
|Title=Interactive Spot demonstration |
||
− | |Dates=5-6 months in |
+ | |Dates=5-6 months in 2018 |
|Research field=Model checking |
|Research field=Model checking |
||
|Related project=Spot |
|Related project=Spot |
||
|Advisor=Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange |
|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 omega-automata, and to simplify these formulas and automata. It also provides support to build |
+ | |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 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 |
+ | 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). |
|Prerequisites=This internship targets students who: |
|Prerequisites=This internship targets students who: |
||
* have some experience in Web development and/or C++ and/or Python (conjunction is favored over disjunction) |
* 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 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 |
+ | |Objectives=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 targeted use-case is the verification of a controller for lifts. |
||
The prototype should provide several functionalities, among which: |
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. |
Such a prototype is intended to be used in the communication of the LRDE, for example during the Journées Portes Ouvertes. |
||
Line 30: | Line 30: | ||
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. |
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 |
+ | |Contact=colange <at> lrde.epita.fr |
|Compensation=1000 € gross / month |
|Compensation=1000 € gross / month |
||
|Type=Master Internship |
|Type=Master Internship |
Latest revision as of 16:01, 12 April 2018
Interactive Spot demonstration | |
---|---|
Reference id |
M2 2017 MC Spot demo |
Dates |
5-6 months in 2018 |
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 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). |
Prerequisites |
This internship targets students who:
|
Objectives |
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:
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 |