We propose a format for precise documentation of requirements to drive the development of dependable software products and to provide evidence for their certification. Requirements are elicited from customers and expressed informally as atomic English descriptions. To analyze the consistency of the requirements, we translate them into a software specification consisting of model contracts and tabular expressions. Model contracts describe queries as pre/post-conditions using mathematical constructs (e.g. quantifiers, sets, relations, sequences) which make them more expressive than classical implementation contracts. Tabular expressions use these queries to provide complete black-box descriptions of the system input-output relation. We validate the requirements via proofs of (a) the completeness, disjointness, and well-definedness of the specification and (b) the consistency between the specification and the atomic requirements. The model contracts are translated into an executable specification using MSL (model specification language). The executable specification plays a dual role. Even before code production, the specification is used to validate the requirements. Once the code is produced, we verify that the code satisfies the specification via runtime assertion checking.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.