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 2.0.0 is a major release that provides a major extension of the OCRA language, namely the possibility to parametrize OCRA architectures using parameters to define the number of subcomponents, ports, and more.
New commands have been added to validate the contract specification, synthesizing tightened versions and debugging the contracts using input traces.
Several bugs were also fixed.

More information here.
Download here.