Formal Verification of Safety Critical Autonomous Systems via Bayesian Optimization

TL;DR

This paper introduces a Bayesian optimization-based method for systematically verifying the safety of complex autonomous control systems by generating tests that lower bound the probability of satisfying operational specifications.

Contribution

It extends existing model-based verification methods by providing probabilistic guarantees for black-box control systems using systematic test generation.

Findings

Successfully lower bounds the probability of specification satisfaction.

Demonstrates effectiveness through experimental validation.

Framework applicable to safety-critical autonomous systems.

Abstract

As control systems become increasingly more complex, there exists a pressing need to find systematic ways of verifying them. To address this concern, there has been significant work in developing test generation schemes for black-box control architectures. These schemes test a black-box control architecture's ability to satisfy its control objectives, when these objectives are expressed as operational specifications through temporal logic formulae. Our work extends these prior, model based results by lower bounding the probability by which the black-box system will satisfy its operational specification, when subject to a pre-specified set of environmental phenomena. We do so by systematically generating tests to minimize a Lipschitz continuous robustness measure for the operational specification. We demonstrate our method with experimental results, wherein we show that our framework can reasonably lower bound the probability of specification satisfaction.