Hypercontracts

Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2021-158
May 31, 2021

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-158.pdf

Contracts (or interface) theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. Over the last decades, a number of formalisms were proposed, sometimes very different in their form and algebra. This motivated the quest for a unification by some authors, e.g., specifications through contracts by Bauer et al. and the contract metatheory by Benveniste et al. to cite a few. These generic models establish precise links between the different contract frameworks. In this paper we propose hypercontracts, a generic model with a richer structure for its underlying model of components, subsuming simulation preorders. While this new model remains generic, it provides a much more elegant and richer algebra for its key notions of refinement, parallel composition, and quotient, and it allows considering new operations. On top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description. We show how to specialize conic hypercontracts to Assume-Guarantee contracts as well as to Interface Automata, two known contract frameworks very different in style. We illustrate conic hypercontracts on specifications involving security and the robustness of machine-learning components.


BibTeX citation:

@techreport{Incer:EECS-2021-158,
    Author = {Incer, Inigo and Benveniste, Albert and Sangiovanni-Vincentelli, Alberto L. and Seshia, Sanjit A.},
    Title = {Hypercontracts},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2021},
    Month = {May},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-158.html},
    Number = {UCB/EECS-2021-158},
    Abstract = {Contracts (or interface) theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. Over the last decades, a number of formalisms were proposed, sometimes very different in their form and algebra. This motivated the quest for a unification by some authors, e.g., specifications through contracts by Bauer et al. and the contract metatheory by Benveniste et al. to cite a few. These generic models establish precise links between the different contract frameworks. In this paper we propose hypercontracts, a generic model with a richer structure for its underlying model of components, subsuming simulation preorders. While this new model remains generic, it provides a much more elegant and richer algebra for its key notions of refinement, parallel composition, and quotient, and it allows considering new operations. On top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description. We show how to specialize conic hypercontracts to Assume-Guarantee contracts as well as to Interface Automata, two known contract frameworks very different in style. We illustrate conic hypercontracts on specifications involving security and the robustness of machine-learning components.}
}

EndNote citation:

%0 Report
%A Incer, Inigo
%A Benveniste, Albert
%A Sangiovanni-Vincentelli, Alberto L.
%A Seshia, Sanjit A.
%T Hypercontracts
%I EECS Department, University of California, Berkeley
%D 2021
%8 May 31
%@ UCB/EECS-2021-158
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-158.html
%F Incer:EECS-2021-158