Start date: September 1st, 2012

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

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

Location: This thesis project will be carried out at the Inria Montbonnot site, about 10 kilometres from Grenoble.

Subject: « Formal modelling and validation of networks of programmable logic controllers »

Important note: Although the application domain of this thesis is electronics, no background in electronics is required. We seek candidates with a solid formation in computer science, particularly programming and formal methods.

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. The aim of this thesis is to contribute to a development environment for networks of PLC, using features available in CADP to help developing, modelling, simulating, and verifying such systems.

This thesis 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:

• In-depth study of existing work in the field of modelling and formal verification of PLC and programmable automata.

• Definition (syntax and formal semantics) of an asynchronous pivot language for describing the communication and synchronisation between several PLC interconnected in a network, the behaviour of each PLC being itself described in a synchronous pivot language also defined in the Bluesky project.

• Formal definition of a semantic-preserving translation from the asynchronous pivot language into an input language of CADP, namely LNT.

• Definition of a temporal logic specification language adapted to the needs of the application designers, and of a catalogue of generic properties specified in this language.

• Development of an interface enabling networks of PLC modelled in the asynchronous pivot language to be simulated and/or verified. This task will require the translator into LNT to be implemented. It may also require the definition and implementation of simulation and/or verification functionalities not yet available in CADP.

• Application of the above work to a case study provided by Crouzet.

Required skills and profile:

• Good knowledge of compiling and parallel programming

• Knowledge of formal methods

• Education: MSc/Master 2 Recherche 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 thesis project should be addressed to:

M. Frédéric Lang Inria Grenoble - Rhône-Alpes / CONVECS Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 55 11 E-mail : Frederic.Lang@inria.fr

Application content:

• Letter of application

• Curriculum vitæ

• School report

• References or letters of recommendation, if any

• Scientific or technical publications, if any

Application submission:

Applications should be addressed directly to Frédéric Lang, preferably by e-mail, mentioning the position number #2012A. Applications received after July 1st, 2012 might not be considered if a candidate has been selected already.