21 releases

0.4.3 Aug 15, 2024
0.4.1 Jul 26, 2024
0.3.7 Jan 26, 2024
0.3.6 Dec 15, 2023
0.1.3 Dec 17, 2022

#5 in Robotics

Download history 685/week @ 2024-08-02 719/week @ 2024-08-09 537/week @ 2024-08-16 568/week @ 2024-08-23 552/week @ 2024-08-30 932/week @ 2024-09-06 672/week @ 2024-09-13 551/week @ 2024-09-20 694/week @ 2024-09-27 700/week @ 2024-10-04 725/week @ 2024-10-11 800/week @ 2024-10-18 627/week @ 2024-10-25 765/week @ 2024-11-01 1293/week @ 2024-11-08 959/week @ 2024-11-15

3,819 downloads per month
Used in ros2_helpers

Custom license

9.5MB
243K SLoC

Contains (WOFF font, 99KB) fontawesome-webfont.woff, (WOFF font, 78KB) fontawesome-webfont.woff2, (WOFF font, 45KB) open-sans-v17-all-charsets-300.woff2, (WOFF font, 41KB) open-sans-v17-all-charsets-300italic.woff2, (WOFF font, 45KB) open-sans-v17-all-charsets-600.woff2, (WOFF font, 43KB) open-sans-v17-all-charsets-600italic.woff2 and 7 more.

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

Supporting ROS2

  • Jazzy, (PR #25)
  • 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
  • Formal Specification
    • Single threaded callback based executer
    • Scheduling Core Algorithm
    • Initializer performed just once

Dependencies

~4–10MB
~111K SLoC