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
3,819 downloads per month
Used in ros2_helpers
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