Contract verification with Auto FOCUS 3 using OCRA

Introduction

AF3 provides a deep integration of OCRA, a contract verification tool, with the following features:

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:
  1. Open the V&V dashboard tab below the editor
  2. Go to the OCRA contracts section
  3. Click on "Click to add a new contract". This creates a default contract:



  4. Now edit this contract to:





Now activate the OCRA check by following steps:
  1. Double click on the root of your project:


  2. 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: