Hypercontracts

TL;DR

This paper introduces hypercontracts, a comprehensive and flexible model for component-based system design that extends existing contract theories with richer algebraic structures and finite descriptions.

Contribution

It proposes hypercontracts, a novel, more expressive model that generalizes simulation preorders and enhances algebraic operations for system refinement and composition.

Findings

Hypercontracts provide a richer algebra for component refinement.

Conic hypercontracts offer a finite, implementable description.

The model subsumes existing simulation preorders.

Abstract

Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. 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 inclusion of new operations. On top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description.