Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels | Springer Nature Link

Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels | Springer Nature Link
Advertisement
Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels
Conference paper
pp 209–224
Cite this conference paper
Formal Techniques for Distributed Systems
(FMOODS 2013, FORTE 2013)
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Runtime verification of real-time event streams under non-synchronized arrival
Article
Open access
18 April 2020
Detecting Anomalies in Communication Packet Streams Based on Generative Adversarial Networks
Chapter
Recommender Systems Over Data Streams
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Communication and replication
Computability and Recursion Theory
Formal Languages and Automata Theory
Quantum Communications and Cryptography
Input/Output and Data Communications
Reverse transcription polymerase chain reaction
Formal Verification Techniques for Software Systems
References
Abdulla, P.A., Annichini, A., Bouajjani, A.: Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 208–222. Springer, Heidelberg (1999)
Chapter
Google Scholar
Abdulla, P.A., Jonsson, B.: Verifying Programs with Unreliable Channels. Inf. Comput. 127(2), 91–101 (1996)
Article
MathSciNet
MATH
Google Scholar
Alur, R., Cerný, P.: Expressiveness of streaming string transducers. In: FSTTCS, pp. 1–12 (2010)
Google Scholar
Alur, R., Cerný, P.: Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs. In: POPL, pp. 599–610 (2011)
Google Scholar
Alur, R., Deshmukh, J.V.: Nondeterministic Streaming String Transducers. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 1–20. Springer, Heidelberg (2011)
Chapter
Google Scholar
Babich, F., Deotto, L.: Formal Methods for Specification and Analysis of Communication Protocols. IEEE Comm. Surveys and Tutorials 4(1), 2–20 (2002)
Article
Google Scholar
Badban, B., Fokkink, W., Groote, J., Pang, J., Pol, J.: Verification of a Sliding Window Protocol in
CRL and PVS. Formal Asp. Comput. 17(3), 342–388 (2005)
Article
MATH
Google Scholar
Billington, J., Gallasch, G.E.: How Stop and Wait Protocols Can Fail over the Internet. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 209–223. Springer, Heidelberg (2003)
Chapter
Google Scholar
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)
Chapter
Google Scholar
Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. J. ACM 30(2), 323–342 (1983)
Article
MathSciNet
MATH
Google Scholar
Cao, Y.: Reliability of Mobile Processes with Noisy Channels. IEEE Trans. Computers 61(9), 1217–1230 (2012)
Article
Google Scholar
Cerf, V., Kahn, R.: A Protocol for Packet Network Intercommunication. IEEE Transactions on Communications 22(5), 637–648 (1974)
Article
Google Scholar
Chkliaev, D., Hooman, J., de Vink, E.P.: Verification and Improvement of the Sliding Window Protocol. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 113–127. Springer, Heidelberg (2003)
Chapter
Google Scholar
Chytil, M., Jákl, V.: Serial composition of 2-way finite-state transducers and simple programs on strings. In: Salomaa, A., Steinby, M. (eds.) ICALP 1977. LNCS, vol. 52, pp. 135–147. Springer, Heidelberg (1977)
Chapter
Google Scholar
D’Argenio, P.R., Katoen, J.P., Ruys, T.C., Tretmans, G.J.: The Bounded Retransmission Protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997)
Chapter
Google Scholar
Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of Ad Hoc Networks with Node and Communication Failures. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 235–250. Springer, Heidelberg (2012)
Chapter
Google Scholar
Finkel, A.: Decidability of the termination problem for completely specified protocols. Distrib. Comput. 7(3), 129–135 (1994)
Article
Google Scholar
Forouzan, B.: Data Communications and Networking. McGraw-Hill Companies (2012)
Google Scholar
Groote, J., Pol, J.: A Bounded Retransmission Protocol for Large Data Packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 536–550. Springer, Heidelberg (1996)
Chapter
Google Scholar
Gurari, E.: The equivalence problem for deterministic two-way sequential transducers is decidable. SIAM J. Comput. 11(3), 448–452 (1982)
Article
MathSciNet
MATH
Google Scholar
Havelund, K., Shankar, N.: Experiments in Theorem Proving and Model Checking for Protocol Verification. In: Gaudel, M.-C., Wing, J.M. (eds.) FME 1996. LNCS, vol. 1051, pp. 662–681. Springer, Heidelberg (1996)
Chapter
Google Scholar
Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-Checking a Data Link Protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127–165. Springer, Heidelberg (1994)
Chapter
Google Scholar
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
Article
MathSciNet
Google Scholar
ISO. Data Communication - HDLC Procedures - Elements of Procedure. Technical Report ISO 4335, International Organization for Standardization (1979)
Google Scholar
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 424–435. Springer, Heidelberg (1997)
Chapter
Google Scholar
Madelaine, E., Vergamini, D.: Specification and Verification of a Sliding Window Protocol in LOTOS. In: FORTE, pp. 495–510 (1991)
Google Scholar
Peterson, W.W., Brown, D.T.: Cyclic Codes for Error Detection. In: IRE, pp. 228–235 (1961)
Google Scholar
Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)
Chapter
Google Scholar
Rusu, V.: Verifying a Sliding Window Protocol using PVS. In: FORTE, pp. 251–268 (2001)
Google Scholar
Sistla, A.P., Zuck, L.D.: Automatic Temporal Verification of Buffer Systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 59–69. Springer, Heidelberg (1992)
Chapter
Google Scholar
Smith, M.A., Klarlund, N.: Verification of a Sliding Window Protocol Using IOA and MONA. In: FORTE, pp. 19–34 (2000)
Google Scholar
Stenning, V.: A Data Transfer Protocol. Computer Networks 1, 99–110 (1976)
Google Scholar
Tanenbaum, A.S., Wetherall, D.: Computer Networks. Pearson (2010)
Google Scholar
Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjørner, N.: Symbolic Finite State Transducers: Algorithms and Applications. In: POPL, pp. 137–150 (2012)
Google Scholar
Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 88–97. Springer, Heidelberg (1998)
Chapter
Google Scholar
Ying, M.:
-calculus with noisy channels. Acta Inf 41(9), 525–593 (2005)
Article
MATH
Google Scholar
Download references
Author information
Authors and Affiliations
Indian Institute of Science, India
Jay Thakkar & Aditya Kanade
University of Pennsylvania, USA
Rajeev Alur
Authors
Jay Thakkar
View author publications
Search author on:
PubMed
Google Scholar
Aditya Kanade
View author publications
Search author on:
PubMed
Google Scholar
Rajeev Alur
View author publications
Search author on:
PubMed
Google Scholar
Editor information
Editors and Affiliations
Department of Computer Science and Mathematics, University of Passau, Innstraße 31, 94034, Passau, Germany
Dirk Beyer
Dipartimento di Sistemi e Informatica, Università di Firenze, Viale Morgagni, 65, 50134, Florence, Italy
Michele Boreale
Rights and permissions
Reprints and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Thakkar, J., Kanade, A., Alur, R. (2013). Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels.

In: Beyer, D., Boreale, M. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2013 2013. Lecture Notes in Computer Science, vol 7892. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38592-6_15
Download citation
.RIS
.ENW
.BIB
DOI
Publisher Name
Springer, Berlin, Heidelberg
Print ISBN
978-3-642-38591-9
Online ISBN
978-3-642-38592-6
eBook Packages
Computer Science
Computer Science (R0)
Springer Nature Proceedings Computer Science
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Equivalence Check
Input String
Noisy Channel
Cyclic Redundancy Check
String Variable
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Publish with us
Policies and ethics