Contracts for System Design
A group of prominent CPS researchers in Europe published a monograph on contract-based design to cope with the complexity of CPS.
Contracts for System Design
https://www.nowpublishers.com/article/Details/EDA-053
Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier,
Alberto Sangiovanni-Vincentelli, Werner Damm, Thomas A. Henzinger, and Kim G. Larsen
Contract-based design has been proposed as an “orthogonal” approach that complements system design methodologies proposed so far to cope with the complexity of system design. Contract-based design provides a rigorous scaffolding 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.
The table of contents follows:
- Introduction, industrial context
- Contract based design, a primer on contracts
- Positioning of this monograph and bibliographical note
- A mathematical meta-theory of contracts
- Assume/Guarantee contracts
- Synchronous Moore Interfaces and Assume/Guarantee contracts
- Rely/Guarantee reasoning and Assume/Guarantee contracts
- Interface theories: interface automata and modal interfaces
- Scheduling contracts and contracts for timing
- Contracts in Requirement Engineering
- Contracts for timing in Autosar
- Conclusion, status of research, status of practice