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로 작성되어 대부분의 로보틱스 개발자에게 익숙하지 않을 수 있습니다
• 의미 있는 명세를 작성하려면 시간 논리에 대한 이해가 필요합니다
• 모니터 생성은 특정 프레임워크를 대상으로 하므로 맞춤형 통합에는 추가 작업이 필요합니다
• 시스템 동작의 완전한 형식 검증이 아니라 속성 모니터링에 초점을 둡니다