Kristin Y Rozier
Professor Heads the Laboratory for Temporal Logic in Aerospace Engineering
Iowa State University
Specification: The Biggest Bottleneck in Formal Methods and Autonomy
Thursday, May 4, 2017
to 5:00 PM
3076 Duncan Hall
6100 Main St
Houston, Texas, USA
Advancement of autonomous systems stands on the shoulders of formal methods, which make possible the rigorous safety analysis autonomous systems require. 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. Formal methods are highly dependent on the specifications over which they reason; there is no escaping the ``garbage
in, garbage out'' reality. Specification is difficult, unglamorous, and arguably the biggest bottleneck facing verification and validation of autonomous systems.
We examine the outlook for formal specification, and highlight the on-going challenges of specification, from design-time to runtime. We exemplify these challenges for specifications in Linear Temporal Logic (LTL) though the
focus is not limited to that specification language. We 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. We call for further research into LTL Genesis.
Biography of Kristin Y Rozier:
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 RiceUniversity 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. She is an Associate Fellow of AIAA and a Senior Member of IEEE, ACM, and SWE. Dr. Rozier serves on the AIAA Intelligent Systems Technical Committee, where she chairs the Professional Development, Education, and Outreach subcommittee. She has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.