[robotics-worldwide] Two postdoc positions (2 years) LAAS and Verimag : Toward a validated and verifiable architecture for autonomous robots

Felix Ingrand felix at laas.fr
Tue Mar 17 06:55:35 PDT 2009

Two Post-doctoral positions at LAAS-CNRS and Verimag,

Title: Toward a validated and verifiable architecture for autonomous  


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.  

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,  

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)

Félix Ingrand (felix at laas.fr) Phone: +33 5 61 33 78 04
7 avenue du Colonel Roche
31077 Toulouse Cedex 4, France

Saddek Bensalem (saddek.bensalem at imag.fr) Phone: +33 4 56 52 03 71
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).

More information about the robotics-worldwide mailing list