maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-6-57-68mais-139Research ArticleОригинальные статьиArticlesДедуктивная верификация протокола скользящего окнаDeductive Verification of the Sliding Window ProtocolШкляевДмитрий АлександровичChkliaevD. A.

магистр математики, ведущий программист

магистр математики, ведущий программист

dmitrichkl@yahoo.comНепомнящийВалерий АлександровичNepomniaschyV. A.

кандидат физ.-мат. наук, зав. лабораторией

кандидат физ.-мат. наук, зав. лабораторией

vnep@iis.nsk.suИнститут систем информатики имени А.П. Ершова СО РАНРоссияИнститут систем информатики имени А.П. Ершова СО РАНRussian Federation2012120320151965768Copyright © Шкляев Д.А., Непомнящий В.А., 20152015Шкляев Д.А., Непомнящий В.А.Chkliaev D.A., Nepomniaschy V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/139

Рассматривается известный протокол скользящего окна, который обеспечивает надёжную и эффективную передачу данных по ненадёжным каналам. Формальное доказательство корректности этого протокола требует преодоления существенных трудностей, связанных с высокой степенью параллелизма, которая создаёт значительные возможности для ошибок. Здесь рассматривается версия данного протокола, основанная на выборочном повторе кадров. На языке системы верификации PVS описаны спецификация этого протокола с помощью машины состояний и его свойство безопасности. С помощью системы PVS проведено в интерактивном режиме доказательство этого свойства протокола скользящего окна.

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.

коммуникационные протоколыпротокол скользящего окнаотказоустойчивостьформальная спецификацияавтоматизированная верификацияинтерактивное доказательство теоремPVScommunication protocolsSliding Window Protocolfault toleranceformal specificationautomated verificationinteractive theorem provingPVSReferencesАлексеев И.В., Соколов В.А., Чалый Д.Ю. Моделирование и анализ транспортных протоколов в информационных сетях. Ярославль: Ярославский государственный университет, 2004. 262 с.Алексеев И.В., Соколов В.А., Чалый Д.Ю. Моделирование и анализ транспортных протоколов в информационных сетях. Ярославль: Ярославский государственный университет, 2004. 262 с.Таненбаум Э. Компьютерные сети. СПб.: Питер, 2002. 848 с.Таненбаум Э. Компьютерные сети. СПб.: Питер, 2002. 848 с.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.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.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.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.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.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.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.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.Owre S., Rushby J.M., Shankar N. PVS: a Prototype Verification System // Lecture Notes in Computer Science. 1992. V. 607. P. 748–752.Owre S., Rushby J.M., Shankar N. PVS: a Prototype Verification System // Lecture Notes in Computer Science. 1992. V. 607. P. 748–752.Rusu V. Verifying a Sliding-Window Protocol using PVS. // Formal Description Techniques (FORTE’01). 2001. P. 251–266.Rusu V. Verifying a Sliding-Window Protocol using PVS. // Formal Description Techniques (FORTE’01). 2001. P. 251–266.Stenning N.V. A data transfer protocol // Computer Networks. 1976. V. 1. P. 99–110.Stenning N.V. A data transfer protocol // Computer Networks. 1976. V. 1. P. 99–110.

The authors declare that there are no conflicts of interest present.