Аннотация: Настоящая работа посвящена исследованию проблемы автоматического построения сетевых моделей Estelle-спецификаций распределенных систем и развития средств верификации этих моделей. Язык выполнимых спецификаций Estelle принят в качестве международного стандарта. Рассматриваются Estelle-спецификации с задержками и приоритетами, но без динамических конструкций, позволяющие адекватно представлять значительный класс коммуникационных протоколов. В качестве моделей выбраны раскрашенные сети Петри, предложенные Йенсеном, которые расширяются посредством семантик времени в смысле Мерлина и приоритетов. В работе представлен метод трансляции Estelle-спецификаций в данной сетевой модели, описана его реализация, а также система NetCalc, предназначенная для редактирования и симуляции такх моделей. Кроме того, представлены результаты экспериментов по сетевому моделированию и поиску семантических ошибок для версий четырех известных протоколов: со скользящим окном, кольцевого, соединений, InRes.
Держатели документа:
ИВМ СО РАН : 660036, Красноярск, Академгородок, 50, стр.44
Доп.точки доступа:
Алексеев, Г.И.; Быстров, А.В; Куртов, С.А.; Мыльников, С.П.; Окунишникова, Е.В.
Экземпляры всего: 1
ИВМ-Фонд (1)
Свободны: ИВМ-Фонд (1)