A Temporal Logics Approach to Contract-Based Design
Alessandro Cimatti, Stefano Tonetta · 2016
OCRA provides a language and tool support to model and analyze a component-based architecture enriched with contracts. Assumptions and guarantees of components are specified in different variants of linear-time temporal logics, supporting variables with infinite domains and continuous dynamics. The tool provides different analysis techniques including contracts refinement checking, contract-based compositional reasoning, contract-based fault-tree generation, and validation of the contracts specification. It has been recently integrated with COMPASS to support the contract-based analysis of AADL models.