Model Checking for ADAS

This is the open source project very fast math, first announced in Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development. We hereby make all the sources of the toolchain public which have so far been published in binary format only (on Zenodo).

Thank you for using

         ___           
.--.--..'  _|.--------.
|  |  ||   _||        |
 \___/ |__|  |__|__|__|
   very fast math

VFM Library

vfm is a formal verification software for ADAS with the nuXmv model checker in its core. It can parse C++ code of an automated driving function (or other) and translate it into a transition system for the nuXmv model checker. Optionally, it can be integrated with an environment model, providing a discrete traffic simulation for the driving function to be verified against. The resulting counterexamples can be visualized and converted into the OSC2 format.

Examples

MC-generated traffic situation on highway

MC-generated road network and traffic situation

Ultra-cooperative driving: live steering of a fleet by model checker

Steered by the MC, a fleet of cars provably* obeys a given SPEC, in this case: invert ordering without colliding. Entrance file: morty/morty.py. (* given a whole bunch of assumtions 😉)

How to build

vfm is implemented in C++ and can be built with CMake (stable) or Bazel (experimental). With CMake, proceed as follows:

• On Windows, open the top-level CMakeLists.txt with Visual Studio and build the vfm target.
• On Linux, run the build.bash script.

Run vfm(.exe) from the bin folder.

There are no additional dependencies, except gtest if you want to run the tests.

Authors

Lukas Koenig, Alexander Georgescu, Christian Heinzemann, Christian Schildwaechter, Michaela Klauck, Henning Koch