Algorithms for Automated Protocol Validation

This paper studies the four basic types of algorithm that, over the last ten years, have been developed for the automated validation of the logical consistency of data communication protocols. The algorithms are compared on memory usage, CPU time requirements, and the quality, or coverage, of the search for errors. It is shown that the best algorithm, according to above criteria, can be improved further in a significant way, by avoiding a known performance bottleneck. 

The algorithm derived in this manner works in a fixed size memory arena (it will never run out of memory), it is up to two orders of magnitude faster than the previous methods, and it has superior coverage of the state space when analyzing large protocol systems. 

The algorithm is the first for which the search efficiency (the number of states analyzed per second) does not depend on the size of the state space: there is no time penalty for analyzing very large state spaces. The practicality of the new algorithm has been tested in the validation of portions of AT&T's 5ESS(TM) switch. The models analyzed in these tests generated up to 1 billion composite system states, that could be analyzed effectively in an hour's worth of CPU time on a large mainframe computer.