[Caml-list] PhD position on formal verification at Université Paris 13 / École Centrale Nantes (France)

[Caml-list] PhD position on formal verification at Université Paris 13 / École Centrale Nantes (France)

[Étienne André]

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