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モニターを自動生成することでこの問題を解決し、構成による正しさ（correctness by construction）を保証します。

主なポイント

• 時相論理の仕様からランタイムモニターを生成（手作業でのCコード作成は不要）
• ROS、ROS 2、NASA cFS、F'（fPrime）、Space ROSの各フレームワークに対応
• ハードリアルタイムのC99を生成する高レベルのランタイム検証フレームワークCopilotを基盤に構築
• 視覚的な図（DOT/Graphviz、Mermaid）からモニターを生成可能
• NASAが開発・保守しており、開発は非常に活発（年間350件以上のコミット）

対象

• ランタイム監視を必要とする安全性重視のシステムを構築するロボティクスエンジニア
• cFS、fPrime、Space ROSを扱うNASAおよび航空宇宙分野の開発者
• アプリケーションに形式検証のレイヤーを追加するROS/ROS 2開発者
• ランタイム検証と安全保証を研究する自律システムの研究者

制限事項

• Haskellで書かれており、多くのロボティクス開発者にはなじみが薄い可能性があります
• 意味のある仕様を書くには時相論理の理解が必要です
• モニター生成は特定のフレームワークを対象としており、独自の統合には追加作業が必要です
• プロパティの監視に重点を置いており、システム挙動の完全な形式検証は対象外です