[agents] PhD Position F/M Formal Modelling and Validation for Electric, Connected, and Automated Vehicles

[Lina Marsso]

PhD Position F/M Formal Modelling and Validation for Electric, Connected,
and Automated Vehicles
--------------------------------------------------------

PhD thesis funded by the EU project ArchitectECA2030 (2020-2023), led by
Infineon AG (Germany). 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.

APPLICATION

See https://jobs.inria.fr/public/classic/fr/offres/2020-02722 for more
details on the call for application. Please feel free to circulate this
announcement to prospective students.

REFERENCES:

[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 <callto: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 <callto: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
<callto: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cs.umbc.edu/pipermail/agents/attachments/20200608/c70ddbb3/attachment-0001.html>