Model Checking for Autonomous Vehicles (NuSMV demo)

Abstract

In this lesson a simple highway lane controller is modelled using the specification language of the well-known NuSMV model checker. Then, some interesting properties are first formalized using temporal logics (LTL/CTL), and then verified on the previously defined model.

Additional notes

The model file is available here.