Title: Toward a validated and verifiable architecture for autonomous robots

Subject:

In recent years, LAAS and VERIMAG have joined their know-how and efforts to develop a new architecture methodology which embed some formal verification techniques and enable the synthesis of robot controller which are correct by construction. This new methodology relies on two paradigms. On one side, the VERIMAG BIP component based design approach which allows the deployment of embedded real-time systems and one the other side the LAAS architecture and its development tools : in particular GenoM, which lays down an open framework where one can harness the BIP approach.

BIP is a software framework for modeling heterogeneous real-time components. The BIP component model is the superposition of three layers: the lower layer describes the behavior of a component as a set of transitions (i.e. a finite state automaton extended with data); the intermediate layer includes connectors describing the interactions between transitions of the layer underneath; the upper layer consists of a set of priority rules used to describe scheduling policies for interactions. Such a layering offers a clear separation between component behavior and structure of a system (interactions and priorities). From a BIP model, one can synthesize a controller which is "correct by construction", and associated with the BIP engine, will only fire and run the valid interaction in the system. The obtained BIP model can also be used off-line to check general safety properties by computing behaviors and interactions invariants.

The LAAS/GenoM methodology is based on the encapsulation of each basic functionality of the robot in a module. All these modules are built by instantiating a unique generic canvas. Each module is specified by providing the following information: the internal functional data structure (IfDS), the list of services (started with requests) provided by this module, the list of posters (if any) exported by this module and the list of execution tasks with their respective activation period.

As a first step, we have already combined the two approaches and are now able to synthesize a complete BIP controller of the functional level of an exploration rover (DALA, an iRobot ATRV) [Bensalem et al. 09].

Our goals are now to:
- improve the current GenoM/BIP integration in the following directions:
    + development of a real-time BIP Engine
    + development of a distributed BIP Engine
    + development of a high level "langage" to specify and check properties in the BIP model
- develop the use of BIP at a higher level in the robot architecture (deliberation layer):
    + model of the supervision component
    + model of the planning/plan execution component
    + model of the situations recognition component.
- develop of an abstracted functional representation to integrate functional components written with other frameworks

Each of these research venues will be both examined and studied at VERIMAG from the V&V point of view and at LAAS from the robotics point of view.

Hence we are looking for two postdocs (one for each site) for 2 years each. The postdoc whose background will be closer to robotics will be at LAAS, and the one whose background is more in the V&V field will be at Verimag. Both postdocs will do cross regular visits at the other places and will take part in a number of projects related to this research topics.

Requirements: PhD in a related field (embedded real time system, robot control architecture, temporal planning with contraint based approach, model based software architecture, formal validation and verification, etc).


Starting date: Spring 2009
Duration: 2 years

Applicants should send:
- a resume/bio
- pointers to their most important publications and/or their PhD (French or English documents)
- recommendation letter(s)

Contacts:
Félix Ingrand (felix@laas.fr) Phone: +33 5 61 33 78 04
LAAS-CNRS, RIS group
7 avenue du Colonel Roche
31077 Toulouse Cedex 4, France

Saddek Bensalem (saddek.bensalem@imag.fr) Phone: +33 4 56 52 03 71
VERIMAG
Centre Équation - 2, avenue de Vignate
38610 GIÈRES

Salary: 2500 Euros/month

[Bensalem et al. 09] Toward a More Dependable Software Architecture for Autonomous Robots
Saddek Bensalem, Matthieu Gallien, Félix Ingrand, Imen Kahloul and Thanh-Hung Nguyen
Special issue on Software Engineering for Robotics of the IEEE Robotics and Automation Magazine (March 2009).