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) suffers 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

Documents

• https://tier4.github.io/safe_drive/
• https://docs.rs/safe_drive/latest/safe_drive/

Supporting ROS2

• Humble
• Galactic (EOL)

Supporting DDS

• CycloneDDS
• FastDDS

Progress

• Zero copy
• Custom memory allocator
• Topic (Pub/Sub)
• Service (Client/Server)
• Asynchronous programming (async/await)
• Callback based programming
• Logging
• Signal handling
• Parameter
• Timer
• Action (service + topic)
• Rust code generation from .msg and .srv files
  • safe_drive_msg
• Formal Specification
  • Single threaded callback based executer
  • Scheduling Core Algorithm
  • Initializer performed just once