Integrative analysis of state-based requirements for completeness and consistency

Statically analyzing requirements specifications to assure that they possess desirable properties is an important activity in any rigorous software development project. All other stages of development depend upon the requirements specification. In addition, errors in the requirements that go undetected and propagate to later stages of development (the design and implementation stages) are the most costly to correct. Therefore, it is important to ensure that the requirements document satisfies certain desired properties before proceeding to later stages of the development process.;However, static analysis is performed on a formal model of the requirements that is an abstraction of the original requirements specification. Some degree of abstraction is necessary or the analysis becomes intractable. The output from the analysis is a report of the desirable properties that the requirements specification fails to satisfy. In many cases, abstractions in the analysis model lead to spurious errors in the analysis output. Spurious errors are conditions that are reported as errors, but information that was abstracted out of the analysis model precludes the reported conditions from being satisfied. A high ratio of spurious errors to true errors in the analysis output makes it difficult, error-prone, and time consuming to find and correct the true errors in the specification.;Two desirable properties that certain requirements documents should satisfy (for example, the requirements for critical systems) are completeness (a behavior is specified for every possible input) and consistency (no conflicting behaviors are specified). Analyzing for completeness and consistency in state-based requirements generalizes to analyzing complex logical expressions for satisfiability and mutual exclusion. Two methods for analyzing logical expressions for satisfiability and mutual exclusion are symbolic methods such as those that rely on Binary Decision Diagrams (BDDs), and reasoning methods such as theorem proving. Symbolic methods are fast and fully automated, but generate output that may contain many spurious errors since the analysis model contains many abstractions. Reasoning methods tend to be slower and require more manual intervention, but generate more accurate output since the analysis model contains fewer abstractions.;The objective of this research is to develop a technique for analyzing logical expressions for satisfiability and mutual exclusion that is fast enough to be used on a day-to-day basis, automated, and that generates analysis output with a small ratio of spurious errors to true errors. The results of the research are: (1) an iterative technique that integrates the strengths of a symbolic and a reasoning component to analyze logical expressions for satisfiability and mutual exclusion and circumvents the weaknesses of the components, and (2) a simple technique that uses a symbolic representation of logical expressions to help identify abstractions in a model that are causing spurious errors in the analysis output.