<div dir="ltr"><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">PhD Position F/M Formal Modelling and Validation for Electric, Connected, and Automated Vehicles</span></span></div><div>--------------------------------------------------------</div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">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.</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">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.</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">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 (<span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1812_com_zimbra_url" style="color:darkblue"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1821_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1915_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1921_com_zimbra_url" style="cursor: pointer;"><a target="_blank" href="http://cadp.inria.fr/" style="color:darkblue;text-decoration-line:none">http://cadp.inria.fr</a></span></span></span></span>), which is widely used in academia and industry.</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">APPLICATION</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">See <span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1813_com_zimbra_url" style="color:darkblue"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1822_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1916_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1922_com_zimbra_url" style="cursor: pointer;"><a target="_blank" href="https://jobs.inria.fr/public/classic/fr/offres/2020-02722" style="color:darkblue;text-decoration-line:none">https://jobs.inria.fr/public/classic/fr/offres/2020-02722</a></span></span></span></span> for more details on the call for application. Please feel free to circulate this announcement to prospective students.</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">REFERENCES:</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px"><br></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">[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):<span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1814_com_zimbra_phone" style="color:darkblue"><a href="callto:89-107, 2013" target="_blank" style="color:darkblue;text-decoration-line:none">89-107, 2013</a></span>. <span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1815_com_zimbra_url" style="color:darkblue"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1823_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1917_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1923_com_zimbra_url" style="cursor: pointer;"><a target="_blank" href="http://hal.inria.fr/hal-00715056/en" style="color:darkblue;text-decoration-line:none">http://hal.inria.fr/hal-00715056/en</a></span></span></span></span></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">[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.</span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">[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):<span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1816_com_zimbra_phone" style="color:darkblue"><a href="callto:843-861, 2013" target="_blank" style="color:darkblue;text-decoration-line:none">843-861, 2013</a></span>. <span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1817_com_zimbra_url" style="color:darkblue"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1824_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1918_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1924_com_zimbra_url" style="cursor: pointer;"><a target="_blank" href="http://hal.inria.fr/hal-00671321/en" style="color:darkblue;text-decoration-line:none">http://hal.inria.fr/hal-00671321/en</a></span></span></span></span></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">[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):<span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1818_com_zimbra_phone" style="color:darkblue"><a href="callto:563-587, 2018" target="_blank" style="color:darkblue;text-decoration-line:none">563-587, 2018</a></span>. <span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1819_com_zimbra_url" style="color:darkblue"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1825_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1919_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1925_com_zimbra_url" style="cursor: pointer;"><a target="_blank" href="http://hal.inria.fr/hal-01862754/en" style="color:darkblue;text-decoration-line:none">http://hal.inria.fr/hal-01862754/en</a></span></span></span></span></span></span></div><div><span style="color:rgb(51,51,51);font-family:monospace"><span style="font-size:14.16px">[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. <span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1820_com_zimbra_url" style="color:darkblue"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1826_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1920_com_zimbra_url" style="cursor: pointer;"><span class="gmail-Object" id="gmail-OBJ_PREFIX_DWT1926_com_zimbra_url" style="cursor: pointer;"><a target="_blank" href="http://hal.inria.fr/hal-01877693/en" style="color:darkblue;text-decoration-line:none">http://hal.inria.fr/hal-01877693/en</a></span></span></span></span></span></span></div><div><br style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif;font-size:16px;background-color:rgb(253,253,253)"></div></div>