Continuous Assurance of Autonomous Vehicle Behavior Through Machine Learned Correctness Properties

Correctness properties are critical to conducting verification and validation on software systems, especially those cyberphysical systems whose functionality changes frequently due to software updates, changes in the operating environment, or newly learned behaviors. We detail a novel method to automatically construct expressive, executable correctness properties in the form of machine-learned correctness properties which can be used to ensure that a system's behavior is correct with respect to its design and operating requirements. We propose a method to bootstrap the creation of these correctness properties using a novel simulation-based generation of training and testing data using multiple extensions to the Cross Entropy algorithm for search-based optimization. Then, we apply this method to a software-in-the-loop evaluation of an autonomous vehicle to demonstrate that such models can assert about important properties of multi-agent cyberphysical systems. We demonstrate that this process brings the task of developing robust correctness properties from the realm of formal methods experts into the domain of system developers and engineers, and that machine-learned correctness properties are expressive enough to capture the correct behavior of cyberphysical systems in their complex environments. This advancement can provide evidence of dependability to system designers and users, enhancing trust in the deployment of autonomous vehicles and other intelligent transportation systems.