Rockets, Route-Analyzers, Rotorcraft, and Robonaut2: Intelligent, On-board Runtime Reasoning 

1 July 2024 | Sala Stringa - Online | 11:00 | Kristin Yvonne Rozier (Heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University)

Abstract

Runtime Verification (RV) has become critical to the deployment of a wide range of systems, including aircraft, spacecraft, satellites, rovers, and robots, as well as the systems that control them, like air traffic control systems and space stations. The most useful, important, and safety-critical jobs will require these systems to operate both intelligently and autonomously, with the ability to sense and respond to both nominal and off-nominal conditions. It is essential that we enable reasoning sufficient to react to dynamic environments and detect critical failures on-board, in real time, to enable mitigation triggering. We are challenged by the constraints of real-life embedded operation that limit the system instrumentation, space, timing, power, weight, cost, and other operating conditions of on-board, runtime verification. While the research area of RV is vast, there is a dearth of RV tools that can operate within these constraints, and without violating rules for air and space flight certification.

The Realizable, Responsive, Unobtrusive Unit (R2U2) analyzes specifications that combine temporal logics with powerful reasoning to provide formal assurances during runtime, enabling self-assessment of critical systems. This presentation overviews recent algorithmic advances and the case studies they enabled, including embedding on-board NASA's humanoid robot Robonaut2, a UTM (UAS Traffic Management) system, a CubeSat, and the NASA Lunar Gateway.  


Bio
Professor Kristin Yvonne Rozier heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University; previously she spent 14 years as a Research Scientist at NASA and three semesters as an Assistant Professor at the University of Cincinnati. She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Dr. Rozier's research focuses on automated techniques for the formal specification, validation, and verification of safety critical systems. Her primary research interests include: design-time checking of system logic and system requirements; runtime system health management; and safety and security analysis.

Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER Award; the NASA Early Career Faculty Award; American Helicopter Society's Howard Hughes Award; Women in Aerospace Inaugural Initiative-Inspiration-Impact Award; two NASA Group Achievement Awards; two NASA Superior Accomplishment Awards; Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award; Building a World of Difference faculty fellowship. She holds an endowed position as Dennis and Rebecca Muilenburg Professor, is an Associate Fellow of AIAA, and is a Senior Member of IEEE, ACM, and SWE. Dr. Rozier has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.