Contracts for System Design
Today, early phases of system design rely on requirement engineering, a task consisting in listing, as requirements, what is expected from the system under design. Requirements are mostly informal and text-based, or, at best, are supported in part by predefined patterns of properties (such as in boiler plate models). There is a stringent need to develop better formal support for this early system design phase. Contract-based design has this in its objectives.
Contract-based design was promoted by Bertrand Meyer in the early 90’s for software systems. The basic idea is that a software component should be developed having in mind two pieces of information: what is expected from the component (its guarantees), and what is expected from the context in which the component will operate (its assumptions). Such pairs {assumptions, guarantees} are called contracts. In the early 2000’s, contract-based design was extended to the design of systems in their whole, including their cyber-physical aspects. This required developing contracts for frameworks such as automata and their variants, and then, for hybrid systems (the mathematical model behind Simulink). First results in these directions were proposed around 2000 by Henzinger et al. with interface automata, a specification framework for automata, in which assumptions and guarantees are folded into a single entity by using modalities such as must and may as labels of transitions. Since the year 2006, Albert Benveniste and Benoît Caillaud developed research on this topic, participating to an international effort gathering T. Henzinger, K. Larsen, W. Damm, and A. Sangiovanni-Vincentelli, among others.
A major contribution of our team in this topic is the collective monograph Contracts for System Design, published in 2018. This monograph reviews and explains Assume/Guarantee contracts and interface theories, and proposes a generic framework called Contract Meta-Theory, encompassing all contract frameworks known so far, including the ones developed in the area of software engineering. In this meta-theory, a contract is simply viewed as a set of possible components (implementations) and a set of legal contexts (environments) for the considered component. Contracts are equipped with refinement order, parallel composition, and quotient. Contracts support independent development of subsystems by suppliers, and the possibility to develop different aspects or viewpoints of the system (function, timing, resource…) and to fuse them, with a guaranteed correct subsequent integration. In this monograph, we develop an illustration case on requirement engineering. The system level contract is developed using modal interfaces. A SysML-like specification of the system architecture is then combined with the system-level contract, from which subcontracts for the different suppliers are synthesized, with guaranteed correct system integration. This use case is way ahead of current practical use of contracts, but it illustrates how far one could go.
Currently, our team focuses on two derived topics. First, we work on proposing probabilistic contract framework aiming at providing a formal specification support for Probabilistic Programming. Second, we remain interested in using contracts for requirement engineering, in particular, DAE-based contracts for physical systems specification.
Participants
Albert Benveniste, Benoît Caillaud.
Publications
The list of publications about this topic can be found here.
Software
The MICA software, implementing the Modal Interface algebra in OCaml, is described here.
