Дедуктивная верификация протокола скользящего окна
https://doi.org/10.18255/1818-1015-2012-6-57-68
Аннотация
Рассматривается известный протокол скользящего окна, который обеспечивает надёжную и эффективную передачу данных по ненадёжным каналам. Формальное доказательство корректности этого протокола требует преодоления существенных трудностей, связанных с высокой степенью параллелизма, которая создаёт значительные возможности для ошибок. Здесь рассматривается версия данного протокола, основанная на выборочном повторе кадров. На языке системы верификации PVS описаны спецификация этого протокола с помощью машины состояний и его свойство безопасности. С помощью системы PVS проведено в интерактивном режиме доказательство этого свойства протокола скользящего окна.
Об авторах
Дмитрий Александрович Шкляев
Институт систем информатики имени А.П. Ершова СО РАН
Россия
магистр математики, ведущий программист
Россия
магистр математики, ведущий программист
Валерий Александрович Непомнящий
Институт систем информатики имени А.П. Ершова СО РАН
Россия
кандидат физ.-мат. наук, зав. лабораторией
Россия
кандидат физ.-мат. наук, зав. лабораторией
Список литературы
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.
Рецензия
Для цитирования:
Шкляев Д.А., Непомнящий В.А. Дедуктивная верификация протокола скользящего окна. Моделирование и анализ информационных систем. 2012;19(6):57-68. https://doi.org/10.18255/1818-1015-2012-6-57-68
For citation:
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
Просмотров:
956
Послать статью по эл. почте 