The authors discuss a set of criteria useful for the detection of errors in the requirements specification of real-time process-control systems. The criteria are based on an abstract state-machine model and defined formally using first-order predicate calculus. They cover such areas as system states, transitions, input/output variables and conditions, and relationships among them.
Some of the criteria are general and merely serve to illustrate how formalisms can be used. For example, the authors recommend that all input must be used somewhere, every state must be reachable, and input conditions must be exhaustive and mutually exclusive.
The authors rightly point out that the mere existence or nonexistence of an event carries no meaning without timing considerations. The most useful and interesting discussions in the paper are mostly related to timing, such as input and output capacities, timing between successive events, latency, data age, interrupt-signaled events, performance degradation, and anomalies such as being too late or too early. The coverage of the reachability considerations of safe states through robust paths is also interesting.
Although the title of the paper suggests that the universe of discourse is real-time process-control systems, most of the analyses suggested are applicable in general and would be just as useful in any safety-critical system. The criteria proposed are far from complete, and more study is required before the specified systems can be guaranteed to be robust and free from ambiguity. Furthermore, the authors do not indicate how the formally expressed criteria can be linked with specification languages or formal verification techniques.