Oxidros: Formally Specified Rust Bindings for ROS2

oxidros 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.

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

Supporting ROS2

• Jazzy
• Humble

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
• Formal Specification
  • Single threaded callback based executer
  • Scheduling Core Algorithm
  • Initializer performed just once

Credits

This project is a fork of safe_drive, originally developed by:

• Yuuki Takano (TIER IV, Inc.)
• Seio Inoue

We are grateful for their excellent work in creating formally specified Rust bindings for ROS2.