Dr. Ivan Perez is a senior research scientist at KBR @ 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. He is the Technical Lead of NASA's Ogma, an open-source tool to generate runtime monitoring applications, and Copilot, a NASA-funded, open-source runtime monitoring language. A frequent program member and chair of scientific conferences, Dr. Perez is the lead chair of the 2nd Open Source for Space Workshop, as part of the IEEE Space Mission Challenges for Information Technology Conference (SMC-IT 2023), which will take place in Pasadena, California, in July 2023. Outside of his work for NASA, he also maintains multiple open-source libraries for reactive programming and functional reactive programming, including Yampa and Dunai, and has been an active member of the open-source community since the early 2000s.
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. With a professional career spanning more than two decades, Dr. Perez has also worked as a programmer and researcher for IMDEA Software (Spain), the High-Performance Computing Center of the University of Stuttgart (Germany), 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), focusing 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. More info: https://ivanperez.io/
Open Source in Space: Challenges Developing and Adopting Open Source Tools for Aerospace
Assuring software to the level needed to run in safety-critical applications imposes
constraints not only on what the software does, but also on how the software
is created. The methods required to achieve such level of assurance come
with additional rules, making them expensive, complex, and hard to adopt by
community-driven open-source projects.
This talk discusses our experience developing two open-source projects at NASA:
Copilot, a runtime monitoring language that generates realtime C code, and
Ogma, a tool to generate runtime monitoring applications ready to run for the
Robot Operating System (ROS 2), NASA’s Core Flight System (cFS) and F’
(FPrime). Both projects are implemented in Haskell, leverage existing open-
source libraries, and are used in flights on unmanned aerial systems. Additionally,
both projects follow a strict development process designed to meet NASA’s
Software Engineering Requirements (NPR7150).
In particular, this talk focuses on the challenges found when adopting a Haskell
as a language, the challenges found when getting the community to contribute,
and the methods and tools we put in place to make that process easier to adopt
by new team members, new projects, and community contributors. Our hope is
that our efforts will encourage the community to start a conversation about how
we design, develop and maintaining open-source software, and what steps we
can take to increase its quality and adoption in safety-critical domains.