Start date: October 1st, 2012

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

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: « Coverage analysis of concurrent specification languages »

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.

CADP accepts different input formats: high level specification languages such as the LOTOS and LOTOS NT process algebras, but also lower level formats such as Labelled Transition Systems (LTSs) and networks of automata. LOTOS NT (LNT for short) is an improved version of the E-LOTOS ISO standard that combines the best features of imperative programming languages and value-passing process algebras. LNT supports both the description of complex data types and of concurrent processes using the same user-friendly syntax. LNT formal operational semantics is defined in terms of LTSs.

In the classic verification setting, we have an LNT specification of a system, a set of temporal properties to be verified on the LTS model corresponding to the LNT specification, and a dataset of examples (test cases) we use for validation purposes. At this stage, building the set of validation examples and debugging the system is a real burden, in particular for non-experts. More precisely here are a few issues that may arise during this phase. First, we do not know whether the set of test cases covers all the possible execution scenarios described in the specification. Second, the LNT specification might be refactored and improved but this cannot be deduced by the counterexamples returned when applying model checking techniques. Third, the set of properties may miss some interesting verification scenarios.

This research project aims at proposing and developing techniques for automatically detecting parts of an LNT specification not (yet) covered during verification. Such LNT coverage analysis techniques would be very helpful for (i) extending the set of test cases with new inputs covering parts of the LNT specification, which have not been analysed yet, (ii) eliminating dead code in the LNT specification, and (iii) extending the set of properties with new formulas. We also plan to develop tool support for automating the coverage analysis. To do so, we will rely on and extend some of the tools available in CADP for compiling LNT into LOTOS and LTS, and exploring the resulting LTS for verification purposes.

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 coverage analysis approach proposed in this project will be used for designing and verifying self-management protocols in cloud computing developed in the context of OpenCloudware.

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

• Study of LNT, CADP tools, state-of-the-art on existing solutions for coverage analysis, e.g., in the white-box testing area, and study of possible solutions

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

• Application of our approach to the cloud computing area in order to validate our new techniques and tools onto state-of-the-art self-management protocols 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 (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 86 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 #2012D. Applications received after July 15st, 2012 might not be considered if a candidate has been selected already.