Formal Methods for Safe Autonomous Driving

Speaker:
Thierry Lecomte – CLEARSY Founder & R&D Director, FM Evangelist

Abstract:
Formal methods history is paved with industry successes towards the improvement of railway systems safety: – L14 Paris driverless metro without accident after 20 years of exploitation, now historic line 1, then line 4 in the near future; – more than 30% worldwide CBTC-based metros embed a formal method; – formal techniques to prove configuration parameters and system level specification correctness; – safety computer programmed with formal method for SIL4 sensor-based C&C systems. Formal methods are adequate to integrate autonomous systems in more open environments like autonomous trains and shuttles. This presentation makes clear how the future autonomous systems could benefit from further formal engineering.