info:eu-repo/semantics/article
Tightening the contract refinements of a system architecture
Fecha
2018-02Registro en:
Cimatti, Alessandro; Demasi, Ramiro Adrian; Tonetta, Stefano; Tightening the contract refinements of a system architecture; Springer; Formal Methods In System Design; 52; 1; 2-2018; 88-116
0925-9856
1572-8102
CONICET Digital
CONICET
Autor
Cimatti, Alessandro
Demasi, Ramiro Adrian
Tonetta, Stefano
Resumen
Contract-based design is an emerging paradigm for correct-by-construction hierarchical systems: components are associated with assumptions and guarantees expressed as formal properties; the architecture is analyzed by verifying that each contract of composite components is correctly refined by the contracts of its subcomponents. The approach is very efficient, because the overall correctness proof is decomposed into proofs local to each component. However, the process for the contract specification and refinement is quite expensive because the requirements are formalized into formal properties, where part of the complexity is delegated to the designer, who has the burden of specifying the contracts. Typical problems include understanding which contracts are necessary, and how they can be simplified without breaking the correctness of the refinement and other refinements in case some subcontracts are shared. In this paper, we tackle these problems by proposing a technique to understand and simplify the contract refinements of a system architecture during the development process for the contract specification and refinement. The technique, called tightening, is based on parameter synthesis. The idea is to generate a set of parametric proof obligations, where each parameter evaluation corresponds to a variant of the original(s) contract refinement(s), and to search for tighter variants of the contracts that still ensure the correctness of the refinement(s). We cast this approach in the OCRA framework, where contracts are expressed with LTL formulas, and we evaluate its performance and effectiveness on a number of benchmarks.