Understandable and Reusable Formal Verification for Cyber-Physical Systems

This project entitled "Verification of Autonomous Systems" sponsored by the Air Force Office of Scientific Research, is looking at ways to formally verify that systems that may operate on their own or autonomously meet their requirements. This is important for systems like autonomous vehicles and emerging systems, with the particular technical focus we're looking at being developing a language called Hyper Properties, which is a generalization of how we might typically write down requirements for these types of systems. We're developing Hyper Properties and also developing methods to try to automatically check whether models of these kind of systems would meet those requirements. This would, for instance, allow us to characterize behaviors of things like neural networks that may show up for different tasks within these kind of systems that are increasingly being used for things like perception or planning to try to figure out how to go from point A to point B. We're then evaluating these methods on a variety of Air Force case studies and benchmarks from both the air domain as well as from the space domain. It's an exciting project that might eventually lead to new methods and new ways to ensure that these systems operate reliably and safely.