AF3-OCRA
is a 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.