Formal Verification of Safety Critical Autonomous Systems via Bayesian Optimization
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.
Additional Information
This work was supported by the Air Force Office of Scientific Research.Attached Files
Submitted - 2009.12909.pdf
Files
Name | Size | Download all |
---|---|---|
md5:c4af2c826eff75bf07e050ddcac4e021
|
16.0 MB | Preview Download |
Additional details
- Eprint ID
- 106544
- Resolver ID
- CaltechAUTHORS:20201109-140925178
- Air Force Office of Scientific Research (AFOSR)
- Created
-
2020-11-09Created from EPrint's datestamp field
- Updated
-
2023-06-02Created from EPrint's last_modified field