The authors have revised and extended their excellent paper from the 1995 International Conference on Software Engineering. It describes the automatic validation and verification of a software requirements specification (SRS) of a nontrivial real system, TCAS III. The SRS was prepared using requirements state machine language, which combines statecharts with AND/OR tables. These tables are simplified limited-entry decision tables that specify conditions for state transitions.

The SRS was selected by the clients in preference to their informal SRS and so underwent expensive independent validation and verification for incompleteness. Meanwhile, tools were used to verify both completeness and consistency. All examples of incompleteness found by independent validation and verification were found by the tools. The tools also found potentially hazardous “inconsistencies” where the SRS permitted multiple responses to an event under some conditions. The tools used binary decision diagrams and showed excellent performance on this nontrivial SRS.

The beginning and end of the paper could be read by anyone developing complex software. Sections 3.1, 3.2, and 4, as well as the appendix, are only for those who enjoy symbolic logic and set theory. They present a compositional semantics that makes automatic validation and verification feasible. The end of the paper describes the tools, gives examples of output, and draws conclusions. There are two interesting conclusions. First, tables with only Boolean values tend to include spurious possibilities. Second, clients and domain experts must be consulted to fix SRS defects.