Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development"

This archive contains supplementary material for the TACAS 2024 submission "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development".

Content

1. `planner.cpp`: The mock behavior planner described in the paper, used to control an automated car on the highway. (For demonstration purposes only! It is deliberately designed to violate major safety requirements.) The file can be compiled and run on its own, and it can be model-checked in the context of an environment model, as explained in the paper.
2. Two versions of the environment model which provide the surrounding traffic simulation for model-checking of the mock planner (or other custom behavior planners).
   • `EnvModel_3NONEGOS.smv`: With 3 non-ego cars, as used to illustrate the "Double Merge" issue in the paper.
   • `EnvModel_7NONEGOS.smv`: With 7 non-ego cars, as used to illustrate the "Gap Occlusion" issue in the paper.
3. `towards_safe_autonomous_driving_extended.pdf`: An extended version of the submitted paper containing an appendix with an in-depth description of how the transition system to model-check is created. The main part of the paper is identical with the submitted version (except for references into the appendix).
4. `LICENSE.txt`: The license under which the files are provided.

NOTE: This archive will be allowed public access to in case of acceptance at TACAS.