safe_drive: Formally Specified Rust Bindings for ROS2

safe_drive is a Rust bindings for ROS2. This library provides formal specifications and tested the specifications by using a model checker. Therefore, you can clearly understand how the scheduler work and the safeness of it.

Specifications

Some algorithms we adopted are formally specified and tested the safeness by using TLA+. Original ROS2's executor (rclcpp) is suffering from starvation. In contrast, the starvation freedom of our executor has been validated by not only dynamic analysis but also formal verification.

See specifications.

We specified and tested as follows.

• Single Threaded Callback Execution
  • Deadlock freedom
  • Starvation freedom
• Scheduling Core Algorithm
  • Validate the insertion algorithm
  • Termination
• Initialize Once
  • Deadlock freedom
  • Termination
  • Initialization is performed just once