Проверка достижимости маркировки сетей Петри при помощи инвертирования деревьев состояний для протокола передачи данных

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

Ключевые слова: сети петри, анализ пространства состояний, достижимость, инверсия, протокол передачи данных

Библиография статьи: Марков А. В. Проверка достижимости маркировки сетей Петри при помощи инвертирования деревьев состояний для протокола передачи данных / А. В. Марков, А. А. Воевода // Доклады ТУСУР. – 2014. – № 1(31). – С. 143–148.