Parallel and Multi-Objective Falsification with Scenic and VerifAI
This work addresses efficiency and specification challenges in verifying autonomous systems, though it is incremental as it builds on existing tools.
The paper tackles the scalability and expressiveness limitations of simulation-based falsification for autonomous systems by introducing parallel execution and multi-objective optimization into the Scenic and VerifAI frameworks, resulting in reduced execution times and enhanced counterexample search capabilities.
Falsification has emerged as an important tool for simulation-based verification of autonomous systems. In this paper, we present extensions to the Scenic scenario specification language and VerifAI toolkit that improve the scalability of sampling-based falsification methods by using parallelism and extend falsification to multi-objective specifications. We first present a parallelized framework that is interfaced with both the simulation and sampling capabilities of Scenic and the falsification capabilities of VerifAI, reducing the execution time bottleneck inherently present in simulation-based testing. We then present an extension of VerifAI's falsification algorithms to support multi-objective optimization during sampling, using the concept of rulebooks to specify a preference ordering over multiple metrics that can be used to guide the counterexample search process. Lastly, we evaluate the benefits of these extensions with a comprehensive set of benchmarks written in the Scenic language.