A specification and analysis of the high-speed transport protocol SNR (named after its inventors, K. Sabnani, A. Netravali, and W. Roome) is presented. The analysis leads to some improvement proposals for SNR. The formal model used is systems of communicating machines (SCM).

The paper is a good blend of theory and practice. The SCM model is a natural modification of the customary automata-based modeling approach. It leads to a compact and readable specification even for a large protocol like SNR. The SCM model has some drawbacks in the analysis phase. The difficulties are properly explained in the paper. On the other hand, there is currently no alternative method that would allow a complete verification of a protocol of this size. All methods must finally resort to simulations, resembling normal debugging with good coverage, instead of a complete verification. This is due to the huge size of the global state space of any real-life protocol.

I can recommend this paper to anyone who is interested in the practical verification and debugging of computer communication protocols.