PoP Seminar Talk

From Design Time To Run Time: Formal Methods for Ensuring the Safetyof Safety-Critical Aerospace Systems

Kristin Yvonne Rozier, Head of the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University
Thursday, 08 December, 2022; 3:00pm
GHC 8102
Host: Marijn Heule


The COVID shutdowns of 2020 brought a new understanding of the need for automation of safety-critical systems, from Unmanned Aerial Systems (UAS) and their automated control to robots taking over tasks recently done by humans. As the demands for automation increase and the systems we design grow ever-more complex to accommodate advancing technology, a question arises: how do we know we are safe? This talk demonstrates how formal methods are growing increasingly vital for the development of safety-critical aerospace systems, and our ability to ensure safety and security of new designs for the next era in air and space.

We highlight success stories of formally-verified automation, including NASA’s automated Air Traffic Management (ATM) system and its equivalent for UAS (UTM). We contribute significant algorithmic advances to launch the design-time verification technique of model checking to new heights. Also, we demonstrate how formal specifications can be carried through to system run time and used to take runtime verification out of this world… all the way to the International Space Station (ISS). Our real-time, Realizable, Responsive, Unobtrusive Unit (R2U2) fills the gap of flight-certifiable reasoning that embeds on constrained safety-critical systems like UAS, satellites, and NASA’s humanoid robot Robonaut2 on the ISS. We introduce current projects to further push the boundaries of both design-time and runtime verification, asking the question, how do we proceed safely from here?


NSF CAREER Award winner and recipient of the Inaugural Initiative-Inspiration-Impact Award from Women in Aerospace, Kristin Yvonne Rozier joined the faculty of the Aerospace Engineering and Computer Science Departments in Fall, 2016. Previous to that, she spent three semesters at the University of Cincinnati (2015-2016) and 14 years as a Research Scientist at NASA, holding civil service positions at NASA Ames Research Center (2008-2014) and NASA Langley Research Center (2001-2008).

Rozier earned her PhD Rice University and MS and BS degrees from the College of William and Mary. During her tenure at NASA, she contributed research to the Aeroacoustics, and Safety-Critial Avionics groups at NASA Langley and to the Robust Software Engineering, and Discovery and Systems Health groups in the Intelligent Systems Division at NASA Ames. She has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.