В.А. Непомнящий, А.Г. Алексеев, А.В. Быстров, С.А. Куртов, С.П. Мыльников, Е.В. Окунишникова, П.А. Чубарев, Т.Г. Чурина
Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри

Монография, 1998

Настоящая работа посвящена исследованию проблемы автоматического построения сетевых моделей Estelle-спецификаций распределенных систем и развития средств верификации этих моделей. Язык выполнимых спецификаций Estelle принят в качестве международного стандарта. Рассматриваются Estelle-спецификации с задержками и приоритетами, но без динамических конструкций, позволяющие адекватно представлять значительный класс коммуникационных протоколов. В качестве моделей выбраны раскрашенные сети Петри, предложенные Йенсеном, которые расширяются посредством семантик времени в смысле Мерлина и приоритетов. В работе представлен метод трансляции Estelle-спецификаций в данной сетевой модели, описана его реализация, а также система NetCalc, предназначенная для редактирования и симуляции таких моделей. Кроме того, представлены результаты экспериментов по сетевому моделированию и поиску семантических ошибок для версий четырех известных протоколов: со скользящим окном, кольцевого, соединений, InRes.




Вы обнаружили ошибку в следующем тексте:
Просто нажмите кнопку "Отправить сообщение об ошибке" для завершения. Вы можете также ввести комментарий (желательно).