Skip to main content
SpringerLink
Log in

Parallel and Multi-objective Falsification with Scenic and VerifAI

  • Conference paper
  • First Online:
Runtime Verification (RV 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12974))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Documentation of the extensions covered in this paper is available at: https://verifai.readthedocs.io/en/kesav-v-multi-objective/.

  2. 2.

    Full listing and source code of these Scenic scripts is available at: https://github.com/BerkeleyLearnVerify/Scenic/tree/kesav-v/multi-objective/examples/carla/Behavior_Prediction.

References

  1. Apollo: Autonomous Driving Solution. http://apollo.auto/. Accessed 22 July 2021

  2. The upper confidence bound algorithm, September 2016. https://banditalgs.com/2016/09/18/the-upper-confidence-bound-algorithm/

  3. Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12(2s) (2013). https://doi.org/10.1145/2465787.2465797

  4. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_21

    Chapter  MATH  Google Scholar 

  5. Araujo, H., Carvalho, G., Mousavi, M.R., Sampaio, A.: Multi-objective search for effective testing of cyber-physical systems. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 183–202. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30446-1_10

    Chapter  Google Scholar 

  6. Arrieta, A., Wang, S., Markiegi, U., Sagardui, G., Etxeberria, L.: Employing multi-objective search to enhance reactive test case generation and prioritization for testing industrial cyber-physical systems. IEEE Trans. Industr. Inf. 14(3), 1055–1066 (2018). https://doi.org/10.1109/TII.2017.2788019

    Article  Google Scholar 

  7. BerkeleyLearnVerify: Berkeleylearnverify/scenic. https://github.com/BerkeleyLearnVerify/Scenic

  8. BerkeleyLearnVerify: Berkeleylearnverify/verifai. https://github.com/BerkeleyLearnVerify/VerifAI

  9. Carpentier, A., Lazaric, A., Ghavamzadeh, M., Munos, R., Auer, P.: Upper-confidence-bound algorithms for active learning in multi-armed bandits. In: Kivinen, J., Szepesvári, C., Ukkonen, E., Zeugmann, T. (eds.) ALT 2011. LNCS (LNAI), vol. 6925, pp. 189–203. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24412-4_17

    Chapter  MATH  Google Scholar 

  10. Castro, L.I.R., Chaudhari, P., Tumova, J., Karaman, S., Frazzoli, E., Rus, D.: Incremental sampling-based algorithm for minimum-violation motion planning. CoRR abs/1305.1102 (2013). http://arxiv.org/abs/1305.1102

  11. Censi, A., et al.: Liability, ethics, and culture-aware behavior specification using rulebooks. CoRR abs/1902.09355 (2019). http://arxiv.org/abs/1902.09355

  12. Clopper, C.J., Person, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404–413 (1934). https://doi.org/10.1093/biomet/26.4.404

    Article  MATH  Google Scholar 

  13. Dosovitskiy, A., Ros, G., Codevilla, F., Lopez, A., Koltun, V.: CARLA: an open urban driving simulator. In: Proceedings of the 1st Annual Conference on Robot Learning, pp. 1–16 (2017)

    Google Scholar 

  14. Dreossi, T., et al.: VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 432–442. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_25

    Chapter  Google Scholar 

  15. Fremont, D.J., Chiu, J., Margineantu, D.D., Osipychev, D., Seshia, S.A.: Formal analysis and redesign of a neural network-based aircraft taxiing system with verifai. CoRR abs/2005.07173 (2020). https://arxiv.org/abs/2005.07173

  16. Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proceedings of the 40th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), June 2019

    Google Scholar 

  17. Fremont, D.J., et al.: Scenic: a language for scenario specification and data generation. CoRR abs/2010.06580 (2020). https://arxiv.org/abs/2010.06580

  18. Fremont, D.J., et al.: Formal scenario-based testing of autonomous vehicles: from simulation to the real world. In: 23rd IEEE International Conference on Intelligent Transportation Systems (ITSC), September 2020

    Google Scholar 

  19. Moritz, P., et al.: Ray: a distributed framework for emerging AI applications. CoRR abs/1712.05889 (2017). http://arxiv.org/abs/1712.05889

  20. Najm, W.G., Smith, J.D., Yanagisawa, M.: Pre-crash scenario typology for crash avoidance research, April 2007. https://www.nhtsa.gov/sites/nhtsa.gov/files/pre-crash_scenario_typology-final_pdf_version_5-2-07.pdf

  21. Qin, X., Aréchiga, N., Best, A., Deshmukh, J.V.: Automatic testing and falsification with dynamically constrained reinforcement learning. CoRR abs/1910.13645 (2019). http://arxiv.org/abs/1910.13645

  22. Ramezani, Z., Eddeland, J.L., Claessen, K., Fabian, M., Åkesson, K.: Multiple objective functions for falsification of cyber-physical systems. IFAC-PapersOnLine 53(4), 417–422 (2020)

    Article  Google Scholar 

  23. Rong, G., et al.: LGSVL simulator: a high fidelity simulator for autonomous driving. In: 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC), pp. 1–6 (2020).https://doi.org/10.1109/ITSC45102.2020.9294422

  24. Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 125–134. Association for Computing Machinery, New York (2012). https://doi.org/10.1145/2185632.2185653

  25. Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence. ArXiv e-prints, July 2016

    Google Scholar 

  26. Viswanadha, K., et al.: Addressing the IEEE AV test challenge with Scenic and VerifAI. In: The IEEE Third International Conference on Artificial Intelligence Testing (2021)

    Google Scholar 

  27. Viswanadha, K., Kim, E., Indaheng, F., Fremont, D.J., Seshia, S.A.: Parallel and multi-objective falsification with Scenic and VerifAI. CoRR abs/2107.04164 (2021). https://arxiv.org/abs/2107.04164

  28. Wishart, J., et al.: Driving safety performance assessment metrics for ADS-equipped vehicles, April 2020. https://doi.org/10.4271/2020-01-1206

  29. Zhang, Z., Arcaini, P., Hasuo, I.: Hybrid system falsification under (in) equality constraints via search space transformation. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 39(11), 3674–3685 (2020)

    Article  Google Scholar 

  30. Zhou, X., Gou, X., Huang, T., Yang, S.: Review on testing of cyber physical systems: methods and testbeds. IEEE Access 6, 52179–52194 (2018). https://doi.org/10.1109/ACCESS.2018.2869834

    Article  Google Scholar 

