Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри

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