, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet,
Philipp Reinkemeier, Alberto Sangiovanni-Vincentelli, Werner Damm, Thomas A. Henzinger, and Kim G. Larsen
Recently, contract-based design has been proposed as an "orthogonal" approach
that complements system design methodologies proposed so far to
ope with the complexity of system design. Contract-based design provides
a rigorous scaolding for verification, analysis, abstraction/refinement, and
even synthesis. A number of results have been obtained in this domain but
a unified treatment of the topic that can help put contract-based design in
perspective was missing. This monograph intends to provide such a treatment
where contracts are precisely defined and characterized so that they can
be used in design methodologies with no ambiguity. In particular, this monograph
identifies the essence of complex system design using contracts through
a mathematical "meta-theory", where all the properties of the methodology
are derived from a very abstract and generic notion of contract. We show that
the meta-theory provides deep and illuminating links with existing contract
and interface theories, as well as guidelines for designing new theories. Our
study encompasses contracts for both software and systems, with emphasis
on the latter. We illustrate the use of contracts with two examples: requirement
engineering for a parking garage management, and the development of
contracts for timing and scheduling in the context of the Autosar methodology
in use in the automotive sector.