Model checking with Auto FOCUS 3
Introduction
New in 2.9.0! AF3 now supports nuXmv!
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.
- advanced verification: We offer support for advanced modeling languages integrated with AF3,
many of them having a non-trivial translation in NuSMV (in this manner we empower the AF3 user
both to work with rich modeling language and do verification) ,
- easy to specify properties: AF users can work at the abstraction level of AF3 models.
- out-of-the-box analyses that make use of model-checking (e.g. detection of
unreachable states)
- verification patterns, that correspond to frequently encountered
verification properties;
- 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.
Note: Integration of NuSMV/nuXmv is undergoing a lot of refactorings in order to support more features; planned for AF3 2.10!
Installing NuSMV or nuXmv
To use the model checking functionality of AF3, you need to install the NuSMV
model checker or its successor nuXmv. You only have to make sure that either of these software is in the PATH. To check whether
AF3 can access the model checker, just press the "NuSMV/nuXmv Version" button from the
"Semantic Inspector View". If correctly installed, a dialog showing the version
will be displayed (as below), otherwise an error message will be displayed.
Using the "Semantic Inspector"
- Step 1 - Open the "Semantic Inspector" view by clicking on the button from the toolbar.
- Step 2 - Choose the "Basic use" or the "Advanced use" tab. The "Basic use" tab offers
one-click, out-of-the-box analyses, the "Advanced use" tab lets the user specify desired properties
on AF model.
- Step 3 - Performing basic analyses
- Step 3.1 - Select a component in the navigator view or in a diagram.
- Step 3.2 - Press "Find unreachable states" button. In case when unreachable states are found,
they will be shown in the table below the button.
- Step 3.3 - By double-clicking on the table, the editor containing the
corresponding state automaton will be opened and the unreachable state will be highlighted.
- Step 4 - Performing advanced analyses
- Step 4.1 - Select a component in the navigator view or in a diagram.
- Step 4.2 - Select a verification context from the 'Verification Context' combo
(the verification context indicates the part of the model that will be used for verification;
selecting a context bigger than the component to be checked helps to restrict the set of input values for the checked component
because the model checker will not consider all input values but only those possible according to the selected context).
All assumptions attached to the component selected as verification context (for more information about attaching assumptions
to a component see the help page for Contracts Specification View)
are taken into account when the verification is performed.
- Step 4.2 - Write the condition to be checked in one of the fields from below and by using the same syntax
as for specifying guards for transitions. In case of failure a counterexample will be displayed.
- Step 4.3 - The counterexample can be opened in the simulator. By clicking on the "next step" simulator button,
the simulator will replay the counterexample until it reaches the desired state when the simulation ends and can be replayed
from the beginning.