[TYPES/announce] Multiple Postdoc Positions

[Uli Fahrenberg]

Inria Rennes offers the three following postdoc positions. Inria is
Public science and technology institution established in 1967, Inria
is the only public research body fully dedicated to computational
sciences. Combining computer sciences with mathematics, Inria's 3,400
researchers strive to invent the digital technologies of the future.

The postdoc will work in the ESTASYS team located at Inria
Rennes. ESTASYS is a newly established Inria team concerned with the
rigorous design of systems of systems (e.g. cloud computing, cyber
physical systems, smart buildings, ...). To this purpose, the team
conducts research in component-based design, modelisation of
dynamicity, formal verification and simulation, quantitative systems,
and testing.  The team members are particularly focused on lifting
their technology to industry (collaborators: Thalès, IBM, EADS,
...). The latter is done via the Plasma toolset (see
https://project.inria.fr/plasma-lab/). Plasma implements several
statistical model checking algorithms (procedures that monitor many
executions of a system and then use statistical techniques to obtain a
global confidence) as well as (experimental) compilers from high level
languages (C, UML) to formal models (hence lifting verification
techniques to the real world).

Contact: Axel Legay (axel.legay at inria.fr)

POSITION 1: Statistical Model Checking for Energy Centric Systems
******************************************************************

The objective of this postdoc is to initiate the development of an
exciting new generation of statistical model checking techniques to
reason on systems whose behaviors rely on energy constraints. The long
term objective being to help engineers to develop systems that respect
human and social constraints (security, efficiency, privacy,
reliability, ...) and are also respectful of the environment. For
doing so, the postdoc will propose new Statistical Model Checking
(SMC) algorithms to solve energy problems. This includes reliability
and safety questions ("does my system achieves this objectives with
this amount of energy"), quantitative questions ("what is the minimal
amount of energy to achieve this objective?"), and optimization
questions ("how to optimize cost-production ?"). This work requires
(1) to exploit new statistical algorithms (Anova, CUSUM, ...), and (2)
to develop new monitoring techniques to cope efficiently with aspects
of dynamicity. The work willl be implemented in the Plasma toolset (in
collaboration with engineers from the team) and applied to case
studies coming from the cloud computing and cyber physical systems
area (each of them being furnished by our industry
collaborators). This is a collaborative work with one PhD student and
one engineer within the EU project SENSATION
(http://www.sensation-project.eu/).

Duration: One year. Can be renewed once.

Criteria: PhD in Computer Science or Mathematics. Background in model
checking and basic knwoledge of mathematics and C/Java languages.

Scientific advisors: Axel Legay (CR1 Inria):
http://people.irisa.fr/Axel.Legay/ (list of publications related to
the project) and Sean Sedwards (Expert Engineer Inria):
http://people.irisa.fr/Sean.Sedwards/


POSITION 2: WCET/WCRT analysis using Statistical/Symbolic Model Checking
*************************************************************************

Inria Rennes (France) will open a new postdoc position on
investiguating the use of Statistical Model Checking and Symbolic
Model Checking for WCET/WCRT analysis of mixed critical systems. This
work is part of the EMC2 project funded by the ARTEMIS Scheme.

Location: Inria Rennes, ESTASYS team.

Duration: This is a one year position, which can be renewed once.

Start date: First of July 2014

Profil: Good knowledge of model checking and of C/Java language.

Contact: Axel Legay <axel.legay at inria.fr>

POSITION 3: New formal models for Systems of Systems
*****************************************************

The objective of this postdoc is to participate to the development of
an exciting new generation of formal models and model checking
techniques to reason on Systems of Systems (SoS) whose behaviors rely
on energy constraints. The long term objective being to help engineers
to develop systems that respect human and social constraints
(security, efficiency, privacy, reliability, ...) and are also
respectful of the environment.

In line with this objective, the postdoc will first challenge the
difficult task of finding relevant formal models for SoS and SoS
components. For doing so the postdoc will extends the automata-based
interface models (used to represent component's behaviors) proposed by
the ESTASYS team with dynamicity aspects and energy costs. This new
model will allow to represent the visible behaviors of complex
components of an SoS as well as their interactions.  Aside from
dealing with costs, two difficulties here will be to characterize the
dynamic interactions (composition) between potentially unknown
components, and to capture the hierarchy between them. One suggestion
will be to work with constraints and context free information on the
transitions in a CSP like fashion.

One of the major difficulties with SoS is that the behavior of some of
the components and the environment behavior can only be characterized
at runtime. However, having as much as possible information on those
entities when performing verification is crucial to help the engineer
to predict changes in system's evolution. To obtain this information,
the postdoc will explore the application/extension of automata-based
learning techniques that will be used to incrementally obtain partial
information on the unknown entities, and represent this information
with the interface model defined above.

In a last step, in collaboration with another postdoc from ESTASYS,
the postdoc will propose simulation and monitoring techniques for the
new model, hence making statistical model checking available as a
verification technique for this framework. Here the main challenge
shall be to avoid the overheads that appears at runtime when
monitoring several components (each of them requiring )

The work will be implemented in the Plasma toolset (in collaboration
with engineers from the team) and applied to case studies coming from
the cloud computing and cyber physical systems area (each of them
being furnished by our industry collaborators). This is a
collaborative work with one PhD student and one engineer.

Duration: This is a one year position, which can be renewed once.

Start date: immediatly

Profil: Good knowledge of model checking and of C/Java language.

Contact: Axel Legay <axel.legay at inria.fr>