论文标题
通过贝叶斯优化对安全关键自主系统的正式验证
Formal Verification of Safety Critical Autonomous Systems via Bayesian Optimization
论文作者
论文摘要
随着控制系统变得越来越复杂，存在迫切需要寻找系统的方法来验证它们。为了解决这一问题，在开发黑盒控制体系结构的测试生成方案方面已经有重要工作。当这些目标通过时间逻辑公式表示为操作规范时，这些方案测试了黑框控制体系结构满足其控制目标的能力。我们的工作通过降低黑框系统将满足其操作规范的概率（在经过预先指定的环境现象集时）来扩展这些先前的基于模型的结果。我们通过系统地生成测试来最大程度地减少Lipschitz的连续鲁棒性度量以进行操作规范来做到这一点。我们通过实验结果演示了我们的方法，其中我们表明我们的框架可以合理地降低规范满意度的概率。
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.
