Deadlock- and Starvation-free Formally Verified Client Library for Robots

Robot middleware is crucial for managing diverse robotic functions, though it often faces issues like deadlock and starvation. Addressing these, this paper introduces two libraries, safe_drive and async_lib, aiming to enhance the efficiency and safety of ROS 2 middleware. These libraries address deadlock and starvation through well-typed APIs and formal verification methods, offering enhanced security. The safe_drive library, a single-threaded client library for ROS 2, features a task executor verified to be free from deadlock and starvation using PlusCal and TLA+, establishing credibility. On the other hand, async_lib offers well-typed intra-process communication APIs for multi-threading environments, with ver-ified multi-threaded executors that support safe_drive in complex applications, thereby facilitating efficient robot applications. Furthermore, the paper proposes using session types and typestate programming for safe communication protocol im-plementation, capable of detecting protocol violations at both compile and run time, especially useful in complex scenarios like state transitions in action servers where violations could lead to deadlock.