Start date: October 2015

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: « Debugging Concurrent Programs using Model Checking and Mining Techniques »

Objectives:

Recent computing trends promote the development of hardware and software applications that are intrinsically parallel, distributed, and concurrent. Designing and developing such systems has always been a tedious and error-prone task, and the ever increasing system complexity is making matters even worse. Although we are still far from proposing techniques and tools avoiding the existence of bugs in a system under development, we know how to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually.

Model checking is an established technique for automatically verifying that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level specification languages (such as process algebras) satisfies a given temporal property, e.g., the absence of deadlocks. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds (even thousands) of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not give any clue on the state of the system (e.g., parallelism or data expressions) when the error occurs.

The objective of this project is to propose and develop new solutions for simplifying the comprehension of counterexamples and thus favouring usability of model checking techniques. To do so, we would like to apply pattern mining techniques to a set of correct traces (extracted from the LTS) and incorrect traces (corresponding to counterexamples), to identify specific patterns indicating more precisely the source of the problem.

CONVECS is a research 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 partnership. 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 via message passing.

This PhD thesis will be achieved in collaboration with the SLIDE research team of the LIG laboratory. SLIDE aims at combining efficient large-scale data processing with pattern mining algorithms to extract value from data. SLIDE's research is data-driven and the team develops algorithms and infrastructures for large-scale analytics, data linkage and ontology-based data access, crowd data sourcing and crowdsourced application evaluation. Working at the intersection of knowledge representation and reasoning, data mining, and data management, SLIDE operates on a variety of application domains such as the semantic and social Web, Health and well-being, Data center monitoring, and embedded systems.

Work proposed and expected results:

The candidate will complete the following tasks, among others:

• Formal models and languages: Start by studying the languages (LNT, MCL) and models (LTS) developed in the CONVECS team. At a later stage, study also other kinds of models (e.g., allowing symbolic data manipulation, quantitative time as in timed automata, etc.).


• Trace extraction: Propose automated techniques for generating finite traces from the models considered.
  
  
• Mining algorithms: Improve existing algorithms for detecting interrupted subsequences and patterns by, e.g., parameterizing these algorithms with a set of meaningful actions or measuring the degree of relevance of the results.


• Methodology: Apply trace extraction and mining algorithms iteratively in an automatic way by using the degree of relevance provided by the mining algorithms and updating the set of input traces accordingly.


• Tool support: Develop new tools for supporting all the steps of the approach. This will be achieved by a combination of mining algorithms on the one hand, and of verification compilers and tools on the other.


• Case studies: Apply the approach to the verification of concrete industrial applications, particularly hardware systems and autonomic management protocols for cloud applications.

Required skills and profile:

• Knowledge of data management and data mining

• Knowledge of formal methods (concurrency theory) and verification is a plus

• Candidates who enjoy programming would be appreciated, as the work is likely to include 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. 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æ

• School report

• References or letters of recommendation, if any

• Scientific or technical publications, if any

Application submission:

Applications should be addressed directly to Gwen Salaün, preferably by e-mail, mentioning the position number #2015A. Applications received after July 8, 2015 might not be considered if a candidate has been selected already.