This paper outlines an approach to precise documentation and validation of system requirements. Precise documentation of requirements is important for developing and certifying mission critical software. Function tables have been used to document specifications of software components that are complete and disjoint. In this paper, function tables are embedded in an event based structure allowing requirements validation by proving invariants expressing safety properties. Function tables usually involve the use of total functions, or partial functions that are extended to be total. However, it is often convenient to use queries involving partial functions in specifications with preconditions defining the valid domain. Their use in tabular expressions raises the issue of whether the expressions in a table are well-defined. We organize queries involving partial functions in modules and specify them with contracts. We then propose a method for precise documentation, where requirements elicited from customers are expressed as atomic, natural language descriptions that are translated into tabular expressions referencing the specification modules, and into global properties expressed as invariants. We develop a calculus to prove that the tabular expressions are well-defined and that they entail the global properties. A biomedical device is used to illustrate our method for precise documentation and validation.

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.