Download references

Acknowledgments

This work is partially supported by NSF grants 1545126 (VeHICaL), 1646208 and 1837132, by the DARPA contracts FA8750-18-C-0101 (AA) and FA8750-20-C-0156 (SDCPS), by Berkeley Deep Drive, and by Toyota under the iCyPhy center.

Author information

Authors and Affiliations

  1. University of California, Berkeley, USA

    Kesav Viswanadha, Edward Kim, Francis Indaheng & Sanjit A. Seshia

  2. University of California, Santa Cruz, USA

    Daniel J. Fremont

Authors
  1. Kesav Viswanadha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Edward Kim
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Francis Indaheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Daniel J. Fremont
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Sanjit A. Seshia
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kesav Viswanadha .

Editor information

Editors and Affiliations

  1. University of Virginia, Charlottesville, VA, USA

    Lu Feng

  2. Ben-Gurion University of the Negev, Be'er Sheva, Israel

    Dana Fisman

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Viswanadha, K., Kim, E., Indaheng, F., Fremont, D.J., Seshia, S.A. (2021). Parallel and Multi-objective Falsification with Scenic and VerifAI. In: Feng, L., Fisman, D. (eds) Runtime Verification. RV 2021. Lecture Notes in Computer Science(), vol 12974. Springer, Cham. https://doi.org/10.1007/978-3-030-88494-9_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-88494-9_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-88493-2

  • Online ISBN: 978-3-030-88494-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation