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: Contracts for System Design
now Publishers Inc., 2018, 296 pages, ISBN 978-1-68083-402-4
While a number of theoretical contract frameworks have been proposed in the literature, missing has been a formal statement of what is required in defining a contract theory. This book addresses that gap, presenting a thorough mathematical treatment of contracts with the development of a new meta-theory for contracts as the foundation. That meta-theory is used to provide an understanding of several contract frameworks, allowing the reader to see how each framework fits into the meta-theory and to assess similarities and differences between the individual frameworks.
This review is written by Elizabeth I. Leonard for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community. The review will also appear in Formal Aspects of Computing.
Contracts for System Design
by A. Benveniste et al.
While a number of theoretical contract frameworks have been proposed in the literature, missing has been a formal statement of what is required in defining a contract theory. This book addresses that gap, presenting a thorough mathematical treatment of contracts with the development of a new meta-theory for contracts as the foundation. That meta-theory is used to provide an understanding of several contract frameworks, allowing the reader to see how each framework fits into the meta-theory and to assess similarities and differences between the individual frameworks. Originally published in the journal Foundations and Trends in Electronic Design Automation [FTEDA18], the book is written for readers who want an in-depth, mathematical understanding of contracts. While it does contain a pair of examples illustrating how contracts can be used in the system development process, this is not a book for practitioners looking for a detailed, step-by-step tutorial on how to use contract-based design.
After some general background on contract-based design and an overview of the book’s structure and technical contributions, the book presents an overview of the elements that are needed to define a contract theory. The basic concepts of implementations, environments, and components are defined and illustrated using a simple example. Operations on contracts are also introduced, including composition for component-based design, refinement for substituting one implementation of a system or component for another, and conjunction for merging contracts from different viewpoints of the same system or component. Written in a style that is accessible to non-experts, this chapter provides a good overview of the basic concepts that will be used later in the book.
After the introductory material, the book presents its main technical contribution, a meta-theory of contracts. In the meta-theory, a contract is defined by a pair of sets, one containing correct implementations and the other containing legal environments. The meta-theory then formally defines refinement, conjunction, and composition. The meta-theory strives to be as general as possible, making no assumptions about how contracts, implementations, and environments are specified. This allows the meta-theory to be instantiated by a wide variety of contract frameworks.
Next, the book dedicates several chapters to discussions of different contract frameworks. Each chapter describes a framework and then relates the theory for that framework to the meta-theory. Each chapter also contains extensive bibliographical notes, discusses relationships among the frameworks, and identifies open questions. Individual chapters cover Assume Guarantee contracts, Synchronous Moore Interfaces, Rely/Guarantee reasoning, Interface theories including Interface Automata and Modal Interfaces, and scheduling contracts. These chapters are best-suited to readers with some prior familiarity with at least one of the frameworks covered in the book. While each chapter contains a brief overview of its associated framework, it is not a tutorial on that formalism. I would recommend that readers with some background in one or more contract frameworks begin with the framework with which they are most familiar to get comfortable with the basic structure used by the book and then move on to the chapters for less familiar frameworks.
The book also includes descriptions of two applications of contracts in the design of systems. The first application uses Modal Interfaces to illustrate how formal contracts can be used to specify requirements at both the system level and component level, with a simple parking garage as the example. The chapter includes a synthesis method for generating contracts for the individual components from the system requirements and the sub-system architecture. The second application focuses on timing and scheduling contracts in the AUTOSAR automotive development process. Scheduling contracts are used to specify top level timing requirements and then refined to timing subcontracts for subcomponents. Resources are assigned to individual tasks performed by the subcomponents, producing resource-aware contracts for the individual components.
If you want to gain a deeper understanding of formal contract theory, this book will provide that, but you will have to work for that understanding. The book is a dense mathematical treatment, moving quickly from one definition or theorem to the next. While examples are provided for some of the contract frameworks, they are generally used only to introduce the formalism and are not carried through the chapters. Unfortunately, the book also suffers from a lack of careful editing. While many of these errors are easy to ignore, particular difficulty arose with some of the typographical errors in the mathematics. In these cases, I spent significant time puzzling over the text and working out the mathematics myself to figure out what the text was supposed to say. Hopefully, these errors will be corrected in future editions of this book to make it more accessible to readers.
[FTEDA18] Benveniste A, Caillaud B, Nickovic D, Passerone R, Raclet J-B, Reinkemeier P, Sangiovanni-Vincentelli A, Damm W, Henzinger TA, and Larsen KG. Contracts for system design. Foundations and Trends in Electronic Design Automation, 12(2-3): 124–400, 2018.