PhD in France
Offers listWhy France ?F.A.Q.Email AlertsPost an offer

Forgot Password ?
Offer Details

Formal verification of parametric real-time systems with preemption
Université Paris 13, Sorbonne Cité, Villetaneuse
Computer Science and IT Software Engineering Mathematics (applied) 
Full Description:

                        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

*** Full subject available at

 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.

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

Posted on: 27 January 2016Deadline to apply: 01 October 2016Start Date: 01 September 2016 Duration: 36 months
The Fund category is CNRS and the salary is 20-25k€ annual gross
Doctoral School is Sciences, technology, health "galileo" in the Ile-de-France Region.

Please connect to your account to see contact details

Back to offer list

Back to home page

PhD in France Website.
© French Embassy in India, CampusFrance 2014.

Contact us

Related Links