On Limits and Possibilities of Automated Protocol Analysis
Gerard J. Holzmann · 1987
It is not likely that many traveling salesmen can be discouraged from their job by a lecture on its complexity [9]. Not surprisingly, writers of automated protocol analyzers are much the same. The problem of determining whether an arbitrary message passing system contains deadlocks is PSPACE-complete at best (for bounded queue lengths) [7-9]. Yet for any given formal analysis model it is easy to derive state space exploration routines that can find such errors with certainty – given a sufficient amount of time and space. In practice, therefore, one of the main problems is to optimize the speed and memory usage of an automated validator. To phrase it differently: it is not hard to validate protocols, it is hard to do it (sufficiently) fast. In reachability analyses, the limits of what can be analyzed in practice can be moved substantially if the traditional finite state machine model is abandoned. To illustrate this, we introduce a simple symbolic execution method based on vector addition. It is extended into a full protocol validator, carefully avoiding known performance bottlenecks. Compared with previous methods the performance of this validator is roughly two orders of magnitude in speed faster and allows validation of protocol systems up to 10 6 states in only minutes of CPU time on a medium size computer.