2020-02722 - PhD Position F/M Formal Modelling and Validation for Electric, Connected, and Automated Vehicles
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Autre diplôme apprécié : Master recherche

Fonction : Doctorant

Niveau d'expérience souhaité : Jeune diplômé

Contexte et atouts du poste

Within the framework of a partnership

  • PhD thesis funded by the EU project ArchitectECA2030 (2020-2023), led by Infineon AG (Germany).

Mission confiée

Vehicle automation is nowadays emerging in many forms and automation comes with many social implications. In order to take full advantage of automation, electric, connected and automated (ECA) vehicles need to be trustworthy. Consequently, there is a strong need for an independent and reproducible validation of automated vehicles even in presence of nondeterministic elements. Independent validation is fundamental to emphasise the capability and safety of any solution in the ECA vehicles space. It is vital that appropriate and audited testing takes place in a controlled environment before any deployment takes place. As the software and hardware components come from multiple vendors and integrate in numerous ways, the various levels of validation required must be fully understood and integration with primary and secondary parts must be considered.

The EU ArchitectECA2030 project aims at implementing a unique in-vehicle monitoring device able to measure the health status and degradation of the functional electronics empowering model-based safety prediction, fault diagnosis, and anomaly detection. A validation framework comprised of harmonized methods and tools able to handle quantification of residual risks using data different sources (e.g. monitoring devices, sensor/actuators, fleet observations) is provided to ultimately design safe, secure, and reliable ECA vehicles with a well-defined, quantified, and acceptable residual risk across all levels of electronic components and systems (ECS). The proposed methods include automatic built-in safety measures in the electronic circuit design, accelerated testing, residual risk quantification, virtual validation, and multi-physical and stochastic simulations.

The goal of this PhD thesis is to apply formal methods for studying the failure modes, fault detection capabilities, and residual risks in the actuators, propulsion systems, and connectivity systems of ECAs. This comprises a formalization of the requirements for fault detection using qualitative and quantitative properties interpretable on behavioural models of tasks and applications. The behavioural models will be exploited to generate automatically high-coverage test suites by means of advanced conformance testing techniques. Quantitative extensions of these models will be exploited to quantify and analyse risk propagation. Finally, formal modelling and validation techniques (model checking, test generation, co-simulation) will be employed to assess the fault detection tool developed in the project.

The PhD will be carried out in the CONVECS project-team of the Inria Grenoble – Rhône-Alpes Centre. The activities of CONVECS focus on the formal modelling and verification of asynchronous concurrent systems, which are instantiated in various domains (communication protocols, distributed algorithms, embedded systems, etc.). To this aim, CONVECS proposes new formal languages for specifying the behaviour and the properties of concurrent systems, and devises efficient verification algorithms and tools running on sequential and massively parallel machines. The research results of CONVECS are instantiated in the CADP verification toolbox (http://cadp.inria.fr), which is widely used in academia and industry.


[GLMS13] H. Garavel, F. Lang, R. Mateescu, and W. Serwe. "CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes". Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2):89-107, 2013. http://hal.inria.fr/hal-00715056/en

[MMS18] L. Marsso, R. Mateescu, and W. Serwe. "TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation". In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS’2018 (Thessaloniki, Greece). Lecture Notes in Computer Science, Springer Verlag, April 2018.

[MS13] R. Mateescu and W. Serwe. "Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols". Science of Computer Programming 78(7):843-861, 2013. http://hal.inria.fr/hal-00671321/en

[MR18] R. Mateescu and J. I. Requeno. "On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators". Springer International Journal on Software Tools for Technology Transfer (STTT) 20(5):563-587, 2018. http://hal.inria.fr/hal-01862754/en

[HMSW18] B. Hofer, R. Mateescu, W. Serwe, and F. Wotawa. "Using LNT Formal Descriptions for Model-Based Diagnosis". Proceedings of the 29th International Workshop on Principles of Diagnosis DX'2018 (Warsaw, Poland), August 27-30, 2018. http://hal.inria.fr/hal-01877693/en

Principales activités

Main activities:

  • Study the fault detection and localization in actuators and propulsion systems, based on formal models, verification, and test generation techniques.

  • Couple the verification, validation, and fault detection based on formal methods into a co-simulation environment for virtual validation.

  • Specify and analyse formally the security and connectivity protocols eployed in ECAs, and generate security test suites from formal models.

  • Carry out a probabilistic model-based analysis of the fault detection and identification device developed in the project.

  • Identify the simulation environments related to a specific functionality by using conformance test generation techniques.

Additional activities:

  • Present the results at conferences and workshops.

  • Participate in project meetings.


Technical skills and level required: knowledge of formal methods and verification for concurrent systems

Languages: proficiency in English; knowledge of French also welcome

Relational skills: team working


  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage