Model checking with Auto FOCUS 3

Introduction

AF3 provides a deep integration of the NuSMV model checker, and of its successor nuXmv, with the following features:

Prerequisite: NuSMV/nuXmv

First ensure that nuXmv or NuSMV is installed: see External Tools for instructions.

Activation

You need to ensure that the reachability check is activated:
  1. Double click on the root of your project:


  2. And check "All states are reachable":


Be sure also that the configuration in which this check is activated is the one which is the "current objective".

This will trigger the check that all state automata of the project have 100% state coverage and activate the automatic trigger of this check for every state automaton that you might add later on to your project. It will also trigger a check for every state automaton as soon as it is modified.

Example

Open the simple traffic light example and double-click on the Controller component. Open the V&V dashboard tab below the editor and add a specification as follows:



You shall see that the check has automatically been run (and in this case provides a successful result). In case of failure:



Double-clicking the status message will start a simulation demonstrating the coutner-example.