Start date: September 1st, 2012

Type of contract: Fixed term contract (CDD) for 3 years.

Salary: About 2137 EUR net per month (2620 EUR gross), health insurance included (French Social Security system).

Location: This post-doctoral fellowship will be carried out at the Inria Montbonnot site, about 10 kilometres from Grenoble.

Subject: « Enhanced equivalence checking for asynchronous systems »

Objectives:

PLC (Programmable logic controllers) are easy-to-use electronic devices that enable the automated control of physical installations, with applications in various domains, such as domotics, water treatment, access control, and small machines to mention only a few. In the last decades, PLC have benefitted from the technological advances of microprocessors and microcontrollers, enabling their price to be reduced and their performances to be increased. Meanwhile, advances in communication systems now enable networks of PLC that communicate with the Internet of things, which opens the way to new applications.

Networks of PLC involve a high degree of asynchronous concurrency, making the applications hard to design and debug. The Inria/CONVECS team develops software tools and techniques based on formal methods for the design and verification of asynchronous concurrent systems, which are packaged in the internationally renowned CADP (Construction and Analysis of Distributed Processes) software toolbox. In this context, the goal of this post-doctoral fellowship is to enhance the equivalence checking verification approach (comparison of abstract and concrete system behaviours modulo various bisimulation relations) by designing and implementing new techniques and experimenting them on realistic examples of PLC networks.

This post-doctoral fellowship will be part of the « Bluesky for I-Automation » collaborative project of the Pôle de compétitivité Minalogic, funded within the 13th call of the French national Fonds unique interministériel. This project is led by Crouzet, the leader of PLC in France. It also involves LCIS (Laboratoire de Conception et d'Intégration des Systèmes, Valence) and the small business companies Mootwin and Vertical M2M.

Work proposed and expected results: The candidate will complete the following tasks, among others:

• Study of state-of-the-art verification techniques for equivalence checking, encompassing compositional, on-the-fly, and distributed techniques.

• Design of new techniques applicable to PLC networks and their implementation using the software components provided by CADP.

• Formal modeling of a PLC network case-study provided within the Bluesky project using the input languages of CADP (LNT, EXP, etc.).

• Experiment the newly developed equivalence checking techniques on the case-study, and fine-tune the performance of verification.

Required skills and profile:

• Good knowledge of formal methods (process algebraic languages)

• Knowledge of explicit-state verification techniques

• Programming skills, development experience is a plus

• Education: PhD in Computer Science

• Good command of English, French is a plus

• Proven communication and interpersonal relationships skills, attention to detail, methodical approach, autonomy, team player

Contacts:

All questions concerning this post-doctoral fellowship should be addressed to:

M. Radu Mateescu Inria Grenoble - Rhône-Alpes / CONVECS Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 54 86 E-mail : Radu.Mateescu@inria.fr

Application content:

• Letter of application

• Curriculum vitæ including the list of publications

• References or letters of recommendation, if any

Application submission:

Applications should be addressed directly to Radu Mateescu, preferably by e-mail, mentioning the position number #2012B. Applications received after July 1st, 2012 might not be considered if a candidate has been selected already.