Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels

Abstract : Unreliable communication channels are a practical reality. They add to the complexity of protocol design and verification. In this paper, 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. 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. We present case studies based on TinyOS serial communication and the HDLC retransmission protocol.
Type de document :
Communication dans un congrès
Dirk Beyer; Michele Boreale. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.209-224, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_15〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01515246
Contributeur : Hal Ifip <>
Soumis le : jeudi 27 avril 2017 - 10:46:50
Dernière modification le : jeudi 27 avril 2017 - 14:43:59
Document(s) archivé(s) le : vendredi 28 juillet 2017 - 12:44:19

Fichier

978-3-642-38592-6_15_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Rajeev Alur, Jay Thakkar, Aditya Kanade. Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels. Dirk Beyer; Michele Boreale. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.209-224, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_15〉. 〈hal-01515246〉

Partager

Métriques

Consultations de la notice

31

Téléchargements de fichiers

12