Model Checking with AF3

Model checking with Auto FOCUS 3

Introduction

AF3 provides a deep integration of the NuSMV model checker 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.

Installing NuSMV

To use the model checking functionality in AF3, firstly we have to install the NuSMV model checker. You only have to make sure that NuSMV is in the PATH. To check whether AF3 can access the NuSMV, just press the "NuSMV Version" button from the "Semantic Inspector View". If NuSMV is correctly installed, a dialog showing its version is 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.