Record Details

Transducer-based Algorithmic Verification of Retransmission Protocols over Noisy Channels

Electronic Theses of Indian Institute of Science

View Archive Info
 
 
Field Value
 
Title Transducer-based Algorithmic Verification of Retransmission Protocols over Noisy Channels
 
Creator Thakkar, Jay
 
Subject Retransmission Protocols
Streaming String Transducers
Checksum
Noisy Channels
Protocol Verification
String Transducers
Sliding Window Protocols
Tranducer Models
Transducer-based Algorithmic Verification
Computer Science
 
Description Unreliable communication channels are a practical reality. They add to the complexity of protocol design and verification. In this work, we consider noisy channels which can corrupt messages. We present an approach to model and verify protocols which combine error detection and error control to provide reliable communication over noisy channels. We call these protocols retransmission protocols as they achieve reliable communication through repeated retransmissions of messages. These protocols typically use cyclic redundancy checks and sliding window protocols for error detection and control respectively. We propose models of these protocols as regular transducers operating on bit strings. Deterministic streaming string transducers provide a natural way of modeling these protocols and formalizing correctness requirements. The verification problem is posed as functional equivalence between the protocol transducer and the specification transducer. Functional equivalence checking is decidable for this class of transducers and this makes the transducer models amenable to algorithmic verification. In our transducer models, message lengths and retransmission rounds are unbounded. We present case studies based on TinyOS serial communication and the HDLC retransmission protocol.

We further extend our protocol models to capture the effects of a noisy channel with non-determinism. We present two non-deterministic yet decidable extensions of transducer models of retransmission protocols. For one of our models, we achieve decidable verification by bounding the retransmission rounds, whereas for the other, even retransmission rounds are unbounded.
 
Contributor Kanade, Aditya
 
Date 2018-04-05T03:24:39Z
2018-04-05T03:24:39Z
2018-04-05
2013
 
Type Thesis
 
Identifier http://etd.iisc.ernet.in/2005/3340
http://etd.iisc.ernet.in/abstracts/4205/G25734-Abs.pdf
 
Language en_US
 
Relation G25734