A Formally Verified Leader Election Algorithm for Autonomous Driving Systems

As autonomous driving systems mature, the importance of fault tolerance to provide safe operation even in hazardous conditions becomes a key issue in deployment. In an autonomous driving system composed of redundant devices, it is necessary to maintain consistency across the system regarding which devices should currently be handling processing. In this paper, we present a new leader election algorithm for autonomous driving systems that guarantees consistency in the presence of the failure of any single system component. To make the algorithm practical for autonomous driving systems, we design it to both handle network link failures and guarantee liveness in the presence of a single failure. Due to the safety-critical nature of our environment and the known difficulty of testing distributed algorithms, we use formal verification to validate our proposed algorithm. Our experiments show that the algorithm completes with reasonable time in a simulated environment of an autonomous driving system.