SoftContract: an assertion-based software development process that enables design-by-contract
J.-Y. Brunel, Marco Di Natale, A. Ferrari, Paolo Giusto, Luciano Lavagno · 2004
This paper discusses a model-based design flow for requirements in distributed embedded software development. Such requirements are specified using a language similar to Linear Temporal Logic which allows one to reason about time and sequencing. They consist of assertions which must hold for a design, given some assumptions on its environment. They can be checked both during simulation and, at least for a subset, even on the target. The key contribution of the paper is the extension to the embedded software domain of assertion-based verification, and the automated generation of property-checking code in multiple target languages, from simulation, to prototyping, to final production. 1.