The CONVECS team of Inria and LIG, and the ERODS team of LIG are
recruiting a PhD student.
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 : [email protected]
and
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 : [email protected]
Application content:
- Letter of application
- Curriculum vitae
- 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.
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
