Given the increasing adoption of modern AI-enabled control systems, ensuring their safety and reliability has become a critical task in software testing. One prevalent approach to testing control systems is falsification, which aims to find an input signal that causes the control system to violate a formal safety specification using optimization algorithms. However, applying falsification to AI-enabled control systems poses two significant challenges: (1)~it requires the system to execute numerous candidate test inputs, which can be time-consuming, particularly for systems with AI models that have many parameters, and (2)~multiple safety requirements are typically defined as a conjunctive specification, which is difficult for existing falsification approaches to comprehensively cover. This paper introduces Synthify, a falsification framework tailored for AI-enabled control systems. Our approach performs falsification in a two-phase process. At the start, Synthify synthesizes a program that implements one or a few linear controllers to serve as a proxy for the AI controller. This proxy program mimics the AI controller's functionality but is computationally more efficient. Then, Synthify employs the $\epsilon$-greedy strategy to sample a promising sub-specification from the conjunctive safety specification. It then uses a Simulated Annealing-based falsification algorithm to find violations of the sampled sub-specification for the control system. To evaluate Synthify, we compare it to PSY-TaLiRo, a state-of-the-art and industrial-strength falsification tool, on 8 publicly available control systems. On average, Synthify achieves a 83.5% higher success rate in falsification compared to PSY-TaLiRo with the same budget of falsification trials. The safety violations found by Synthify are also more diverse than those found by PSY-TaLiRo, covering 137.7% more sub-specifications.

翻译：随着现代人工智能赋能控制系统日益普及，确保其安全性与可靠性已成为软件测试中的关键任务。测试控制系统的一种主流方法是**证伪测试**，其旨在利用优化算法寻找导致控制系统违反形式化安全规约的输入信号。然而，将证伪测试应用于人工智能赋能控制系统面临两大挑战：(1) 该方法需要系统执行大量候选测试输入，这可能非常耗时，尤其对于包含多参数AI模型的系统；(2) 多重安全要求通常被定义为合取规约，现有证伪方法难以全面覆盖。本文提出Synthify——一个专为人工智能赋能控制系统设计的证伪框架。我们的方法采用两阶段流程执行证伪：首先，Synthify合成一个实现单个或多个线性控制器的程序，作为AI控制器的代理。该代理程序能模拟AI控制器的功能，同时具有更高的计算效率；随后，Synthify采用$\epsilon$-贪婪策略从合取安全规约中采样具有潜力的子规约，并运用基于模拟退火的证伪算法来发现控制系统对采样子规约的违反情况。为评估Synthify，我们在8个公开可用的控制系统上将其与工业级先进证伪工具PSY-TaLiRo进行对比。在相同证伪试验预算下，Synthify平均获得比PSY-TaLiRo高83.5%的证伪成功率。同时，Synthify发现的安全违规行为更具多样性，其覆盖的子规约数量比PSY-TaLiRo多137.7%。