Overview
This work introduces the PRoBify framework, a probabilistic programming approach for modeling behavioral uncertainty and verifying safety properties of AVs in the presence of the uncertainty. We describe a probabilistic programming language for specifying behavior spaces that capture uncertainty of driver behaviors. We then show how behaviors can be sampled from the behavior space to discover safety violations in the AV under study. We present several use cases that apply the proposed framework in traffic scenarios based on real-world data to demonstrate how PRoBify can discover unintuitive but plausible and dangerous AV failures.
Data flow diagram for PRoBify framework
Metamodel of PRoBify language
Results
We illustrate the PRoBify framework in several illustrative use cases based on real-world traffic scenarios. We provide video demonstrations for the PRoBify-discovered counterexamples below.
Busy Event Parking (see Figure 5, Manuscript)
Counterexample for Busy Event Parking (see Figure 6, Manuscript)
Irregular Intersection (see Figure 7, Manuscript)
Counterexample 1: Rapid Merge (see Figure 8(a), Manuscript)
Counterexample 2: Sharp Turn (see Figure 8(b), Manuscript)
Counterexample 3: Stop and Go (see Figure 8(c), Manuscript)
Interactive Sandbox
Interactive sandbox for exploring the PRoBify language. Select an example PRoBify program in the left panel. Click "Sample" to generate an instance of the corresponding concrete program. Note: Our experiments use an external simulator (Metadrive) to execute a concrete program. As the PRoBify framework is intended to be simulator-agnostic, we provide a sandbox for exploring the key features of the language, while the choice of simulation platform is up to the end user.