Jobs/M2 2017 MC Spot demo

From LRDE

Revision as of 15:41, 28 November 2016 by Max (talk | contribs) (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...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Interactive Spot demonstration
Reference id

M2 2016 MC Spot demo

Dates

5-6 months in 2016

Research field

Model checking

Related project

Spot

Advisor

{{{Advisor}}}

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.

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