Foundations and Trends® in Electronic Design Automation > Vol 12 > Issue 2-3

Contracts for System Design

Albert Benveniste, INRIA, France, albert.benveniste@inria.fr Benoît Caillaud, INRIA, France, benoit.caillaud@inria.fr Dejan Nickovic, Austrian Institute of Technology, Austria, Dejan.Nickovic@ait.ac.at Roberto Passerone, University of Trento, Italy, roberto.passerone@unitn.it Jean-Baptiste Raclet, IRIT, France, raclet@irit.fr Philipp Reinkemeier, Offis and University of Oldenberg, Germany, Philipp.Reinkemeier@offis.de Alberto Sangiovanni-Vincentelli, University of California at Berkeley, USA, alberto@eecs.berkeley.edu Werner Damm, Offis and University of Oldenburg, Germany, werner.damm@offis.de Thomas A. Henzinger, IST Austria, Austria, tah@ist.ac.at Kim G. Larsen, Aalborg University, Denmark, kgl@cs.aau.dk
 
Suggested Citation
Albert Benveniste, Benoît Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Alberto Sangiovanni-Vincentelli, Werner Damm, Thomas A. Henzinger and Kim G. Larsen (2018), "Contracts for System Design", Foundations and Trends® in Electronic Design Automation: Vol. 12: No. 2-3, pp 124-400. http://dx.doi.org/10.1561/1000000053

Published: 28 Mar 2018
© 2018 A. Benveniste et al.
 
Subjects
System Level Design,  Test,  Verification,  Program Verification,  Formal semantics
 
Keywords
System designContract based designComponent based designFormal semanticsInterfacesEmbedded systems
 

Free Preview:

Article Help

Share

Download article
In this article:
1. Introduction
2. Contracts: What? Where? And How?
3. Positioning of this Monograph and Bibliographical Note
4. A Mathematical Meta-Theory of Contracts
5. Assume/Guarantee Contracts
6. Synchronous Moore Interfaces and A/G Contracts
7. Rely/Guarantee Reasoning and A/G Contracts
8. Interface Theories
9. Scheduling Contracts
10. Contracts for Requirement Engineering
11. Contracts for Timing in Autosar
12. Conclusion
Acknowledgements
References

Abstract

Recently, 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.

DOI:10.1561/1000000053
ISBN: 978-1-68083-402-4
296 pp. $99.00
Buy book
 
ISBN: 978-1-68083-403-1
296 pp. $270.00
Buy E-book (.pdf)
Table of contents:
1. Introduction
2. Contracts: What? Where? And How?
3. Positioning of this Monograph and Bibliographical Note
4. A Mathematical Meta-Theory of Contracts
5. Assume/Guarantee Contracts
6. Synchronous Moore Interfaces and A/G Contracts
7. Rely/Guarantee Reasoning and A/G Contracts
8. Interface Theories
9. Scheduling Contracts
10. Contracts for Requirement Engineering
11. Contracts for Timing in Autosar
12. Conclusion
Acknowledgements
References

Contracts for System Design

Recently, 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. Several results have been obtained in this domain but a unified treatment of the topic that can help put contract-based design in perspective has been missing.

Contracts for System Design provides such a treatment where contracts are precisely defined and characterized so that they can be used in design methodologies with no ambiguity. It 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. This meta-theory provides deep and illuminating links with existing contract and interface theories, as well as guidelines for designing new theories. It encompasses contracts for both software and systems, with emphasis on the latter. Contracts for System Design illustrates 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.

 
EDA-053