Abstract

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. However, the introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. In this talk we discuss two systems: Copilot 3, a stream-based runtime verification language for real-time embedded systems, and NASA's Ogma, a tool to transform high-level specifications into Copilot monitors. When used in combination, the toolchain can be used to translate structured natural language requirements into C code with static memory requirements, which can be compiled to run on embedded hardware. Apart from generating standalone monitors, our tools generate self-contained units ready to be integrated in NASA Core Flight System cFS and Robot Operating System (ROS2) applications.

Bio

Dr. Ivan Perez is a senior research scientist contractor at NASA Ames Research Center, and has been a member of the NASA Formal Methods Group since 2018. Dr Perez investigates the application of formal methods to problems in aerospace, with particular focus on runtime verification of unmanned aerial vehicles. Prior to joining NASA, Dr. Perez founded and led Keera Studios, the first mobile Haskell game programming company in the world, and Cubilabs.com, a functional programming company focused on business applications. Over the last two decades, Dr. Perez has also worked as a programmer and researcher for the High Performance Computing Center (Germany), IMDEA Software (Spain), the Technical University of Madrid (Spain), and the University of Twente (Netherlands), as well as for multiple functional programming companies. Dr. Perez completed his PhD in Computer Science at the University of Nottingham (UK), which focused on testing and functional programming applied to games and user interfaces. He also holds a Master's Degree in Computational Logic and a Degree of Engineer in Computer Science, both from the Technical University of Madrid.