[robotics-worldwide] [Jobs] PostDoc position: Formal Validation and Verification of Cyber Physical Systems; LAAS, Toulouse, France.

Felix Ingrand felix at laas.fr
Fri Feb 13 06:47:06 PST 2015

PostDoc position: Formal Validation and Verification of Cyber Physical Systems;  LAAS, Toulouse, France. 

                  Formal Validation and Verification of Cyber Physical 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.

We believe that this approach which has been successfully applied to robotics system using GenoM2 and BIP, can be extended to cyber physical systems programmed with GenoM.

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 distributed platform.

The objective of this PostDoc is to pursue the joint GenoM3/BIP effort, within the CPS Engineering Labs H2020 european project, to allow the development of robust and verifiable Cyber Physical Systems components. This will be applied to different platforms, some robotics, but also other Cyber Physical Systems.

Required candidate background:
- PhD in computer science (Validation and Verification and/or Robotics would be a definite plus)
- Software engineering and good programming skills (C/C++)

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

The PostDoc candidate will be mostly based at LAAS (Toulouse), but will make long visits at Verimag (Grenoble) to work jointly with the BIP team. The position is proposed for a duration of 18 to 24 months, starting spring 2015.

Bibliographic references presenting the background of the research topic:

[1]	T. Abdellatif, S. Bensalem, J. Combaz, L. de Silva, and F. Ingrand, “Rigorous design of robot software: A formal component-based approach,” Robotics and Autonomous Systems, 2012.
[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.
[7]	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.

Candidates should send :
- a letter of motivation,
- a resume,
- a copy of their PhD,
- a copy of their major relevant publications,
- recommendation letters,

Send your application to felix at laas.fr and Saddek.Bensalem at imag.fr

More information about the robotics-worldwide mailing list