Start date: January 1st, 2015

Type of contract: Fixed term contract (CDD) for 12 months.

Salary: About 2127 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: « Verification of Asynchronously Communicating Systems »

Objectives:

CONVECS is a research team of Inria and LIG. 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 partnership. In particular, the members of CONVECS have been developing the CADP verification toolbox for about 20 years. CADP is dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting via message passing.

Recent software is mostly constructed by reusing and composing existing components. Software components are usually stateful and therefore described using behavioral models such as finite state machines. Asynchronous communication is a classic interaction mechanism used for such software systems. However, analyzing communicating systems interacting asynchronously via reliable FIFO buffers is an undecidable problem. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing buffer sizes.

In this line of work, we focus on infinite systems and we do not restrict the system by imposing any arbitrary bounds. We introduced recently a notion of stability and proved that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables us to check certain properties on the system for that bound and to ensure that the system will preserve them whatever larger bounds are used for buffers. We also proved that computing this bound is undecidable but we are able to compute these bounds for many typical examples using heuristics and equivalence checking. The candidate will have to refine these results focusing on the perspectives of this work, to develop the corresponding tool support, and to apply these results to existing areas (e.g., cloud computing).

This post-doctoral fellowship will be part of the « OpenCloudware » project funded by the FSN (Fonds national pour la Société Numérique). The project is led by France Telecom / Orange Labs (Meylan, France) and involves 18 partners (among which Bull, Ow2, Thalès, Inria, etc.). OpenCloudware aims at providing an open software platform enabling the development, deployment, and administration of cloud applications. The verification techniques proposed in this project will be used for analyzing cloud applications developed in the context of OpenCloudware.

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

• Study of the state of the art on verification techniques for systems interacting asynchronously via communication buffers

• Development of the devised solution, implementation of tools supporting the approach

• Application and validation of our approach on to real-world applications developed by our partners from UJF and Orange labs

• Publication of these results into international conferences and journals

Required skills and profile:

• Knowledge of formal methods, in particular description languages for concurrent systems (process algebraic languages)

• Knowledge of explicit-state verification techniques

• Candidates who enjoy programming would be appreciated, as the work is likely to include software development

• Education: PhD in Computer Science

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

Gwen Salaün Inria Grenoble - Rhône-Alpes / CONVECS Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 54 28 E-mail : Gwen.Salaun@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 Gwen Salaün, preferably by e-mail, mentioning the position number #2014B. Applications received after October 10th, 2014 might not be considered if a candidate has been selected already.