Kristin Rozier, Iowa State University

The Biggest Bottleneck in Formal Methods and Autonomy


Advancement of increasingly AI-enhanced control in autonomous systems stands on the shoulders of formal methods, which make possible the rigorous safety analysis autonomous systems require. For example, an aircraft cannot operate autonomously unless it has design-time reasoning to ensure correct operation of the autopilot and runtime reasoning to ensure system health management, or the ability to detect and respond to off-nominal situations that could not be verified at design time. Formal methods are highly dependent on the specifications over which they reason; not only are specifications required for analysis, but there is no escaping the "garbage in, garbage out" reality. Correct, covering, and formal specifications are thus an essential element for enabling autonomy. However, specification is difficult, unglamorous, and arguably the biggest bottleneck facing verification and validation of aerospace, and other, autonomous systems. This talk will examine the outlook for the practice of formal specification, and highlight the on-going challenges of specification, from design-time to runtime system health management. We will pose challenge questions for specification that will shape both the future of formal methods, and our ability to more automatically verify and validate autonomous systems of greater variety and scale.


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. She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER 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; the Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award. She is an Associate Fellow of AIAA.