kirancodes.me
To Proof Maintenance & Beyond!
ASE 2013

OCRA: A tool for checking the refinement of temporal contracts

Alessandro Cimatti, Michele Dorigatti, Stefano Tonetta

DOI 10.1109/ase.2013.6693137dblp

Abstract

Contract-based design enriches a component model with properties structured in pairs of assumptions and guarantees. These properties are expressed in term of the variables at the interface of the components, and specify how a component interacts with its environment: the assumption is a property that must be satisfied by the environment of the component, while the guarantee is a property that the component must satisfy in response. Contract-based design has been recently proposed in many methodologies for taming the complexity of embedded systems. In fact, contract-based design enables stepwise refinement, compositional verification, and reuse of components. However, only few tools exist to support the formal verification underlying these methods. OCRA (Othello Contracts Refinement Analysis) is a new tool that provides means for checking the refinement of contracts specified in a linear-time temporal logic. The specification language allows to express discrete as well as metric real-time constraints. The underlying reasoning engine allows checking if the contract refinement is correct. OCRA has been used in different projects and integrated in CASE tools.

BibTeX
@inproceedings{Cimatti-al:ASE13,
  author    = {Alessandro Cimatti and
               Michele Dorigatti and
               Stefano Tonetta},
  title     = {{OCRA:} A tool for checking the refinement of temporal contracts},
  booktitle = {ASE},
  pages     = {702--705},
  publisher = {{IEEE}},
  year      = {2013},
}

Related papers