Deadlock- and Starvation-free Formally Verified Client Library for Robots
Yuuki Takano · 2023
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.