Jobs/M2 2017 MC Spot demo

From LRDE

Revision as of 16:01, 12 April 2018 by Daniela (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Interactive Spot demonstration
Reference id

M2 2017 MC Spot demo

Dates

5-6 months in 2018

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