Welcome

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

7/02/2021
OCRA 2.1.0 is a major release that provides a new time domain.
Several bugs were also fixed.

More information here.
Download here .