Formalization and completeness of evolving requirements using Contracts

The contract-based paradigm, founded on the use of contracts as formal requirements, allows distributed designers to develop different aspects and components of the overall system in a concurrent but controlled way. In this paper we describe an extension of contract-based design that aims at bridging the gap between requirements, as they are identified in current industrial practice, and contracts. Our contributions can be summarized as follows: (1) the contract formalization is enriched with the concept of precondition for the unification of the two traditional contract operators, namely parallel composition and conjunction; (2) the definition of contract completeness has been formalized based on the concept of precondition in order to avoid vacuous contract implementations; (3) two new operators, extension and override, are introduced to support the formalization of evolving requirements; (4) a methodology has been defined for the formalization of contracts starting from requirements using the precondition, extension, override and completeness concepts and (5) a simulation-based support for the methodology using executable monitors has been described.