Integration of Formal Specification and Traffic Simulation for Scenario-Based Validation.

Scenario-based testing has been used for validation and verification of autonomous vehicles in various settings. In these efforts, simulation platforms are extensively utilized to run and analyze test scenarios, which is crucial for the validation of perception, decision-making and action in different traffic situations. Providing formal specification for scenarios used in these simulations is also critical for standardization, repeatability and verification. In this paper, we propose an approach which integrates an open-source network-based traffic simulator with an open-source formal scenario description language designed for formal scenario specification of autonomous vehicle validation scenarios. This approach provides the capability to describe, generate, and share abstract traffic scenarios for validation. It also allows integration with higher fidelity or physical testing methods as it utilizes a widely used scenario specification methodology. We provide an integration of formal specification and traffic simulation and also show the potential of such an integration through simulation examples.