NASA Ogma

NASA 的執行期監控器產生工具，用於安全的機器人與飛行系統

授權條款

Apache-2.0

概述

Ogma 是 NASA 開發的工具，用於為機器人與飛行系統產生執行期監控應用程式。它將以時序邏輯撰寫的高階安全需求（例如「當 Y 啟用時，高度絕不能超過 X」）轉換成高效的 C、C++ 或 ROS 監控程式碼，與實際系統一同執行。Ogma 支援 Robot Operating System（ROS/ROS2）、NASA 的 cFS/fPrime 飛行軟體框架，以及 Space ROS。它用於在無法對整個系統進行形式驗證時，為自主系統提供安全保證。

NASA Ogma 是為機器人與飛行軟體系統產生執行期監控器的工具。它擴充了高階執行期驗證框架 Copilot，能從時序邏輯規格產生硬即時的 C99 監控程式碼。產生的監控器可直接整合進 ROS、ROS 2、NASA Core Flight System（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 撰寫，大多數機器人開發者可能不熟悉
• 需要了解時序邏輯，才能撰寫有意義的規格
• 監控器產生只針對特定框架，客製整合需要額外工作
• 聚焦於屬性監控，而非對系統行為進行完整的形式驗證