@article{oai:ipsj.ixsq.nii.ac.jp:02004821, author = {Ryuta,Kambe and Makoto,Kurihara and Tetsuhiro,Kawaguchi and Ryohei,Kawabuchi and Yuuki,Takano and Ryuta Kambe and Makoto Kurihara and Tetsuhiro Kawaguchi and Ryohei Kawabuchi and Yuuki Takano}, issue = {2}, journal = {情報処理学会論文誌コンピューティングシステム(ACS)}, month = {Oct}, note = {Fault tolerance in autonomous driving systems is important for ensuring safe operation even under hazardous conditions, and is therefore a key consideration for deployment. In an autonomous driving system with redundant devices, it is necessary to maintain consistency across the system regarding which devices should handle processing at any given time. This paper introduces a new leader election algorithm tailored for autonomous driving systems and proposes a redundant system architecture that leverages this algorithm. To ensure practicality in autonomous driving scenarios, the algorithm is designed to handle any single failure, including network link crashes. Given the safety-critical nature of the environment and the inherent challenges in testing distributed algorithms, formal verification methods were employed to ensure both safety and liveness. In designing the redundant system, we propose a mechanism that enables safe stopping, even under constraints of limited computational resources. Experimental results show that the leader election algorithm operates within reasonable time frames in a simulated environment, and that the proposed redundant autonomous driving system successfully achieves in-lane stopping in scenarios requiring safe stops, such as navigating curved road segments. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.33(2025) (online) ------------------------------, Fault tolerance in autonomous driving systems is important for ensuring safe operation even under hazardous conditions, and is therefore a key consideration for deployment. In an autonomous driving system with redundant devices, it is necessary to maintain consistency across the system regarding which devices should handle processing at any given time. This paper introduces a new leader election algorithm tailored for autonomous driving systems and proposes a redundant system architecture that leverages this algorithm. To ensure practicality in autonomous driving scenarios, the algorithm is designed to handle any single failure, including network link crashes. Given the safety-critical nature of the environment and the inherent challenges in testing distributed algorithms, formal verification methods were employed to ensure both safety and liveness. In designing the redundant system, we propose a mechanism that enables safe stopping, even under constraints of limited computational resources. Experimental results show that the leader election algorithm operates within reasonable time frames in a simulated environment, and that the proposed redundant autonomous driving system successfully achieves in-lane stopping in scenarios requiring safe stops, such as navigating curved road segments. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.33(2025) (online) ------------------------------}, title = {Redundant Autonomous Driving System with Formally Verified Leader Election Algorithm}, volume = {18}, year = {2025} }