************************************************************
PhD position
Title : Formal verification of parametric real-time systems with preemption
Laboratory 1: LIPN, CNRS UMR 7030, Université Paris 13, Sorbonne Paris Cité, France
Laboratory 2: IRCCyN, École Centrale Nantes, France
Contact : Étienne André and Didier Lime
application.phd.pacs@lipn.univ-paris13.fr
************************************************************
*** Full subject available at
https://lipn.univ-paris13.fr/~andre/sujets/2016-PhD-PACS.pdf
************************************************************
Context of the subject
************************************************************
Real-time systems have become ubiquitous in the past few years.
Some of them (automated plane and unmanned systems control, banking systems, etc.) are critical in the sense that no error must occur.
Testing these systems can possibly detect the presence of bugs, but not guarantee their absence.
It is thus necessary to use formal methods such as model checking so as to formally prove their correctness.
Real-time systems are characterized by a set of timing constants, such as the reading period of a sensor on an unmanned aircraft system, the traversal time of a circuit by the electric current, or the delay before retransmitting data in a cellphone.
Although numerous techniques to verify a system for one set of constants exist, formally verifying the system for numerous values of these constants can require a very long time, or even infinite if one aims at verifying dense sets of values.
It is therefore interesting to use parameterized techniques, by considering that these constants are unknown, i.e. parameters, and synthesize a constraint on these parameters guaranteeing the system correctness.
Parametric timed automata have been proposed to model and verify parametric timed systems, and tools such as Romeo and IMITATOR were developed to perform efficient analyses.
This formalism extends finite state automata with clocks (real-valued variables) that are compared with parameters in linear inequalities.
Parameter synthesis can also be used to study the "implementability" of a system, i.e. its robustness w.r.t. infinitesimal variations of the timing constants.
The goal of this PhD is to:
1) study parameter synthesis for parametric timed automata and hybrid systems;
2) devise efficient algorithms reusing recent concepts such as the integer hulls;
3) implement all algorithms in state-of-the art tools.
Keywords:
Formal methods, model checking, real-time systems, parameter synthesis
One or several of the following skills would be appreciated (though not compulsory):
- formal methods;
- model checking;
- (parametric) timed automata, (parametric / timed) Petri nets;
- C++ or OCaml programming.
************************************************************
Context: The PACS Project
************************************************************
This post-doctoral position is funded by national project ANR PACS (Parametric Analyses of Concurrent Systems) 2014--2019.
ANR PACS involves four laboratories: LIPN (Paris 13), IRIF (Paris 7), IRCCyN (École Centrale Nantes) and LINA (Université de Nantes).
In addition, Kim Larsen's group in Aalborg (Denmark) acts as a foreign partner.
LIPN is a high-quality laboratory involving about 80 professors, associate professors and full-time researchers, and many more students.
Université Paris 13 is located less than 30 minutes from central Paris.
IRCCyN is a leading laboratory in the domain of cyber-physical systems and robotics, with about a hundred researchers. It is located in Nantes, on the west coast of France, two hours from Paris by a direct, high-speed train.
************************************************************
Conditions and Application
************************************************************
The PhD position is for three years, and can start anytime (the sooner the better), and in any case before October 1st, 2016.
The monthly salary is 1400€ + an additional 250€ if teaching 64h/year (netto, but before income tax, about 5,5%).
Local transportation fees (Paris métro) are subsidized by half by the employer.
Applications shall be made by email to Didier Lime and Étienne André, enclosing a fully detailed curriculum, and any other relevant document (recommendations, etc.).
Contact : Étienne André and Didier Lime
application.phd.pacs@lipn.univ-paris13.fr