Dr. Kristin Y. Rozier gave an invited College of Engineering Colloquium at the University of Miami on “Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System at NASA.” Dr. Rozier presented an overview of some of the most important principles of formal verification, such as model checking, and described her research in applying formal verification techniques early in the design stage of the Automated Airspace Concept (AAC) to ensure there are no potentially catastrophic design flaws remaining in the AAC coordination protocol design before the next stage of production.
The Colloquium was very well attended by the departments of Electrical and Computer Engineering, Aerospace Engineering, Industrial Engineering, and Computer Science, with standing room only. Dr. Rozier met with many interested members of the College of Engineering following the talk. Dr. Rozier also delivered two hours of invited lectures for the Embedded Microprocessor System Design course in the Department of Electrical and Computer Engineering. She instructed the class on the subjects of temporal logic and composition of state machines, and included applications such as formal specification and model checking. She tied the material in the students’ text to her research and real-life successes in formal verification at NASA.
BACKGROUND: Dr. Kristin Yvonne Rozier is a research computer scientist contributing research to the Next Generation Air Transportation System (NextGen) Air Traffic Management project of the Airspace Systems Program. She focuses on automated techniques for formal specification and verification of safety-critical systems.
NASA PROGRAM FUNDING: Separation Assurance Research focus area, Airspace Systems Program
Contact: Kristin Y. Rozier