CProver based model checking with Auto FOCUS 3

Introduction

AF3 provides a integration of the CBMC 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.

• 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.

Installing CBMC

To use the CProver model checking functionality in AF3, firstly we have to install the CBMC model checker (download can be found here).

For Linux and MasOS:

You only have to make sure that CBMC is in the PATH.

For Windows:

1.    Make sure, that the folder in which your CBMC binary files are contained in, is in the Path environment variable.

2.    CBMC requires 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 the CBMC, just press the "CProver Version" button from the "CProver Analyses View". If CBMC 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 "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.