Difference between revisions of "Jobs/M2 2017 MC Spot demo"

From LRDE

(Created page with "{{Job |Reference id=M2 2016 MC Spot demo |Title=Interactive Spot demonstration |Dates=5-6 months in 2016 |Research field=Model checking |Related project=Spot |General presenta...")
 
Line 5: Line 5:
 
|Research field=Model checking
 
|Research field=Model checking
 
|Related project=Spot
 
|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 Büchi 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.
+
|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).
 
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).
Line 12: Line 13:
 
* 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-checking.
 
|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 targeted use-case is the verification of a controller for lifts.

Revision as of 15:45, 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

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.

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