Dynamic, Multi-Objective Specification and Falsification of Autonomous CPS

Kevin Kai-Chun Chang, Kaifei Xu, Edward Kim, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. Dynamic, Multi-Objective Specification and Falsification of Autonomous CPS. In International Conference on Runtime Verification (RV), pp. 40–58, Springer, October 2024.

Download

[pdf] 

Abstract

Simulation-based falsification has proved to be an effective verification method for cyber-physical systems. Traditional approaches to falsification take as input a single or a set of temporal properties that must be satisfied by the system at all times. In this paper, we consider falsification of a more complex specification with two dimensions: multiple objectives with relative priorities and the evolution of these objectives characterized by time-varying priorities. We introduce the concept of dynamic rulebooks as a way to specify a prioritized multi-objective specification and its evolution over time. We develop a novel algorithm for falsifying a dynamic rulebook specification on a cyber-physical system. To evaluate our approach, we define scenarios and dynamic rulebook specifications for the domains of autonomous driving and human-robot interaction. Our experiments demonstrate that integrating dynamic rulebooks allows us to capture counterexamples more accurately and efficiently than when using static rulebooks. Moreover, our falsification framework identifies more numerous and more significant counterexamples as compared to previous approaches.

BibTeX

@InProceedings{chang-rv24,
author="Chang, Kevin Kai-Chun and Xu, Kaifei and Kim, Edward and Sangiovanni-Vincentelli, Alberto and Seshia, Sanjit A.",
editor="{\'A}brah{\'a}m, Erika and Abbas, Houssam",
title="Dynamic, Multi-Objective Specification and Falsification of Autonomous {CPS}",
booktitle="International Conference on Runtime Verification (RV)",
year="2024",
month=oct,
publisher="Springer",
pages="40--58",
abstract="Simulation-based falsification has proved to be an effective verification method for cyber-physical systems. Traditional approaches to falsification take as input a single or a set of temporal properties that must be satisfied by the system at all times. In this paper, we consider falsification of a more complex specification with two dimensions: multiple objectives with relative priorities and the evolution of these objectives characterized by time-varying priorities. We introduce the concept of dynamic rulebooks as a way to specify a prioritized multi-objective specification and its evolution over time. We develop a novel algorithm for falsifying a dynamic rulebook specification on a cyber-physical system. To evaluate our approach, we define scenarios and dynamic rulebook specifications for the domains of autonomous driving and human-robot interaction. Our experiments demonstrate that integrating dynamic rulebooks allows us to capture counterexamples more accurately and efficiently than when using static rulebooks. Moreover, our falsification framework identifies more numerous and more significant counterexamples as compared to previous approaches.",
}