Jobs/M2 2017 MC Spot demo

From LRDE

Revision as of 15:57, 28 November 2016 by Maximilien Colange (talk | contribs)
Interactive Spot demonstration
Reference id

M2 2016 MC Spot demo

Dates

5-6 months in 2016

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 a 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 counter-example).

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 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

colange@lrde.epita.fr