Parallel and Multi-Objective Falsification with Scenic and VerifAI

Kesav Viswanadha, Edward Kim, Francis Indaheng, Daniel J. Fremont, and Sanjit A. Seshia. Parallel and Multi-Objective Falsification with Scenic and VerifAI. In 21st International Conference on Runtime Verification (RV), pp. 265–276, Lecture Notes in Computer Science 12974, Springer, 2021.

Download

[pdf] 

Abstract

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.

BibTeX

@inproceedings{viswanadha-rv21,
  author    = {Kesav Viswanadha and
               Edward Kim and
               Francis Indaheng and
               Daniel J. Fremont and
               Sanjit A. Seshia},
  title     = {Parallel and Multi-Objective Falsification with {Scenic} and {VerifAI}},
  booktitle = {21st International Conference on Runtime Verification (RV)},
  series    = {Lecture Notes in Computer Science},
  volume    = {12974},
  pages     = {265--276},
  publisher = {Springer},
  year      = {2021},
  abstract  = {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.},
}