Title: A Faithful Execution Engine for Autonomous Systems
Keywords: robotic software; embedded systems; formal verification; real-time operating systems
This PhD thesis will be a Cifre fellowship. CIFRE stands for Industrial Agreement of Training through Research (Conventions Industrielles de Formation par la REcherche). The CIFRE fellow signs a 3 years full time work contract with a French company and a public laboratory. During the thesis, the fellow works in the company as well as the laboratory.
The design of complex real-time systems requires the use of specific tool chains in order to ensure that the expected behavior and properties of a system are retained throughout the development phases. This means that, ultimately, the behavior of the code running on a target platform should be faithful to the semantics that developers had in mind when they described their system. This generally requires the use of a dedicated execution engine to run the code, that is a software system in charge of mediating the interactions between higher-level components—such as data processing or task planning—and low-level hardware devices.
The goal of this PhD thesis is to generate embedded code automatically from a formally verified high-level model of the applications. The code will target the real-time software platform selected by the company and we will focus on methods that allow to generate code along with guarantees of high level functional properties which can be independently verified.
The proposed work will be carried out within an interdisciplinary team at LAAS and will benefit from our expertise in the different domains covered in this project, including research on autonomous mobile robots (in the RIS team, https://urldefense.proofpoint.com/v2/url?u=https-3A__www.laas.fr_public_en_ris&d=DwIFaQ&c=clK7kQUTWtAVEOVIgvi0NU5BOUHhpN0H8p7CSfnc_gI&r=0w3solp5fswiyWF2RL6rStC00sfV_qVWqlcnmGhKrRoTMim5rLso-FTzVW2NfNyo&m=b2GLApxpNCgoSiI3A9XvkzcqCL_aJhH-fFqgSgP0ex4&s=jVxi1cPu_Dll4mDbPkBgMJNXGK9ppovHVVyX-DuLgoA&e= ) as well as research on the formal verification of real time systems (in the VERTICS team, https://urldefense.proofpoint.com/v2/url?u=https-3A__www.laas.fr_public_en_vertics&d=DwIFaQ&c=clK7kQUTWtAVEOVIgvi0NU5BOUHhpN0H8p7CSfnc_gI&r=0w3solp5fswiyWF2RL6rStC00sfV_qVWqlcnmGhKrRoTMim5rLso-FTzVW2NfNyo&m=b2GLApxpNCgoSiI3A9XvkzcqCL_aJhH-fFqgSgP0ex4&s=bH3BY6ExFV79Ts0WIYM_nmhPegTio5S5JGjunpgkUYs&e= ). We expect that the results of this project will contribute very valuable tools that could be of great impact when building future mobile autonomous applications, where vehicle and other autonomous systems need to be deployed in contact with human environments (autonomous cars, coworker robots, surgery robotics, etc.). Indeed, in this context, trust in the underlying execution engine is of paramount importance.
The objective of this thesis is to participate to the conception and the implementation of an execution engine for a high-level language inspired by GenoM3 , a component-based language dedicated to programming complex on-board systems, such as mobile robots. GenoM3 provides also a methodology that eases the control of robotic modules, the communication between these modules, and enables their rigorous validation. In particular, GenoM3 can be connected to formal verification tools, such as the formal language Fiacre  and the real-time model-checkers Tina, that is also being developed at LAAS (see ). The idea, in this research project, is to build upon this connection between the high-level language and a formal specification language in order to implement a “faithful” execution engine that should preserve the semantics and real-time constraints.
*** IMPORTANT: if you contact us to apply for this Thesis, your message should include at least one paragraph of text explaining why your profile matches the description given in the "Skills and qualifications" section below. ***
Objectives: The student will collaborate with the researchers that have been driving these works. The proposed work includes:
• Extend GenoM to a Domain Specific Language (DSL) for the automotive domain,
• Adapt the execution engine to the dedicated platform,
• Demonstrate compliance of the execution engine with the real-time semantics of the DSL,
• Extend the support for asynchronous events and the management of external data,
• Evaluate different possible implementation strategies with respect to performance.
To demonstrate the feasibility and performance of the implementation, a case study will be developed in the field of autonomous vehicle.
Skills and qualifications: the successful candidate should have at least some partial knowledge of the following topics,
• A basic scientific culture in formal methods (automata, Petri nets, etc.) and real-time systems.
• C / C ++ programming skills and systems programming (if possible with real-time OS).
• Be autonomous and have a strong ability to work in teams.
 Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., Mallet, A. Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. In Proc. of ICFEM 2016, LNCS 10009.
 Mallet, A., Pasteur, C., Herrb, M., Lemaignan, S., Ingrand, F.: GenoM3: building middleware-independent robotic components. In: IEEE ICRA, 2010.
 Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: Fiacre: an intermediate language for model verification in the topcased environment. In Proc. of ERTS, 2008.
You can apply for this PhD at the following web site:
https://urldefense.proofpoint.com/v2/url?u=https-3A__app.laas.fr_boreal_web_fr_utilisateur_voir_these_afficher_183&d=DwIFaQ&c=clK7kQUTWtAVEOVIgvi0NU5BOUHhpN0H8p7CSfnc_gI&r=0w3solp5fswiyWF2RL6rStC00sfV_qVWqlcnmGhKrRoTMim5rLso-FTzVW2NfNyo&m=b2GLApxpNCgoSiI3A9XvkzcqCL_aJhH-fFqgSgP0ex4&s=0f7juqEHvAOYt0Zb8MNxdkL8tbTH1bg_DVogzpdfsdU&e= <https://urldefense.proofpoint.com/v2/url?u=https-3A__app.laas.fr_boreal_web_fr_utilisateur_voir_these_afficher_183&d=DwIFaQ&c=clK7kQUTWtAVEOVIgvi0NU5BOUHhpN0H8p7CSfnc_gI&r=0w3solp5fswiyWF2RL6rStC00sfV_qVWqlcnmGhKrRoTMim5rLso-FTzVW2NfNyo&m=b2GLApxpNCgoSiI3A9XvkzcqCL_aJhH-fFqgSgP0ex4&s=0f7juqEHvAOYt0Zb8MNxdkL8tbTH1bg_DVogzpdfsdU&e= >
If you have further question, you can contact: Félix Ingrand <[hidden email]>, Pierre-Emmanuel Hladik <[hidden email]>, Bernard Berthomieu <[hidden email]>, Silvano Dal Zilio <[hidden email]>
robotics-worldwide mailing list
|Free forum by Nabble||Edit this page|