Autonomous vehicles can only be accepted by end users and authorities after bringing convincing arguments on the benefits of having such vehicles, of their trustworthiness and after having a clear assessment on the potential risks they bring into our cities. It is absolutely critical to establish formally that benefits are higher than risks and that the vehicle decisions will, in all cases, “outperform” decisions from average human drivers. To achieve this goal, simple test is too weak. Hence, the design process must rely on a formal modelling and verification methodology that gives sufficient convincing guarantees to the car manufacturers and authorities. However, full exhaustive verification is also discarded because of the complexity of dynamic situations to consider.
The proposed approach aims at building dynamically a model of the surrounding complex environment of an autonomous vehicle based on formal rule-based models of typical actors involved (vehicles, obstacles, local driving legislation). This formal model would allow the monitoring of lower-level control systems, like the trajectory planning system, to ensure they behave as expected given the circumstances. The set of rules of the primitive actors must include both driving procedures in normal conditions following local laws as well as emergency behaviours with collision avoidance manoeuvres in extreme situations. The main objective is therefore to provide formal verification at runtime, with alerts when detecting rule violations. Liveness properties, like convergence towards desirable behaviours, might also be studied.
We want to explore the use of a model-based system engineering approach to reconcile all the heterogeneous models involved in the design of such a complex system and to rely on the industrial success of logical time in the design of safety-critical systems to address these issues.
Requirements: holding a Master in Computer Science, or equivalent.
Location: Sophia Antipolis, France, shared time between Renault Software Labs and Kairos team (I3S/INRIA)
Contact: Frederic.Mallet@unice.fr, firstname.lastname@example.org
PhD contract: Joint industry/university agreement (CIFRE)
Starting date: end 2018.
Instructions: Send your resume and transcripts (undergraduate and graduate) by email.