P. A. Abdulla, A. Aniinichini, S. Bensalem, A. Bouajjani, P. Habermehl et al., Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis, Computer Aided Verification. 11th International Conference, CAV '99, 1999.
DOI : 10.1007/3-540-48683-6_15

K. A. Barlett, R. A. Scantlebury, and P. C. Wilkinson, A note on reliable transmission over half duplex links, Communications of the ACM, vol.12, 1969.

D. Brand, J. William, and H. Joyner, Verification of HDLC, IEEE Transactions on Communications, vol.30, issue.5, pp.301136-1142, 1982.
DOI : 10.1109/TCOM.1982.1095558

R. E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys, vol.24, issue.3, pp.293-318, 1992.
DOI : 10.1145/136035.136043

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Workshop on Logics of Programs, 1981.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

S. J. Garland and J. V. Guttag, A guide to the larch prover Updated version available as http, 1991.

J. Stephen, N. A. Garland, and . Lynch, The IOA language and toolset: Support for designing , analyzing, and builiding distributed systems, 1998.

P. Godefroid and D. E. Long, Symbolic protocol verification with Queue BDDs. Formal Methods in System Design, pp.257-271, 1999.

M. J. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993.

K. Havelund and N. Shankar, Experiments in theorem proving and model checking for protocol verification, Formal Methods Europe (FME), volume 1051 of Lecture Notes in Computer Science, 1996.
DOI : 10.1007/3-540-60973-3_113

J. G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, R. Paige et al., Mona: Monadic second-order login in practice, Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS '95 LCNS 1019, 1995.

T. Higashino, M. Mori, Y. Sugiyama, K. Taniguchi, and T. Kasami, An Algebraic Specification of HDLC Procedures and Its Verification, IEEE Transactions on Software Engineering, vol.10, issue.6, pp.10825-836, 1984.
DOI : 10.1109/TSE.1984.5010311

R. Kaivola, Using compositional preorders in the verification of sliding window protocol, Computer Aided Verification. 9th International Conference, CAV'97, pp.48-59, 1997.
DOI : 10.1007/3-540-63166-6_8

N. Klarlund, &. Mona, and . Fido, The logic-automaton connection in practice, CSL '97 Proceedings, 1998.

N. Lynch and M. Tuttle, An introduction to input/output automata, CWI Quarterly, vol.3, issue.2, 1989.

P. Manolios, K. Namjoshi, and R. Sumners, Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation, Computer Aided Verification. 11th International Conference, CAV '99, 1999.
DOI : 10.1007/3-540-48683-6_32

R. Milner, Communication and Concurrency, 1990.

S. Owre, J. Rushby, N. Shankar, and F. Von-henke, Formal verification for fault-tolerant architectures: prolegomena to the design of PVS, IEEE Transactions on Software Engineering, vol.21, issue.2, pp.107-125, 1995.
DOI : 10.1109/32.345827

J. Postel, Transmission Control Protocol -DARPA Internet Program Specification (Internet Standard STC-007), 1981.

J. L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron, Verification in Xesar of the sliding window protocol, Protocol Specification, Testing and Verification VII, pp.235-248, 1987.

K. Sabnani, An algorithmic technique for protocol verification, IEEE Transactions on Communications, vol.36, issue.8, 1988.
DOI : 10.1109/26.3772

A. , U. Shankar, and S. S. Lam, An HDLC protocol specification and verification using image protocols, ACM Transactions on Computer Systems, vol.1, issue.4, pp.331-368, 1983.

P. Wolper, Synthesis of communication processes from temporal logic specifications, Proceedings 13th ACM Symposium on POPL, pp.184-193, 1986.

R. , U. De-recherche, I. Lorraine, V. Technopôle-de-nancy-brabois, I. Lès-nancy-unité-de-recherche et al., Campus scientifique, 615 rue du Jardin Botanique Irisa, Campus universitaire de Beaulieu, 35042 RENNES Cedex Unité de recherche INRIA Rhône-Alpes, p.78153, 2004.