Context and Problem Statement. Given the increasing adoption of modern AI-enabled control systems (e.g., autonomous vehicles, drones), 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 existing falsification methods struggle to cover comprehensively. In such contexts, developing a falsification framework tailored for AI-enabled control systems is of paramount importance.

Methodology. 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 𝜖-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. If a violation is spurious, Synthify refines the proxy program to perform more similarly to the original AI controller. Otherwise, it terminates the falsification process and report the found violations.

Evaluation. We compare Synthify 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 trial, and reveals 7.8× more safety violations than PSY-TaLiRo within the same time budget. Additionally, our method is 12.8× 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. The implementation of Synthify, along with datasets and raw results, has been made available at https://github.com/soarsmu/Synthify.

Future Work. Our work highlights several promising directions for future research, such as extending Synthify to AI-enabled control systems that handle more complex inputs like images. Another promising avenue is to integrate Synthify with other safety analysis techniques, such as runtime shields, to further enhance the reliability of AI-enabled control systems.

This paper has been accepted for publication in ACM Transactions on Software Engineering and Methodology (TOSEM) on January 14, 2025, and is available at https://doi.org/10.1145/3715105. Jieke Shi will be the presenting author.