Welcome to the home page of OCRA, a command-line tool for the verification of logic-based contract refinement for embedded systems.
It supports the specification and analysis of component-based specifications of system architectures.
Components are enriched with contracts specified in discrete or hybrid linear-time temporal logics.
OCRA is developed by the Embedded Systems Unit of FBK.
It is built on top of the nuXmv and HyCOMP model checkers.
It is also integrated in the modeling tool AutoFOCUS3 through the AF3-OCRA plugin.

Latest release

OCRA 1.4.0 is a major release that provides six new commands, a new port type, handy extensions of the input language, the Mac OS X executable, and several bug fixes.
More information here.
Download here.