From specifications to contracts

Roberto Passerone / Persyval-Lab

The specification of a system or a component is usually expressed in terms of what the properties that the system in question should satisfy, and/or what it should do. In the last decade, a new form of specification has emerged which defines both the properties of the system as well as its assumptions on the context in which the system is used. These specifications take the name of interfaces or contracts.  In this talk we will review the notion of a specification, and how it can be converted into a contract. We will analyze the role of the assumptions, and introduce the operators that are used to combine contracts through parallel composition and conjunction.  Next we will discuss relationships between contracts that define their refinement and compatibility, and between a contract and an implementation to check its compliance. We then give examples of practical interface and contract models.

Roberto Passerone is assistant professor of Electrical Engineering at the University of Trento, Italy. Before that, he was research scientist at Cadence Design Systems, Berkeley, California.  His research interests are in methodologies for system level design, integration of heterogeneous systems, and the design of wireless sensor networks. Roberto received his PhD from the University of California, Berkeley.