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

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

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



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






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


Информ. и её примен., 2014, том 8, выпуск 2, страницы 55–69 (Mi ia311)  

Метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений

А. М. Миронов

Институт проблем информатики Российской академии наук

Аннотация: Рассматривается проблема доказательства наблюдаемой эквивалентности для класса вычислительных процессов, называемых процессами с передачей сообщений. Действия, выполняемые такими процессами, заключаются в посылке или приеме сообщений, проверке логических условий и обновлении значений внутренних переменных процессов. Основным результатом статьи является теорема, сводящая задачу доказательства наблюдаемой эквивалентности пары процессов с передачей сообщений к задаче нахождения формул, ассоциированных с парами состояний этих процессов, удовлетворяющих некоторым условиям, которые связаны с переходами этих процессов. Данное сведение является обобщением известного метода Флойда верификации блок-схем, в котором задача верификации блок-схемы сводится к задаче нахождения формул (называемых промежуточными утверждениями), связанных с некоторыми точками в блок-схемах и удовлетворяющих некоторым условиям, соответствующим переходам в блок-схемах. Изложенный метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений иллюстрируется примером верификации протокола скользящего окна.

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

DOI: https://doi.org/10.14375/19922264140206

Полный текст: PDF файл (333 kB)
Список литературы: PDF файл   HTML файл

Реферативные базы данных:

Тип публикации: Статья
Поступила в редакцию: 04.02.2014

Образец цитирования: А. М. Миронов, “Метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений”, Информ. и еë примен., 8:2 (2014), 55–69

Цитирование в формате AMSBIB
\RBibitem{Mir14}
\by А.~М.~Миронов
\paper Метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений
\jour Информ. и е\"e примен.
\yr 2014
\vol 8
\issue 2
\pages 55--69
\mathnet{http://mi.mathnet.ru/ia311}
\crossref{https://doi.org/10.14375/19922264140206}
\elib{http://elibrary.ru/item.asp?id=21646363}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/ia311
  • http://mi.mathnet.ru/rus/ia/v8/i2/p55

    ОТПРАВИТЬ: 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
  • Информатика и её применения
    Просмотров:
    Эта страница:99
    Полный текст:42
    Литература:13
    Первая стр.:1

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2017