Contract verification with Auto FOCUS 3 using OCRA
Introduction
AF3 provides a deep integration of OCRA, a contract verification tool, with the following features:
- user proximity: AF3 brings contract verification closer to its users. Contract refinement with
AF3 is easy to understand, easy to learn, simple and efficient to use.
- 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.
Prerequisite: OCRA
First ensure that OCRA is installed: see External Tools for instructions.
Example
Open the simple traffic light example and double-click on the Behavior component.
First we need to add a contract:
- Open the V&V dashboard tab below the editor
- Go to the OCRA contracts section
- Click on "Click to add a new contract". This creates a default contract:
- Now edit this contract to:
Now activate the OCRA check by following steps:
- Double click on the root of your project:
- And check "All OCRA contracts satisfied":
Be sure also that the configuration in which this check is activated is the one which is the "current objective".
You shall see that the check has automatically been run (and in this case provides a successful result). It is integrated with the constraint mechanism of AF3,
which means if the analysis is successful the user would not see anything, but if a contract verification fails then the user will see a red error marker on the component.
Additionally, the user can also see the status in the V&V dashboard:
Following is an example of failure in contract verification:
In the above figure the contract neverTrafficAndPedestrianSignal is not satisfied. The user can click on the failure status and is taken to the simulator where the counterexample (if provided by OCRA) can be simulated. Screenshot from such a simulation is shown below: