RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2012, том 19, номер 6, страницы 57–68 (Mi mais270)  

Дедуктивная верификация протокола скользящего окна

Д. А. Шкляев, В. А. Непомнящий

Институт систем информатики им. А. П. Ершова СО РАН

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

Ключевые слова: коммуникационные протоколы, протокол скользящего окна, отказоустойчивость, формальная спецификация, автоматизированная верификация, интерактивное доказательство теорем, PVS.

Полный текст: PDF файл (279 kB)
Список литературы: PDF файл   HTML файл
Тип публикации: Статья
УДК: 519.7+004.75
Поступила в редакцию: 22.07.2012

Образец цитирования: Д. А. Шкляев, В. А. Непомнящий, “Дедуктивная верификация протокола скользящего окна”, Модел. и анализ информ. систем, 19:6 (2012), 57–68

Цитирование в формате AMSBIB
\RBibitem{ShkNep12}
\by Д.~А.~Шкляев, В.~А.~Непомнящий
\paper Дедуктивная верификация протокола скользящего окна
\jour Модел. и анализ информ. систем
\yr 2012
\vol 19
\issue 6
\pages 57--68
\mathnet{http://mi.mathnet.ru/mais270}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais270
  • http://mi.mathnet.ru/rus/mais/v19/i6/p57

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:205
    Полный текст:86
    Литература:25
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020