Start date: September 2012

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: « Rigorous design of cloud applications using formal methods »

Objectives:

Cloud applications are often complex distributed applications composed of multiple software running on separate virtual machines. Such applications benefit from several services provided in the cloud, like database storage, load balancing, and so on. However, setting up, (re)configuring, and monitoring distributed applications in the cloud is a real burden since a software may depend on several remote software and virtual machine configurations. These management tasks involve many complex protocols, which fully automate them while preserving application consistency. In addition, some of these tasks are executed in parallel and resist failures. These characteristics of the management tasks (full automation, robustness, parallel execution, failure resistance) complicate their development compared to classic software. Therefore, the design of such applications must be very rigorous, requiring the use of formal methods equipped with efficient verification tools.

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 20 years. CADP is dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting via message passing.

ERODS is a new research team of the LIG laboratory, associated with CNRS, Grenoble INP and UJF. The goal of ERODS is to study the construction and the management of cloud systems. Based on large scale environments involving a broad range of multicore servers and end-user devices, cloud computing is defined as the capacity to deliver IT resources and services automatically on demand over the network. The activity of ERODS focuses on the following scientific goals: self-management, by integrating automation within cloud environments, with the intent of providing the controllability of SLA criteria for performance and robustness; distributed runtime support, by providing system support through advanced distributed algorithms, enhanced replication protocols, and extended runtimes to build efficient and robust cloud infrastructures; virtual machine, by collapsing the various virtualization layers of cloud infrastructures (high-level virtual machine, middleware, operating system, and hypervisor) into one modular platform in order to rationalize the overall design, avoid redundancy, improve observability, and increase the end-to-end performances and their controllability.

This PhD thesis 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 aim of this thesis is to contribute to the effort of designing and analyzing the self-deployment and 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:

• Debugging techniques: When a bug is found out by model checking tools, it is identified with a counterexample (a sequence of actions violating the property). This diagnostic can be quite long (up to hundreds or thousands of actions while verifying the reconfiguration protocol), and in this case it is rather complicated to extract the configuration of the system when the error occurs. Similarly to state-based techniques, a direct access to the data expressions state would help debugging. Another issue comes from the lack of parallelism view of the system: the current state of each concurrent process would help to understand what each participant was doing when the error occurred.


• Coverage analysis: 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.
  
  Coverage analysis 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 that 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.


• Model checking and property patterns: Simulation tools (such as step-by-step and guided animation) are simple to use but not powerful enough to find subtle bugs. In contrast, temporal logics and model checking techniques are powerful techniques but not intuitive enough to be used by non-experts. There is a clear need of automated, yet simple tools to analyse LTSs. An idea would be to identify some common properties in autonomic systems in order to propose specific patterns in temporal logics for formalising these properties.


• Dynamicity: Cloud applications running on physical platforms must take into account the presence of failures of equipment and/or loss of data, which require self-management and dynamic reconfiguration. These are highly dynamic phases during which new processes are created, unreachable processes are destroyed, and new communication links are established. The rigorous design of cloud applications must provide features to describe and analyze dynamic systems formally. Regarding the formal description of the dynamic aspects, languages based on mobile process calculi, such as the pi-calculus, are particularly appropriate but difficult to implement and analyze. An expected contribution of the thesis concerns the enhancements of existing tools for applied pi-calculus developed on top of CADP, and their application to the specification and analysis of dynamic cloud applications.

Required skills and profile:

• Good knowledge of compiling and distributed algorithms

• Knowledge of formal methods

• 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 55 11 E-mail : Gwen.Salaun@inria.fr

or

Mr. Noël de Palma Inria Grenoble - Rhône-Alpes / ERODS Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 55 16 E-mail : Noel.dePalma@imag.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 #2012E. Applications received after August 15, 2012 might not be considered if a candidate has been selected already.