From Design Time To Run Time: Formal Methods for Ensuring the Safety of Safety-Critical Aerospace Systems
- 14:00 1st May 2018 ( Trinity Term 2018 )LTB
As the demands on our airspace 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 are at the dawn of the age of automated air traffic control, where safe separation between aircraft remains the primary consideration. This talk highlights our recent success applying formal verification techniques in NASA's design for automated Air Traffic Management (ATM). We formalize the high-level operational concept, perform model validation, formalize specifications describing safe system operations, and use model checking for early design-stage verification. New modeling methods increase scalability to analyze a large (20K+) set of possible ATM designs. Our results revealed unexpected emergent behaviors in the operational concept that triggered design changes by system engineers to meet safety standards. Also, we demonstrate how formal specifications can be carried through to system run time and used for System Health Management (SHM). Our real-time, Realizable, Responsive, Unobtrusive Unit (R2U2) meets the emerging needs for SHM of both aircraft and new safety-critical embedded systems like Unmanned Aerial Systems (UAS), robots, and spacecraft. We highlight a new project adapting R2U2 for Robonaut2, whose leg joint arrived at ISU in January, 2018, and look toward the future, asking the question, how do we proceed safely from here?
Speaker 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. 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.
Share this:
