NASA Ogma

NASA-Generator für Laufzeitmonitore für sichere Robotik- und Flugsysteme

Lizenz

Apache-2.0

Überblick

Ogma ist ein von der NASA entwickeltes Werkzeug zur Erzeugung von Laufzeitüberwachungsanwendungen für Robotik- und Flugsysteme. Es übersetzt übergeordnete Sicherheitsanforderungen, die in temporaler Logik formuliert sind (z. B. „die Flughöhe darf X niemals überschreiten, solange Y aktiv ist“), in effizienten C-, C++- oder ROS-Überwachungscode, der parallel zum eigentlichen System läuft. Ogma unterstützt das Robot Operating System (ROS/ROS2), die NASA-Flugsoftware-Frameworks cFS/fPrime und Space ROS. Es wird zur Sicherheitsabsicherung autonomer Systeme eingesetzt, bei denen eine formale Verifikation des Gesamtsystems nicht praktikabel ist.

NASA Ogma ist ein Werkzeug, das Laufzeitmonitore für Robotik- und Flugsoftwaresysteme erzeugt. Es erweitert Copilot, ein High-Level-Framework für Laufzeitverifikation, um aus temporallogischen Spezifikationen harten Echtzeit-Überwachungscode in C99 zu erzeugen. Die generierten Monitore lassen sich direkt in Anwendungen für ROS, ROS 2, das NASA Core Flight System (cFS), F' (fPrime) und Space ROS integrieren.

Das Werkzeug übersetzt formale Spezifikationen – geschrieben als temporallogische Ausdrücke oder sogar als visuelle Diagramme im DOT/Graphviz- und Mermaid-Format – in Überwachungsanwendungen, die das Systemverhalten zur Laufzeit beobachten. Wird eine Spezifikation verletzt, löst der Monitor Warnungen aus, sodass sicherheitskritische Probleme früh erkannt werden, bevor sie sich zu Ausfällen ausweiten.

Ogma wird von der NASA aktiv gepflegt, mit über 350 Commits pro Jahr. Es ist als Debian/Ubuntu-Paket und über das Haskell-Repository Hackage erhältlich. Das Projekt ist eine seltene Brücke zwischen der Forschung zu formalen Methoden und dem praktischen Robotikeinsatz und macht Laufzeitverifikation auf Luft- und Raumfahrtniveau der Open-Source-Robotik-Community zugänglich.

Warum es wichtig ist

Ogma bringt Laufzeitverifikation auf NASA-Niveau in die breitere Robotik-Community. Indem es Monitore automatisch aus formalen Spezifikationen erzeugt, ermöglicht es Entwicklern, ROS-, ROS-2- und Flugsoftwaresystemen Sicherheitsebenen hinzuzufügen, ohne komplexen Überwachungscode von Hand zu schreiben.

Welches Problem es löst

Sicherheitskritische Robotik- und Flugsysteme benötigen eine kontinuierliche Laufzeitüberwachung, um Verletzungen der Spezifikation zu erkennen, doch korrekten Überwachungscode von Hand zu schreiben ist fehleranfällig und zeitaufwendig. Ogma löst dieses Problem, indem es aus übergeordneten temporallogischen Spezifikationen automatisch harte Echtzeit-Monitore in C99 erzeugt und so Korrektheit durch Konstruktion sicherstellt.

Wichtigste Punkte

• Erzeugt Laufzeitmonitore aus temporallogischen Spezifikationen – kein manueller C-Code nötig
• Unterstützt die Frameworks ROS, ROS 2, NASA cFS, F' (fPrime) und Space ROS
• Basiert auf Copilot, einem High-Level-Framework für Laufzeitverifikation, das harten Echtzeit-C99-Code erzeugt
• Kann Monitore aus visuellen Diagrammen (DOT/Graphviz, Mermaid) erzeugen
• Von der NASA entwickelt und gepflegt, mit äußerst aktiver Entwicklung (über 350 Commits pro Jahr)

Für wen

• Robotikingenieure, die sicherheitskritische Systeme mit Bedarf an Laufzeitüberwachung entwickeln
• NASA- und Luft- und Raumfahrtentwickler, die mit cFS, fPrime oder Space ROS arbeiten
• ROS/ROS 2-Entwickler, die ihren Anwendungen Ebenen zur formalen Verifikation hinzufügen
• Forschende im Bereich autonomer Systeme, die Laufzeitverifikation und Sicherheitsnachweise untersuchen

Einschränkungen

• In Haskell geschrieben, das den meisten Robotikentwicklern wenig vertraut sein dürfte
• Erfordert Verständnis temporaler Logik, um aussagekräftige Spezifikationen zu schreiben
• Die Monitorerzeugung zielt auf bestimmte Frameworks – individuelle Integrationen erfordern zusätzlichen Aufwand
• Auf die Überwachung von Eigenschaften ausgerichtet, nicht auf die vollständige formale Verifikation des Systemverhaltens