Proof assistants are a programming technique for writing trustworthy software, in which the programmer writes not only the program code but also a mathematical proof of the code's correctness. An automated proof checker then either verifies that the code is correct or shows where the proof is wrong, thus empowering the programmer to fix incorrect assumptions. This project focuses on the goal of software assurance for autonomous vehicles (AVs), which are complex cyber-physical systems, such as multi-robot teams, that move in the world and interact with one another. Examples of these systems include self-driving cars, automated drones for inspection and surveillance, and rescue robots for disaster recovery. Programs that interact with the real world through sensors and actuators must make many assumptions about noisy sensors, physics, human users, and other circumstances that cannot be controlled by the program. The intellectual merits are three tools to implement and prove complex AVs correct for noisy, real-world operations. These tools equip AVs to handle increasing levels of complexity of interaction. This project will lead to advances in software assurance of many kinds of AVs and multi-CPS systems. The project's broader significance and importance are that all kinds of AVs in the future must be built to be safe for real-world deployment, even under adverse conditions. Interoperability of diverse AV systems will also be improved, which will aid in coordination, for example among first-responders.
The project integrates three key tasks into the verification of cyber-physical systems with increasing levels of concurrent operation. First, the project investigates the application of transformers to AVs. A transformer is a mechanism to combine a complex program with a proof about a corresponding simpler program in order to yield a proof about the complex program. This method will empower engineers to design AVs that can interact with one another safely and correctly in the real world without proving by hand the correctness of the multi-CPS variant of the program that handles errors in sensing and actuation. In the second task, the project turns to the verification of certain core building blocks of mobile AVs, including the rapidly-exploring random trees (RRT) motion planner and the Kalman filter state estimator. The core challenge in this task is to prove properties about algorithms that use continuum probabilities and other real numbers, typically implemented as floats. Since floating-point errors present an obstacle to verification, the PIs instead leverage constructive reals, which are capable of computing a result to arbitrary precision. In the third task, the project seeks to define a type system as the basis for codifying and performing inference about capabilities of heterogeneous AVs. This representation of capabilities is flexible, extensible, and supports probabilistic inference, thus accounting for sensing and actuation errors. This task will enable close coordination, even among AVs that have never encountered one another before.
