NASA Ogma

Generatore di monitor a runtime della NASA per sistemi robotici e di volo sicuri

Licenza

Apache-2.0

Panoramica

Ogma è uno strumento sviluppato dalla NASA per generare applicazioni di monitoraggio a runtime per sistemi robotici e di volo. Traduce requisiti di sicurezza di alto livello scritti in logica temporale (ad esempio “l'altitudine non deve mai superare X mentre Y è attivo”) in codice di monitoraggio C, C++ o ROS efficiente, che gira accanto al sistema reale. Ogma supporta Robot Operating System (ROS/ROS2), i framework di software di volo cFS/fPrime della NASA e Space ROS. È usato per garantire la sicurezza di sistemi autonomi in cui la verifica formale dell'intero sistema non è praticabile.

NASA Ogma è uno strumento che genera monitor a runtime per sistemi software robotici e di volo. Estende Copilot, un framework di verifica a runtime di alto livello, per produrre codice di monitoraggio C99 in tempo reale stretto a partire da specifiche in logica temporale. I monitor generati possono essere integrati direttamente in applicazioni ROS, ROS 2, NASA Core Flight System (cFS), F' (fPrime) e Space ROS.

Lo strumento traduce specifiche formali, scritte come espressioni di logica temporale o persino come diagrammi visivi in formato DOT/Graphviz e Mermaid, in applicazioni di monitoraggio che osservano il comportamento del sistema a runtime. Quando una specifica viene violata, il monitor genera avvisi, permettendo di rilevare precocemente problemi critici per la sicurezza prima che si propaghino in guasti.

Ogma è mantenuto attivamente dalla NASA, con oltre 350 commit all'anno. È disponibile come pacchetto Debian/Ubuntu e tramite il repository Hackage di Haskell. Il progetto rappresenta un raro ponte tra la ricerca sui metodi formali e il deployment pratico della robotica, e rende la verifica a runtime di livello aerospaziale accessibile alla comunità della robotica open source.

Perché è importante

Ogma porta la verifica a runtime di livello NASA alla più ampia comunità della robotica. Generando automaticamente monitor da specifiche formali, permette agli sviluppatori di aggiungere livelli di garanzia della sicurezza a sistemi ROS, ROS 2 e di software di volo senza scrivere a mano complesso codice di monitoraggio.

Il problema che risolve

I sistemi robotici e di volo critici per la sicurezza hanno bisogno di un monitoraggio continuo a runtime per rilevare le violazioni delle specifiche, ma scrivere a mano codice di monitoraggio corretto è soggetto a errori e richiede molto tempo. Ogma risolve il problema generando automaticamente monitor C99 in tempo reale stretto da specifiche di alto livello in logica temporale, garantendo la correttezza per costruzione.

Punti chiave

• Genera monitor a runtime da specifiche in logica temporale: nessun codice C da scrivere a mano
• Supporta i framework ROS, ROS 2, NASA cFS, F' (fPrime) e Space ROS
• Basato su Copilot, un framework di verifica a runtime di alto livello che produce C99 in tempo reale stretto
• Può generare monitor da diagrammi visivi (DOT/Graphviz, Mermaid)
• Sviluppato e mantenuto dalla NASA, con uno sviluppo estremamente attivo (oltre 350 commit all'anno)

A chi si rivolge

• Ingegneri robotici che costruiscono sistemi critici per la sicurezza che richiedono monitoraggio a runtime
• Sviluppatori della NASA e del settore aerospaziale che lavorano con cFS, fPrime o Space ROS
• Sviluppatori ROS/ROS 2 che aggiungono livelli di verifica formale alle proprie applicazioni
• Ricercatori di sistemi autonomi che studiano la verifica a runtime e la garanzia della sicurezza

Limiti

• Scritto in Haskell, che può risultare poco familiare alla maggior parte degli sviluppatori di robotica
• Richiede la conoscenza della logica temporale per scrivere specifiche significative
• La generazione dei monitor è rivolta a framework specifici: le integrazioni personalizzate richiedono lavoro aggiuntivo
• È incentrato sul monitoraggio di proprietà, non sulla verifica formale completa del comportamento del sistema