#initialization #ros2 #callback #bindings #formally #once

safe_drive

safe_drive: ROS2 的形式化 Rust 绑定

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机器人

Download history 554/week @ 2024-05-04 509/week @ 2024-05-11 373/week @ 2024-05-18 329/week @ 2024-05-25 404/week @ 2024-06-01 221/week @ 2024-06-08 414/week @ 2024-06-15 361/week @ 2024-06-22 520/week @ 2024-06-29 380/week @ 2024-07-06 558/week @ 2024-07-13 581/week @ 2024-07-20 827/week @ 2024-07-27 696/week @ 2024-08-03 713/week @ 2024-08-10 426/week @ 2024-08-17

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