Logical-time contracts for reactive embedded components

Abstract

The “Design by contract ” principle has been applied successfully in the context of object-oriented designs, since it was first proposed by B. Meyer for Eiffel. We claim that a simple pre-post specification is not sufficient for reactive software. We introduce a model of reactive components suitable for reactive embedded software, and a notion of logical-time contract for the specification and use of these components in synchronous compositions. 1.