Jobs/M2 2017 MC Spot demo
From LRDE
Interactive Spot demonstration  

Reference id 
M2 2017 MC Spot demo 
Dates 
56 months in 2018 
Research field 
Model checking 
Related project  
Advisor 
Alexandre DuretLutz, É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 omegaautomata, 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 modelchecking 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, webbased demonstration prototype for Spot, to illustrate the interest of model checking. The targeted usecase 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 
colange <at> lrde.epita.fr 