AF3 provides a integration of the CProver model checkers CBMC and SATABS 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.
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.
To use the CProver model checking functionality in AF3, firstly we have to install the CBMC and/or SATABS model checkers (download can be found here for CBMC and here for SATABS).
For Linux and MasOS:
You only have to make sure that CBMC and/or SATABS is in the PATH.
For Windows:
1. Make sure, that the folders in which your CBMC and/or SATABS binary files are contained in, are in the Path environment variable.
2. All CProver model checkers require to be able to access a c compiler, thus you have to make sure a compiler is available. AF3 provides support for Cygwin (with gcc installed) or Microsoft Visual Studio (Visual Studio Express is sufficient).
For Cygwin, make sure that Cygwin's bin folder is in the Path environment variable.
For Visual Studio, add the folder which contains VsDevCmd.bat to the Path environment variable. Usually, this is something like C:\Program Files\Microsoft Visual Studio 11.0\Common7\Tools.
To
check whether AF3 can access CBMC and/or
SATABS,
just press the "CProver Version" button from the "CProver
Analyses View". If CBMC and/or
SATABS
are
correctly installed, a dialog showing its version is displayed (as
below), otherwise an error message will be displayed.
Step
1 - Open the "CProver Analyses" view by clicking on
the button from the toolbar.
Step 2 - Performing 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).
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.