Non-deterministic transducer models of retransmission protocols over noisy channels
We propose non-deterministic transducer models of retransmission protocols. We give the verification methodology for these protocol models. We establish decidability for two expressive cases of models. The verification is decidable even if the message lengths are unbounded. Our technique models key aspects of HDLC and TCP protocols over noisy channels.
protocols noisy channels formal methods string transducers