Инструмент для распределенного анализа поведенческих свойств вполне структурированных систем помеченных переходов

Модель вполне структурированных систем переходов все более широко используется в качестве инструмента исследования параллельных и распределенных систем. С помощью данного класса систем следующие проблемы могут быть решены: покрытия, неизбежности, поддержки управляющего состояния, останова и другие семантические свойства. Несмотря на то, что модель вполне структурированных систем переходов известна и изучается уже несколько десятков лет, был замечен недостаток в практической реализации алгоритмов их анализа и исследовании их применения. Так как на практике моделируемые системы могут иметь довольно большое количество состояний, подходы, применяемые, к их анализу должны эффективно использовать имеющиеся ресурсы, чтобы, как минимум, сэкономить время исследователя. Целью данной работы – является разработка инструмента распределенного анализа поведенческих свойств вполне структурированных систем переходов. В работе рассматриваются два основных алгоритма, используемых для изучения поведенческих свойств вполне структурированных систем переходов: Метод насыщения и Покрывающее дерево системы переходов, для которых представлены возможные параллельные версии реализации. На основе исследования спроектирован и реализован инструмент для анализа вполне структурированных систем переходов в распределенном окружении. Применимость подхода продемонстрирована на примере эксперимента, в ходе которого была исследована производительность реализованных алгоритмов, примененных к анализу сетей Петри, описывающих задачу об обедающих философах разного размера. Разработанный инструмент может быть использован для дальнейшего изучения разных экземпляров конкретных формализмов, являющихся вполне структурированными система переходов, и для изучения работы реализованных алгоритмов на практике. Работа содержит 68 страниц, 4 главы, 39 рисунков, 19 таблиц, 47 источников Ключевые слова: формальная верификация, системы переходов, правильные квазипорядки, распределенные вычисления