General

Contract-based design, first conceived for software specifica-tion [7] and now also applied to embedded systems (cfr. e.g., [2, 1]), structures the component properties into contracts. A contract specifies the properties assumed to be satisfied by the component environment (assumptions), and the properties guaranteed by the component in response (guarantees). There are several points sup-porting the idea of contract-based reasoning. The first one is that it provides a clean framework for compositional verification of global properties of a system: the contracts are used as landmarks for the proof, so that in the end it is possible to obtain the guarantee for the global property out of the proof that each of the components satisfies its contracts, and that the individual contracts entail the global property. The second is that it supports stepwise refinement, so that when a component is decomposed, the corresponding speci-fication is decomposed at the same time, i.e. way before the behav