On the analysis needs when verifying state-based software requirements: An experience report

In a previous investigation we formally defined procedures for analyzing hierarchical state-based requirements specifications for two properties: (1) completeness with respect to a set of criteria related to robustness (a response is specified for every possible input and input sequence) and (2) consistency (the specification is free from conflicting requirements and undesired non-determinism). Informally, the analysis involves determining if large Boolean expressions are tautologies. We implemented the analysis procedures in a prototype tool and evaluated their effectiveness and efficiency on a large real world requirements specification expressed in an hierarchical state-based language called Requirements State Machine Language. Although our initial approach was largely successful, there were some drawbacks with the original tools. In our initial implementation we abstracted all formulas to propositional logic. Unfortunately, since we are manipulating the formulas without interpreting any of the functions in the individual predicates, the abstraction can lead to large numbers of spurious (or false) error reports. To increase the accuracy of our analysis we have continually refined our tool with decision procedures and, finally, come to the conclusion that theorem proving is often needed to avoid large numbers of spurious error reports. This paper discusses the problems with spurious error reports and describes our experiences analyzing a large commercial avionics system for completeness and consistency.