The following functionalities are visible from the OCRA perspective.

Check Contract

Refinement

The contract refinement check can be performed from both the Model Navigator and Contract Navigator.

From the Model Navigator, select the Contracts item just below the component and choose the Refine Contract menu ...

Contracts Refinement Check


From the Contract Navigator, select the Contract and choose the Refine Contract menu ...

Contract Refinement Check

Implementation

The contract implementation check can be performed from both the Model Navigator and Contract Navigator in a quite similar
way
to the refinement check.

If the component which owns the contract doesn't have an implementation, the check is not admitted and a message error is shown.

Missing Implementation

Check Result

Once the check is completed, the result is displayed in the Contract Navigator by means of colored contract icons.
(gray no check has been performed, green success and red failure)

Contract Navigator Check Result


Selecting the wrong contract and invoking the Show Contract Result menu, yuo can see the detailed result on the right bottom side.

Check Trace

AF-OCRA has been developed and is mantained by:
Embeded System