Beware! This job offer has been fulfilled and is no longer valid.
The CONVECS team of Inria and LIG is recruiting a post-doc fellowship
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 »
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:
Required skills and profile:
All questions concerning this post-doctoral fellowship should be addressed to:
Inria Grenoble - Rhône-Alpes / CONVECS
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
Tel : +33 (0)4 76 61 54 86
E-mail : Gwen.Salaun@inria.fr
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.