Jobs/M2 2017 MC Spot demo

	Interactive Spot demonstration
Reference id	M2 2017 MC Spot demo
Dates	5-6 months in 2017
Research field	Model checking
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 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: 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 popularize model-checking and formal methods
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: 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	http://spot.lrde.epita.fr
Place	LRDE: How to get to us
Compensation	1000 € gross / month
Future work opportunities
Contact	<at> lrde.epita.fr colange <at> lrde.epita.fr