21 个版本
0.4.3 | 2024年8月15日 |
---|---|
0.4.1 | 2024年7月26日 |
0.3.7 | 2024年1月26日 |
0.3.6 | 2023年12月15日 |
0.1.3 | 2022年12月17日 |
#4 在 机器人 中
2,877 每月下载量
9.5MB
243K SLoC
包含 (WOFF 字体, 99KB) fontawesome-webfont.woff, (WOFF 字体, 78KB) fontawesome-webfont.woff2, (WOFF 字体, 45KB) open-sans-v17-all-charsets-300.woff2, (WOFF 字体, 41KB) open-sans-v17-all-charsets-300italic.woff2, (WOFF 字体, 45KB) open-sans-v17-all-charsets-600.woff2, (WOFF 字体, 43KB) open-sans-v17-all-charsets-600italic.woff2 和更多.
safe_drive: ROS2 的形式化 Rust 绑定
safe_drive
是 ROS2 的 Rust 绑定。此库提供了形式化规范,并通过使用模型检查器测试了规范。因此,您可以清楚地了解调度器的工作原理及其安全性。
规范
我们采用的一些算法是形式化指定的,并使用 TLA+ 测试了安全性。原始 ROS2 的执行器 (rclcpp) 存在饥饿问题。相比之下,我们的执行器的饥饿自由性不仅通过动态分析,而且通过形式验证得到了验证。
见 规范。
我们按以下方式指定和测试。
- 单线程回调执行
- 死锁自由
- 饥饿自由
- 调度核心算法
- 验证插入算法
- 终止
- 初始化一次
- 死锁自由
- 终止
- 初始化仅执行一次
文档
支持 ROS2
- Jazzy, (PR #25)
- Humble
- Galactic (EOL)
支持 DDS
- CycloneDDS
- FastDDS
进展
- 零拷贝
- 自定义内存分配器
- 主题 (发布/订阅)
- 服务 (客户端/服务器)
- 异步编程 (async/await)
- 基于回调的编程
- 日志记录
- 信号处理
- 参数
- 计时器
- 操作 (服务 + 主题)
- Rust 代码生成自 .msg 和 .srv 文件
- 形式化规范
- 基于单线程回调的执行器
- 调度核心算法
- 初始化仅执行一次
依赖关系
~4–11MB
~112K SLoC