[TYPES/announce] Postdoc position at INRIA Grenoble : Foundations and programming for recoverable embedded systems

[Alain Girault]

		    Proposal for Post-doc Position
		    ==============================

Title
=====

   Foundations and programming for recoverable embedded systems

Team
====

   Spades, Inria Rhone-Alpes, Grenoble
   (http://team.inria.fr/spades)

Supervisors
===========

   Pascal Fradet           Pascal.Fradet at inria.fr
   Jean-Bernard Stefani    Jean-Bernard.Stefani at inria.fr

Starting date and length
========================

16 months post-doc starting imperatively in 2013
ideally around September or October 2013

Abstract
========

Embedded systems are omnipresent today: automotive, electronic
appliances, space, avionics, nuclear... Due to the target domains,
embedded systems are critical and they must be tolerant to failures.
In this project, we are interested in software solutions to implement
fault-tolerance policies in such systems.

Recent works by Bonakdarpour et al. have considered e.g. compositional
design of real-time fault-tolerant (fault-masking) programs and
initiated an analysis of fault recovery in component-based design.  In
parallel, other recent works(e.g., Fradet et al.) have considered how
to automate the construction of real time fault-tolerant programs by
means of program transformations, or the use of aspect-oriented
programing techniques for fault management. Others, (e.g., Bruni et
al. and Lanese et al.) have developed extensive analysis of fault
recovery schemes in Web services which are based on compensations.

However, we currently lack a comprehensive formal framework that
handles the fault-tolerance concerns prevalent in networked embedded
systems. In particular, we are lacking a theory and associated
programming and verification tools dealing with non-masking forms of
fault tolerance such as fault recovery. These techniques are specially
important since fault masking methods such as spatial replication are
often too expensive.

The goal of the postdoc is twofold. First, it will strive to develop a
formal theory of recoverable programs or components. Second, it will
seek to develop programming techniques and tools to aid in the
incremental construction of systems with fault recovery (typically
exploiting program transformations or program weaving techniques).
This study will be conducted at a semantic level (e.g., on labeled
transition systems or formal calculi) in order to consider (and be
applied to) both programs or software components.

Several questions will be worth considering:

- how well can one achieve a true separation of fault-recovery concerns?

- can fault recovery schemes be realized efficiently and modularly as
   superimposed programs?

- how to take into account dynamic component structures?

- what is the relationship between fault recovery schemes in a
   component-based model and compensation studied for Web services?

- can one exploit a reversible programming model as studied by Lanese
   et al. in the design of fault-recovery schemes for component
   systems?

Key-Words
=========

   Fault-tolerance, compensation, embedded systems, weaving, program
   transformation

References
==========

B. Bonakdarpour and S. S. Kulkarni.
Compositional verification of real-time fault-tolerant programs.
In Proceedings of EMSOFT, 2009.

B. Bonakdarpour, M. Bozga, and G. Goessler.
A theory of fault recovery for component-based models.
In 14th Int. Symp. on Stabilization, Safety, and Security of
Distributed Systems (SSS), 2011. LNCS 7596.

T. Ayav, P. Fradet, and A. Girault.
Implementing fault-tolerance in real-time programs by automatic
program transformations.
ACM Trans. Embedded Comput. Syst. 7(4), 2008.

P. Fradet and S. Hong Tuan Ha.
Aspects of availability: Enforcing timed properties to prevent denial
of service.
Sci. Comput. Program., 75(7), 2010.

I. Lanese, C. Vaz, and C. Ferreira.
On the Expressive Power of Primitives for Compensation Handling.
In Proceedings ESOP, 2010. LNCS 6012.

I. Lanese, M. Lienhardt, C.A. Mezzina, J.B. Stefani.
A Reversible Abstract Machine and Its Space Overhead.
In Proceedings FMOODS/FORTE, 2012. LNCS 7273.

Required Skills
===============

The candidate should have a PhD in formal methods (e.g., compilation,
semantics, verification, validation, ...). He should possess a good
background in programming languages, their semantics and
implementation. A good knowledge of formal models for concurrent
computation, real-time and/or embedded systems and/or programming
techniques such as aspect-oriented programming would be a plus.

Context
=======

The SPADES team at INRIA Grenoble conducts research on programming
dependable networked embedded systems. As part of that effort, the
team develops new formal component models, programming languages and
associated tools for verification, analysis or synthesis.