A Generic Model of Contracts for Embedded Systems

TL;DR

This paper introduces a mathematical framework for contract-based modeling in embedded systems, enabling concurrent and controlled system design through rich component behaviors and formalized composition.

Contribution

It presents a novel generic mathematical model supporting speculative design with rich components and formalized composition methods.

Findings

Supports concurrent system development

Formalizes component behaviors and composition

Enables integration of diverse system aspects

Abstract

We present the mathematical foundations of the contract-based model developed in the framework of the SPEEDS project. SPEEDS aims at developing methods and tools to support "speculative design", a design methodology in which distributed designers develop different aspects of the overall system, in a concurrent but controlled way. Our generic mathematical model of contract supports this style of development. This is achieved by focusing on behaviors, by supporting the notion of "rich component" where diverse (functional and non-functional) aspects of the system can be considered and combined, by representing rich components via their set of associated contracts, and by formalizing the whole process of component composition.