# 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](https://github.com/tier4/safe_drive/tree/main/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://tier4.github.io/safe_drive/)
- [https://docs.rs/safe_drive/latest/safe_drive/](https://docs.rs/safe_drive/latest/safe_drive/)
## Supporting ROS2
- [x] Jazzy, ([PR #25](https://github.com/tier4/safe_drive/pull/25))
- [x] Humble
- [ ] Galactic (EOL)
## Supporting DDS
- [x] CycloneDDS
- [x] FastDDS
## Progress
- [x] Zero copy
- [x] Custom memory allocator
- [x] Topic (Pub/Sub)
- [x] Service (Client/Server)
- [x] Asynchronous programming (async/await)
- [x] Callback based programming
- [x] Logging
- [x] Signal handling
- [x] Parameter
- [x] Timer
- [x] Action (service + topic)
- [x] Rust code generation from .msg and .srv files
- [safe_drive_msg](https://github.com/tier4/safe_drive_msg)
- [x] Formal Specification
- [x] Single threaded callback based executer
- [x] Scheduling Core Algorithm
- [x] Initializer performed just once