AF3-OCRA is the FBK plugin designed for the Autofocus platform.
It adds the contract based composition paradigm to the Autofocus modeling tool providing the functionalities to edit, refine and check contracts.
For the check feature, AF3-OCRA interacts with OCRA which is the tool for the verification of logic-based contracts refinement for embedded systems
developed by FBK.