通过合成代理程序洞察 AI 赋能控制系统的安全违规

鉴于现代 AI 赋能控制系统的日益普及，确保其安全性和可靠性已成为软件测试中的关键任务。测试控制系统的常见方法是 falsification，即通过优化算法寻找导致控制系统违反形式化安全规范的输入信号。然而，将 falsification 应用于 AI 赋能控制系统会提出两个重大挑战：(1) 需要执行大量候选测试输入，这在 AI 模型参数众多时可能耗时，而且(2) 多个安全要求通常定义为联合约束，现有 falsification 方法难以全面覆盖。本文引入了 Synthify，一个专为 AI 赋能控制系统设计的 falsification 框架。我们的方法采用两个阶段的 falsification过程。首先，Synthify 合成一个实现一个或多个线性控制器的程序作为 AI 控制器的代理。该代理程序模拟 AI 控制器的功能，但计算更高效。随后，Synthify 采用 $\epsilon$-贪婪策略从联合安全规范中抽样出一个有前景的子规范。然后，它使用基于模拟退火的 falsification算法寻找控制系统对抽样子规范的违规。为评估 Synthify，我们将其与 PSY-TaLiRo—a款最先进且工业级的 falsification工具，在 8 个公开可用的控制系统上进行比较。平均而言，Synthify 在相同 falsification 试验预算下，比 PSY-TaLiRo 实现了 83.5% 的更高成功率。Synthify 找到的安全违规也比 PSY-TaLiRo 更具多样性，覆盖了 137.7% 更多的子规范。