P. A. Abdulla, A. Annichini, and A. Bouajjani, Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol, TACAS, pp.208-222, 1999.
DOI : 10.1007/3-540-49059-0_15

P. A. Abdulla and B. Jonsson, Verifying Programs with Unreliable Channels, Information and Computation, vol.127, issue.2, pp.91-101, 1996.
DOI : 10.1006/inco.1996.0053
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.9558

R. Alur and P. Cern´ycern´y, Expressiveness of streaming string transducers, FSTTCS, pp.1-12, 2010.

R. Alur and P. Cern´ycern´y, Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs, POPL, pp.599-610, 2011.

R. Alur and J. V. Deshmukh, Nondeterministic Streaming String Transducers, ICALP, pp.1-20, 2011.
DOI : 10.1007/BF00264285
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.259.6918

F. Babich and L. Deotto, Formal methods for specification and analysis of communication protocols, IEEE Communications Surveys & Tutorials, vol.4, issue.1, pp.2-20, 2002.
DOI : 10.1109/COMST.2002.5341329

B. Badban, W. Fokkink, J. Groote, J. Pang, and J. Pol, Verification of a Sliding Window Protocol in µCRL and PVS. Formal Asp, Comput, vol.17, issue.3, pp.342-388, 2005.

J. Billington and G. E. Gallasch, How Stop and Wait Protocols Can Fail over the Internet, pp.209-223, 2003.
DOI : 10.1109/2.58215

A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili, Regular Model Checking, CAV, pp.403-418, 2000.
DOI : 10.1007/10722167_31
URL : https://hal.archives-ouvertes.fr/hal-00159512

D. Brand and P. Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM, vol.30, issue.2, pp.323-342, 1983.
DOI : 10.1145/322374.322380

Y. Cao, Reliability of Mobile Processes with Noisy Channels, IEEE Transactions on Computers, vol.61, issue.9, pp.611217-1230, 2012.
DOI : 10.1109/TC.2011.147

V. Cerf and R. Kahn, A Protocol for Packet Network Intercommunication, IEEE Transactions on Communications, vol.22, issue.5, pp.637-648, 1974.
DOI : 10.1109/TCOM.1974.1092259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.7384

D. Chkliaev, J. Hooman, and E. P. De-vink, Verification and Improvement of the Sliding Window Protocol, TACAS, pp.113-127, 2003.
DOI : 10.1007/3-540-36577-X_9

M. Chytil and V. Jákl, Serial composition of 2-way finite-state transducers and simple programs on strings, ICALP, pp.135-147, 1977.
DOI : 10.1007/3-540-08342-1_11

G. Delzanno, A. Sangnier, and G. Zavattaro, Verification of Ad Hoc Networks with Node and Communication Failures, FMOODS/FORTE, pp.235-250, 2012.
DOI : 10.1007/978-3-642-30793-5_15
URL : https://hal.archives-ouvertes.fr/hal-00909367

B. Forouzan, Data Communications and Networking, 2012.

J. Groote and J. Pol, A bounded retransmission protocol for large data packets, AMAST, pp.536-550, 1996.
DOI : 10.1007/BFb0014338

E. Gurari, The Equivalence Problem for Deterministic Two-Way Sequential Transducers is Decidable, SIAM Journal on Computing, vol.11, issue.3, pp.448-452, 1982.
DOI : 10.1137/0211035

K. Havelund and N. Shankar, Experiments in theorem proving and model checking for protocol verification, FME, pp.662-681, 1996.
DOI : 10.1007/3-540-60973-3_113
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.4275

L. Helmink, M. P. Sellink, and F. W. Vaandrager, Proof-checking a data link protocol, TYPES, pp.127-165, 1993.
DOI : 10.1007/3-540-58085-9_75
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.1021

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.
DOI : 10.1109/32.588521

. Iso, Data Communication -HDLC Procedures -Elements of Procedure, International Organization for Standardization, 1979.

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar, Symbolic model checking with rich assertional languages, CAV, pp.424-435, 1997.
DOI : 10.1016/S0304-3975(00)00103-1

E. Madelaine and D. Vergamini, Specification and Verification of a Sliding Window Protocol in LOTOS, pp.495-510, 1991.
DOI : 10.1016/B978-0-444-89402-1.50045-X

W. W. Peterson and D. T. Brown, Cyclic Codes for Error Detection, IRE, pp.228-235, 1961.
DOI : 10.1109/JRPROC.1961.287814

A. Podelski and A. Rybalchenko, ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement, PADL, pp.245-259, 2007.
DOI : 10.1007/978-3-540-69611-7_16

V. Rusu, Verifying a Sliding-Window Protocol Using PVS, FORTE, pp.251-268, 2001.
DOI : 10.1007/0-306-47003-9_16

A. P. Sistla and L. D. Zuck, Automatic temporal verification of buffer systems, CAV, pp.59-69, 1991.
DOI : 10.1007/3-540-55179-4_7

M. A. Smith and N. Klarlund, Verification of a Sliding Window Protocol Using IOA and MONA, pp.19-34, 2000.
DOI : 10.1007/978-0-387-35533-7_2
URL : https://hal.archives-ouvertes.fr/inria-00072689

V. Stenning, A data transfer protocol, Computer Networks (1976), vol.1, issue.2, pp.99-110, 1976.
DOI : 10.1016/0376-5075(76)90015-5

M. Veanes, P. Hooimeijer, B. Livshits, D. Molnar, and N. Bjørner, Symbolic Finite State Transducers: Algorithms and Applications, POPL, pp.137-150, 2012.
DOI : 10.1145/2103621.2103674

P. Wolper and B. Boigelot, Verifying systems with infinite but regular state spaces, CAV, pp.88-97, 1998.
DOI : 10.1007/BFb0028736
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.8097

M. Ying, ??-calculus with noisy channels, Acta Informatica, vol.266, issue.9, pp.525-593, 2005.
DOI : 10.1007/s00236-005-0168-0