NASA Ogma

Gerador de monitores em tempo de execução da NASA para sistemas robóticos e de voo seguros

Licença

Apache-2.0

Visão geral

Ogma é uma ferramenta desenvolvida pela NASA para gerar aplicações de monitoramento em tempo de execução para sistemas robóticos e de voo. Ela traduz requisitos de segurança de alto nível escritos em lógica temporal (por exemplo, 'a altitude nunca deve exceder X enquanto Y estiver ativo') em código de monitoramento eficiente em C, C++ ou ROS, executado em paralelo ao sistema real. O Ogma oferece suporte ao Robot Operating System (ROS/ROS2), aos frameworks de software de voo cFS/fPrime da NASA e ao Space ROS. É usado para a garantia de segurança de sistemas autônomos nos quais a verificação formal do sistema completo é inviável.

O NASA Ogma é uma ferramenta que gera monitores em tempo de execução para sistemas robóticos e de software de voo. Ele estende o Copilot, um framework de verificação em tempo de execução de alto nível, para produzir código de monitoramento C99 de tempo real rígido a partir de especificações em lógica temporal. Os monitores gerados podem ser integrados diretamente em aplicações ROS, ROS 2, NASA Core Flight System (cFS), F' (fPrime) e Space ROS.

A ferramenta traduz especificações formais — escritas como expressões de lógica temporal ou até como diagramas visuais nos formatos DOT/Graphviz e Mermaid — em aplicações de monitoramento que observam o comportamento do sistema em tempo de execução. Quando uma especificação é violada, o monitor dispara alertas, permitindo detectar cedo problemas críticos de segurança antes que se transformem em falhas em cascata.

O Ogma é mantido ativamente pela NASA, com mais de 350 commits por ano. Está disponível como pacote Debian/Ubuntu e pelo repositório Hackage do Haskell. O projeto representa uma ponte rara entre a pesquisa em métodos formais e a implantação prática em robótica, tornando a verificação em tempo de execução de nível aeroespacial acessível à comunidade de robótica de código aberto.

Por que importa

O Ogma leva a verificação em tempo de execução de nível NASA à comunidade de robótica em geral. Ao gerar monitores automaticamente a partir de especificações formais, permite que desenvolvedores adicionem camadas de garantia de segurança a sistemas ROS, ROS 2 e de software de voo sem escrever manualmente códigos de monitoramento complexos.

Problema que resolve

Sistemas robóticos e de voo críticos para a segurança precisam de monitoramento contínuo em tempo de execução para detectar violações de especificação, mas escrever manualmente um código de monitoramento correto é propenso a erros e demorado. O Ogma resolve isso gerando automaticamente monitores C99 de tempo real rígido a partir de especificações de alto nível em lógica temporal, garantindo a correção por construção.

Pontos principais

• Gera monitores em tempo de execução a partir de especificações em lógica temporal, sem necessidade de escrever código C manualmente
• Oferece suporte aos frameworks ROS, ROS 2, NASA cFS, F' (fPrime) e Space ROS
• Construído sobre o Copilot, um framework de verificação em tempo de execução de alto nível que produz C99 de tempo real rígido
• Pode gerar monitores a partir de diagramas visuais (DOT/Graphviz, Mermaid)
• Desenvolvido e mantido pela NASA, com desenvolvimento extremamente ativo (mais de 350 commits por ano)

Para quem é

• Engenheiros de robótica que constroem sistemas críticos de segurança que exigem monitoramento em tempo de execução
• Desenvolvedores da NASA e do setor aeroespacial que trabalham com cFS, fPrime ou Space ROS
• Desenvolvedores ROS/ROS 2 que adicionam camadas de verificação formal às suas aplicações
• Pesquisadores de sistemas autônomos que estudam verificação em tempo de execução e garantia de segurança

Limitações

• Escrito em Haskell, linguagem que pode ser pouco familiar para a maioria dos desenvolvedores de robótica
• Exige compreensão de lógica temporal para escrever especificações significativas
• A geração de monitores é voltada a frameworks específicos; integrações personalizadas exigem trabalho adicional
• Focado no monitoramento de propriedades, não na verificação formal completa do comportamento do sistema