Contracts for System Design

Description

Recently, contract-based design has been proposed as an "orthogonal" approachthat complements system design methodologies proposed so far tocope with the complexity of system design. Contract-based design providesa rigorous scaffolding for verification, analysis, abstraction/refinement, andeven synthesis. Several results have been obtained in this domain buta unified treatment of the topic that can help put contract-based design inperspective has been missing. Contracts for System Design provides such a treatmentwhere contracts are precisely defined and characterized so that they canbe used in design methodologies with no ambiguity. It identifies the essence of complex system design using contracts througha mathematical "meta-theory", where all the properties of the methodologyare derived from a very abstract and generic notion of contract. This meta-theory provides deep and illuminating links with existing contractand interface theories, as well as guidelines for designing new theories. It encompasses contracts for both software and systems, with emphasison the latter. Contracts for System Design illustrates the use of contracts with two examples: requirementengineering for a parking garage management, and the development ofcontracts for timing and scheduling in the context of the AUTOSAR methodologyin use in the automotive sector.