Degree Type


Date of Award


Degree Name

Master of Science


Computer Science


Computer Science


Inadequate communication of domain knowledge in natural language (such as English) has been implicated as a major source of requirements defects in high-confidence software. Such defects can lead to loss of lives and property. This thesis develops two techniques that offer partial solutions to the requirements defects problem. First, the thesis describes a technique for resolving requirements confusion, a problem that has been observed repeatedly during testing and operations of complex, high-confidence software, and a source of requirements defects. The technique defines requirements patterns for recurring sets of requirements confusion, and then uses these patterns to create formal specifications of the correct behavior. This approach allows the user to identify and explore any gaps between the expected and the correct behavior using the specification tool's simulation capabilities. The thesis illustrates and evaluates the technique on real-world sets of requirements confusion involving watermarks. The second major contribution of this thesis is to describe a technique for preventing some timing requirements defects caused by communication gaps during domain knowledge transfer between system experts and software engineers. The technique applies timing constraints on software inputs and relies on data-age, a variable that must be defined for each input to the software. The thesis defines the guidelines for specifying the behavior of data-age variables, as well as how to use them in setting the timing constraints of the corresponding inputs. The technique is applied to a Mars Polar Lander (MPL) software module through formal specification of the module. Analysis shows how this technique could have been used to prevent a requirement defect due to the gaps in domain knowledge communication, perhaps preventing the MPL accident.


Copyright Owner

Oko Robert Swai



OCLC Number


File Format


File Size

123 pages