Difference between revisions of "Jobs/M2 2017 MC Spot demo"
From LRDE
(typos) |
|||
Line 6: | Line 6: | ||
|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. |
||
Revision as of 19:23, 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 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 |