Principles of Programming Seminar
— 4:00pm
Location:
In Person
-
Gates Hillman 8102
Speaker:
KRISTIN YVONNE ROZIER
,
Black & Veatch Associate Professor of Aerospace Engineering, Computer Science, , Electrical and Computer Engineering, and Mathematics, Iowa State University of Science and Technology
https://faculty.sites.iastate.edu/kyrozier/
From Design Time To Run Time: Formal Methods for Ensuring the Safety of Safety-Critical Aerospace
The COVID shutdowns of 2020 brought a new understanding of the need for automation of safety-critical systems, from Unmanned Aerial Systems (UAS) and their automated control to robots taking over tasks recently done by humans. As the demands for automation 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 highlight success stories of formally-verified automation, including NASA's automated Air Traffic Management (ATM) system and its equivalent for UAS (UTM). We contribute significant algorithmic advances to launch the design-time verification technique of model checking to new heights. Also, we demonstrate how formal specifications can be carried through to system run time and used to take runtime verification out of this world... all the way to the International Space Station (ISS). Our real-time, Realizable, Responsive, Unobtrusive Unit (R2U2) fills the gap of flight-certifiable reasoning that embeds on constrained safety-critical systems like UAS, satellites, and NASA's humanoid robot Robonaut2 on the ISS. We introduce current projects to further push the boundaries of both design-time and runtime verification, asking the question, how do we proceed safely from here? Faculty Host: Marijn HeuleEvent Website:
https://www.cs.cmu.edu/Groups/pop/index.html