Start date: October 2016

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

Salary: About 1300 EUR net per month (without teaching obligations), 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, with periodical visits to the LCIS laboratory and Innovista Sensors in Valence.

Subject: "Formal Methods for Testing Networks of Controllers"

Objectives:

The applications embedded on Programmable Logic Controllers (PLCs) communicating through a network are instances of GALS (Globally Asynchronous, Locally Synchronous) systems, which are increasingly spreading with the development of the Internet of Things (IoT). These applications are numerous, both in industry (automation, control of processes), individuals (home automation), and infrastructures (water and solar panel management). GALS systems are intrinsically complex due to the simultaneous presence of synchronous and asynchronous aspects, which make their development and debugging difficult. Therefore, to ensure the reliability and functional safety of GALS systems, it is necessary to adopt rigorous design methodologies, based on formal methods assisted by efficient validation tools.

The scientific objective of the PhD thesis is to enhance the design flow of a GALS system by integrating the automatic generation of conformance tests from the formal model and the temporal properties used for verifying the system. This yields a double benefit for the designer: on the one hand, it makes possible to check that a physical implementation conforms to the verified model and, on the other hand, the development cost of the model and properties is distributed on the verification and testing phases of the design process, therefore increasing the return on investment.

To reach this objective, we propose to generalize the method for conformance test generation based on the ioco (input-output conformance) relation with test purposes, whose usefulness for asynchronous systems was demonstrated by successful tools like TGV. Starting from a formal model of the system and a test purpose, this method generates automatically a set of test cases to be executed on the physical implementation of the system. Intuitively, a test purpose enables to select the states of the model that must be reached during the execution of the test case on the implementation. The test case generation algorithms explore the model on the fly, handle the nondeterminism and ensure that the test case provides only the inputs allowing to reach the test purpose.

To extend this methodology and make it applicable to industrial GALS systems, it is necessary to tackle several scientific and technical challenges: integrate the testing techniques for synchronous systems in the methodology (initially defined for asynchronous systems); automate as much as possible the specification of test purposes; ensure a good coverage and quality of the generated test cases; and increase the capabilities of the tools to handle complex systems.

The PhD will take place in the CONVECS research project-team of Inria and the LIG laboratory. Its areas of expertise lie on formal verification techniques and tools for asynchronous concurrent systems. CONVECS is involved in several research directions: providing formal specification languages for describing concurrent systems; enhancing temporal logics and verification tools; fighting state explosion; designing generic components for verification, test, and performance evaluation; and demonstrating the applicability of its methods and tools on real-life applications with academic and industrial partnerships. In particular, the members of CONVECS have been developing the CADP verification toolbox for about 25 years. CADP is dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting by message passing.

This PhD thesis will be achieved in collaboration with the CTSYS research team of the LCIS laboratory. The research activities of CTSYS focus on the design of embedded and distributed systems with a strong emphasis on dependability, which is a major issue in applications of high criticality (telecommunications, air transportation, railway, automobile, etc.). The common goal of CTSYS researchers is achieving dependable systems using approaches contributing to the fault elimination, fault tolerance or fault prediction using fault models. Additionnally, CTSYS has skills in embedded system design, especially when systems are subject to severe resource (memory, energy consumption, etc.) or security constraints. There is a wide variety of embedded systems, so approaches developed within CTSYS include distributed systems with low stress, heterogeneous systems including software, digital and analog hardware, or mechanical components.

Work proposed and expected results:

The work proposed in this PhD project is intended to build upon the results of the FUI project Bluesky for I-Automation concerning the validation of applications embedded on networks of em4 controllers produced by Innovista Sensors (previously Crouzet Automation). The GALS systems will be modeled using the GRL language defined in the Bluesky project, which is connected to the em4soft studio of Innovista Sensors, as well as to the CADP verification toolbox of Inria.

The candidate will complete the following tasks, among others:

• Integration of testing methods for synchronous systems into the conformance testing theory for asynchronous systems (high-level description of synchronous aspects by investigating the translation of synchronous programming languages to GRL, derivation of synchronous tests from abstract GRL models representing partially the behaviour of synchronous subsystems).


• Generalization of the test generation algorithms to handle GALS systems (extension of test purposes to capture synchronous aspects, data and behaviour, on-the-fly generation of controllable test cases, new distributed test generation algorithms running on computer grids, automatic derivation of test purposes from temporal logic properties).


• Validation of the obtained methodology on industrial case studies, provided in particular by Innovista Sensors.

Required skills and profile:

• Knowledge of formal methods (synchronous and/or asynchronous settings), verification, and testing

• Knowledge of embedded systems is a plus

• Good programming skills and motivation for software development

• 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:

Mr. 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

Mr. Ioannis Parissis LCIS / CTSYS 50, rue Barthélémy de Laffemas BP 54 26902 Valence Tel : +33 (0)4 75 75 93 91 E-mail : Ioannis.Parissis@grenoble-inp.fr

Application content:

• Letter of application

• Curriculum vitae

• School report

• References or letters of recommendation, if any

• Scientific or technical publications, if any

Application submission:

Applications should be addressed directly to Radu Mateescu and Ioannis Parissis, preferably by e-mail, mentioning the position number #2016C. Applications received after July 15, 2016 might not be considered if a candidate has been selected already.