Update on Machine-Learned Correctness Properties

Abstract

This report details a novel method which has the potential for improving the U.S. Navy’s ability to perform continuous assurance on autonomous and other cyberphysical systems. Specifically, this report presents a novel technique for simulation-driven data generation of explainable machine-learned correctness properties, called ML-assertions, for the purpose of subsequent runtime verification. The method brings the task of providing formal guarantees about the dependability of autonomous systems from the realm of doctoral-level experts into the domain of system developers and engineers. Preliminary experimentation demonstrates that ML-assertions can be utilized for behavior prediction in complex multi-agent systems, serving as a state-of-the-art method for conducting verification and validation on autonomous cyberphysical systems.