The following functionalities are visible from the OCRA perspective.

Edit Contract

To create new contracts, select the component and choose the Edit Contract menu ...

Edit New Contract


To edit contracts, select the Contracts node just below the component and double click or choose the Edit Contract menu ...

Edit Contract


... and on the right side will be opened the Contract Editor.

Contract Editor

The contract editor provides several hints to facilitate the specification of the contract: keywords, ports, patterns.
To define patterns, refer to AF3 Help at the Temporal Logic Specifications section.

Contract Editor Hints

If a pattern was chosen, it is displayed by its type name (uppercase, between brackets and colored). If hovered, the equivalent LTL formula is shown.

Contract Editor Hints

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