Geodesic
Deductive Verification of the Sliding Window Protocol
Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 6, pp. 57-68.

Voir la notice de l'article provenant de la source Math-Net.Ru

We consider the well-known Sliding Window Protocol which provides reliable and efficient transmission of data over unreliable channels. A formal proof of correctness for this protocol faces substantial difficulties caused by a high degree of parallelism which creates a significant potential for errors. Here we consider a version of the protocol that is based on selective repeat of frames. The specification of the protocol by a state machine and its safety property are represented in the language of the verification system PVS. Using the PVS system, we give an interactive proof of this property of the Sliding Window Protocol.
Mots-clés : communication protocols
Keywords: Sliding Window Protocol, fault tolerance, formal specification, automated verification, interactive theorem proving, PVS. 
@article{MAIS_2012_19_6_a4,
     author = {D. A. Chkliaev and V. A. Nepomniaschy},
     title = {Deductive {Verification} of the {Sliding} {Window} {Protocol}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {57--68},
     publisher = {mathdoc},
     volume = {19},
     number = {6},
     year = {2012},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a4/}
}
TY  - JOUR
AU  - D. A. Chkliaev
AU  - V. A. Nepomniaschy
TI  - Deductive Verification of the Sliding Window Protocol
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2012
SP  - 57
EP  - 68
VL  - 19
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a4/
LA  - ru
ID  - MAIS_2012_19_6_a4
ER  - 
%0 Journal Article
%A D. A. Chkliaev
%A V. A. Nepomniaschy
%T Deductive Verification of the Sliding Window Protocol
%J Modelirovanie i analiz informacionnyh sistem
%D 2012
%P 57-68
%V 19
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a4/
%G ru
%F MAIS_2012_19_6_a4
D. A. Chkliaev; V. A. Nepomniaschy. Deductive Verification of the Sliding Window Protocol. Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 6, pp. 57-68. http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a4/

[1] I. V. Alekseev, V. A. Sokolov, D. Yu. Chalyi, Modelirovanie i analiz transportnykh protokolov v informatsionnykh setyakh, Yaroslavskii gosudarstvennyi universitet, Yaroslavl, 2004, 262 pp.

[2] E. Tanenbaum, Kompyuternye seti, Piter, SPb., 2002, 848 pp.

[3] B. Badban, W. Fokkink, J. F. Groote, J. Pang, J. van de Pol, “Verification of a Sliding Window Protocol in $\mu$CRL and PVS”, Formal Aspects of Computing, 17:3 (2005), 342–388 | Zbl

[4] D. A. Chkliaev, Mechanical verification of concurrency control and recovery protocols, PhD thesis, Eindhoven University of Technology, Eindhoven, 2001, 154 pp. http://alexandria.tue.nl/extra2/200112908.pdf | Zbl

[5] D. Chkliaev, J. Hooman, E. P. de Vink, “Verification and Improvement of the Sliding Window Protocol”, Lecture Notes in Computer Science, 2619, 2003, 113–127 | Zbl

[6] D. A. Chkliaev, V. A. Nepomniaschy, “Specification and verification of the classical sliding window protocol”, Bulletin of the Novosibirsk Computing Center. Ser.: Computer Science, 32, IIS Special Issue (2011), 37–56

[7] S. Owre, J. M. Rushby, N. Shankar, “PVS: a Prototype Verification System”, Lecture Notes in Computer Science, 607, 1992, 748–752

[8] V. Rusu, “Verifying a Sliding-Window Protocol using PVS”, Formal Description Techniques, FORTE'01, 2001, 251–266

[9] N. V. Stenning, “A data transfer protocol”, Computer Networks, 1 (1976), 99–110