abstract:
We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that is more scalable while also proving at least as safe. Now that we have the chance to redefine air traffic control from scratch, the question arises: how do we do it safely?
We explore new frontiers in symbolic model checking to scalably answer the functional allocation question: instead of analyzing one design, or comparing a pair of designs, we now need to take into account a large number of permutations and combinations of functions that comprise a large set of possible designs. We introduce a compositional, modular, parameterized approach to model generation. We comparatively analyze the design space with regard to safety on multiple levels, considering the set of possible system designs both in nominal conditions and in the presence of faults. Our analysis helps NASA narrow the possible design space, saving time and cost of later-phase evaluations, identifying both novel and known problematic design configurations. Our methods pave the way for the complexities demanded by future analysis, as the question of how to reason about adding Unmanned Aerial Systems into the national air traffic management system looms on the horizon.
bio:
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 Spring, 2015. Previous to that, she spent 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 in Computer Science from 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.
Most recently, Rozier was a primary contributing researcher to the Next Generation Air Transportation System (NextGen) Air Traffic Management project of the Airspace Systems Program at NASA. She also served as Principal Investigator of an ARMD Seedling project advancing System and Safety Health Management for Unmanned Aerial Systems (UAS). Rozier is an Associate Fellow of AIAA and a Senior Member of IEEE and SWE.