Mostrar el registro sencillo del ítem
dc.contributor.author
Cimatti, Alessandro
dc.contributor.author
Demasi, Ramiro Adrian
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.contributor.author
Tonetta, Stefano
dc.date.available
2019-12-03T17:29:15Z
dc.date.issued
2018-02
dc.identifier.citation
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
dc.identifier.issn
0925-9856
dc.identifier.uri
http://hdl.handle.net/11336/91228
dc.description.abstract
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.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Springer
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
CONTRACT-BASED DESIGN
dc.subject
OCRA
dc.subject
TEMPORAL LOGIC
dc.subject
PARAMETER SYNTHESIS
dc.subject.classification
Ciencias de la Computación
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
Ciencias de la Computación e Información
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.title
Tightening the contract refinements of a system architecture
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2019-10-22T17:51:32Z
dc.identifier.eissn
1572-8102
dc.journal.volume
52
dc.journal.number
1
dc.journal.pagination
88-116
dc.journal.pais
Alemania
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.description.fil
Fil: Cimatti, Alessandro. Fondazione Bruno Kessler; Italia
dc.description.fil
Fil: Demasi, Ramiro Adrian. Fondazione Bruno Kessler; Italia. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina
dc.description.fil
Fil: Tonetta, Stefano. Fondazione Bruno Kessler; Italia
dc.journal.title
Formal Methods In System Design
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/http://link.springer.com/10.1007/s10703-017-0312-9
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1007/s10703-017-0312-9
Archivos asociados