NASA Ogma

NASA 开发的运行时监控生成器，用于安全的机器人与飞行系统

许可证

Apache-2.0

概述

Ogma 是 NASA 开发的一款工具，用于为机器人和飞行系统生成运行时监控应用。它将用时序逻辑编写的高层安全需求（例如“当 Y 处于激活状态时，高度绝不能超过 X”）转换为高效的 C、C++ 或 ROS 监控代码，与实际系统并行运行。Ogma 支持机器人操作系统（ROS/ROS2）、NASA 的 cFS/fPrime 飞行软件框架以及 Space ROS。它用于自主系统的安全保障，适用于对整个系统进行形式化验证不切实际的场合。

NASA Ogma 是一款为机器人和飞行软件系统生成运行时监控器的工具。它扩展了高层运行时验证框架 Copilot，可从时序逻辑规约生成硬实时 C99 监控代码。生成的监控器可直接集成到 ROS、ROS 2、NASA 核心飞行系统（cFS）、F'（fPrime）和 Space ROS 应用中。

该工具将形式化规约（以时序逻辑表达式编写，甚至可以是 DOT/Graphviz 和 Mermaid 格式的可视化图）转换为在运行时观察系统行为的监控应用。一旦规约被违反，监控器就会触发警报，从而在安全攸关问题演变为故障之前及早发现。

Ogma 由 NASA 积极维护，每年提交超过 350 次。它以 Debian/Ubuntu 软件包形式提供，也可通过 Haskell 的 Hackage 仓库获取。该项目是连接形式化方法研究与实际机器人部署的少有桥梁，使开源机器人社区也能用上航空航天级的运行时验证。

为何重要

Ogma 将 NASA 级的运行时验证带给更广泛的机器人社区。它通过从形式化规约自动生成监控器，使开发者无需手动编写复杂的监控代码，就能为 ROS、ROS 2 和飞行软件系统添加安全保障层。

解决的问题

安全攸关的机器人和飞行系统需要持续的运行时监控来检测违反规约的情况，但手工编写正确的监控代码既容易出错又耗时。Ogma 通过从高层时序逻辑规约自动生成硬实时 C99 监控器来解决这一问题，从构造上保证正确性。

要点

• 从时序逻辑规约生成运行时监控器，无需手写 C 代码
• 支持 ROS、ROS 2、NASA cFS、F'（fPrime）和 Space ROS 框架
• 基于高层运行时验证框架 Copilot 构建，生成硬实时 C99 代码
• 可从可视化图（DOT/Graphviz、Mermaid）生成监控器
• 由 NASA 开发和维护，开发极为活跃（每年 350 次以上提交）

适用人群

• 构建需要运行时监控的安全攸关系统的机器人工程师
• 使用 cFS、fPrime 或 Space ROS 的 NASA 及航空航天开发者
• 为其应用添加形式化验证层的 ROS/ROS 2 开发者
• 研究运行时验证与安全保障的自主系统研究人员

局限

• 使用 Haskell 编写，大多数机器人开发者可能不熟悉
• 需要理解时序逻辑才能编写有意义的规约
• 监控器生成面向特定框架，定制集成需要额外工作
• 侧重于属性监控，而非对系统行为进行完整的形式化验证