Deductive Verification of the Sliding Window Protocol
https://doi.org/10.18255/1818-1015-2012-6-57-68
Abstract
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.
About the Authors
D. A. Chkliaev
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
магистр математики, ведущий программист
Russian Federation
магистр математики, ведущий программист
V. A. Nepomniaschy
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
кандидат физ.-мат. наук, зав. лабораторией
Russian Federation
кандидат физ.-мат. наук, зав. лабораторией
References
1. Алексеев И.В., Соколов В.А., Чалый Д.Ю. Моделирование и анализ транспортных протоколов в информационных сетях. Ярославль: Ярославский государственный университет, 2004. 262 с.
2. Таненбаум Э. Компьютерные сети. СПб.: Питер, 2002. 848 с.
3. Badban B., Fokkink W., Groote J.F., Pang J., van de Pol J. Verification of a Sliding Window Protocol in µCRL and PVS // Formal Aspects of Computing. 2005. V. 17(3). P. 342–388.
4. Chkliaev D.A. Mechanical verification of concurrency control and recovery protocols (PhD thesis) // Eindhoven: Eindhoven University of Technology, 2001. 154 p. Available at http://alexandria.tue.nl/extra2/200112908.pdf.
5. Chkliaev D., Hooman J., de Vink E.P. Verification and Improvement of the Sliding Window Protocol // Lecture Notes in Computer Science. 2003. V. 2619. P. 113–127.
6. Chkliaev D.A., Nepomniaschy V.A. Specification and verification of the classical sliding window protocol // Bulletin of the Novosibirsk Computing Center, Series: Computer Science, IIS Special Issue. 2011. V. 32. P. 37–56.
7. Owre S., Rushby J.M., Shankar N. PVS: a Prototype Verification System // Lecture Notes in Computer Science. 1992. V. 607. P. 748–752.
8. Rusu V. Verifying a Sliding-Window Protocol using PVS. // Formal Description Techniques (FORTE’01). 2001. P. 251–266.
9. Stenning N.V. A data transfer protocol // Computer Networks. 1976. V. 1. P. 99–110.
Review
For citations:
Chkliaev D.A., Nepomniaschy V.A. Deductive Verification of the Sliding Window Protocol. Modeling and Analysis of Information Systems. 2012;19(6):57-68. (In Russ.) https://doi.org/10.18255/1818-1015-2012-6-57-68
Views:
965
Email this article 