[robotics-worldwide] PhD Student position and scholarship "Formal Validation and Verification of Robotic Systems", Verimag Grenoble and LAAS/CNRS Toulouse, France

Felix Ingrand felix at laas.fr
Fri Jun 8 00:51:17 PDT 2012

A PhD Scholarship in the area of "Formal Validation and Verification of Robotic Systems" 
is being offered jointly at Verimag, Grenoble and LAAS-CNRS, Toulouse, for the fall 2012,
under the joint supervision of Saddek Bensalem and Felix Ingrand.
Application deadline: July 31

Formal Validation and Verification of Robotic Systems

Verimag and LAAS started a few years ago an effort to provide a framework to deploy robust and formally verifiable robotics software. They combined a state of the art tool for developing functional modules of robotic systems (GenoM) with a component based framework for implementing embedded real-time systems (BIP).  Over the years, they have successfully developed a first version of the GenoM/BIP component based design approach and applied it to the functional level of a complex exploration rover. This original approach allows to :
- produce a very fine grained formal computational model of the robot functional level; 
- run the BIP engine on the real robot, which executes and enforces the model semantics at runtime; and 
- check the model offline for deadlock freedom, as well as other safety properties using tools such as D-Finder.

The latest evolution of GenoM (GenoM3) is templates based, and while retaining the "codels", execution automata organization to implement functional module services and posters, it allows now to produce modules for different robotics middlewares (CSlib, ROS Com, etc). In parallel, recent evolutions of the BIP framework and toolset allow the use of timed models and models distribution over more than one CPU, and provide a realtime BIP Engine which is able to execute these models on the targeted platform.

The objective of this PhD is to pursue the joint GenoM/BIP effort to allow the development of robust and verifiable functional layer for robots, as well as to study the extensions of this approach toward the decisional level of the robot (planning/supervision). This will be applied to different platforms, in particular on a PR2 (Willow Garage) robot at LAAS but also on a fleet of UAV each running its own GenoM/BIP model, with execution coordination (performed in BIP) among them. 

Required candidate background:
- major in computer science
- software engineering and good programming skills (C/C++)

Background knowledge in the following areas would be a plus.
- robot programming (fluency with tools like ROS, GenoM, Orocos, BCM, etc would be a plus)
- formal methods for validation and verification

The PhD candidate will be mostly based at Verimag in Grenoble, but will make long visits (few months each year) at LAAS (Toulouse) to implement and test its work on the various robotic platforms (PR2, UAV, etc).

Bibliographic references presenting the background of the subject:

[1]	S. Bensalem, M. Bozga, T.-H. Nguyen, and J. Sifakis, “D-finder: A tool for compositional deadlock detection and verification,” Computer Aided Verification, no. Grenoble, France, 2009.
[2]	S. Bensalem, M. Gallien, F. Ingrand, I. Kahloul, and T.-H. Nguyen, “Toward a More Dependable Software Architecture for Autonomous Robots,” Robotics & Automation Magazine, IEEE, vol. 16, no. 1, pp. 67–77, 2009.
[3]	S. Bensalem, M. Bozga, T.-H. Nguyen, and J. Sifakis, “Compositional verification for component-based systems and application,” Software, IET, vol. 4, no. 3, pp. 181–193, 2010.
[4]	S. Bensalem, L. de Silva, A. Griesmayer, F. Ingrand, A. Legay, and R. Yan, “A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems,” Software Composition, pp. 116–132, 2011.
[5]	S. Bensalem, L. de Silva, F. Ingrand, and R. Yan, “A Verifiable and Correct-by-Construction Controller for Robot Functional Levels,” Journal of Software Engineering for Robotics, vol. 1, no. 2, pp. 1–19, Sep. 2011.
[6]	A. Mallet, C. Pasteur, M. Herrb, S. Lemaignan, and F. Ingrand, “GenoM3: Building middleware-independent robotic components,” presented at the Robotics and Automation (ICRA), 2010 IEEE International Conference on, 2010, pp. 4627–4632.

PhD candidates should send :
- a letter of motivation,
- a resume,
- grades of their master and a copy of their master thesis (pdf),
- recommendation letters,

to felix at laas.fr and saddelk.bensalem at imag.fr before 31/07/2012

Start date of the PhD, fall 2012. Duration 3 years.

Scholarship : 1700 € gross, 1370 € net


Felix Ingrand and Saddek Bensalem

More information about the robotics-worldwide mailing list