Model checking with Auto FOCUS 3
AF3 provides a deep integration of the NuSMV model checker, and of its successor nuXmv,
with the following features:
- user proximity: AF3 brings model checker closer to its users. Model checking with
AF3 is easy to understand, easy to learn, simple and efficient to use.
- easy to specify properties: AF users can work at the abstraction level of AF3 models.
- analyses results are easy to interpret. Counter-examples can be simulated in AF3 such that
the users gain an immediate feedback about the causes that brought the property violation.
First ensure that nuXmv or NuSMV is installed: see External Tools for instructions.
You need to ensure that the reachability check is activated:
Be sure also that the configuration in which this check is activated is the one which is the "current objective".
- Double click on the root of your project:
- And check "All states are reachable":
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.
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.