Finding Safety Violations of AI-Enabled Control Systems through the Lens of Synthesized Proxy Programs

• Published in: ACM transactions on software engineering and methodology 2025-01
• Main Authors: Shi, Jieke, Yang, Zhou, He, Junda, Xu, Bowen, Kim, Dongsun, Han, DongGyun, Lo, David
• Format: Article
• Language: English
• Subjects: Computing methodologies; Control methods; Search-based software engineering; Software and its engineering; Software testing and debugging
• ISSN: 1049-331X; 1557-7392
• DOI: 10.1145/3715105

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, i.e., control systems equipped with AI controllers. 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. Additionally, our method is 12.8 \(\times\) faster in finding a single safety violation than the baseline. The safety violations found by Synthify are also more diverse than those found by PSY-TaLiRo, covering 137.7% more sub-specifications.