Анализ свойств сети Петри выполняется на основе ее дерева достижимости

Алгоритм построения дерева достижимости

1. Пусть S=(P1,..,Pn) граничная вершина дерева (состояние сети Петри), не являющаяся тупиковой или дублирующей. Тогда для каждого перехода tj, активированного в S, создается новая вершина S' =(Pi',..,Pn'), в которой состояние позиций Рi', i=1,...,n, определяется следующим образом:

2. ЕСЛИ Pi=So, ТО Р,' = ω

3. ЕСЛИ на пути от корневой вершины к S существует вершина S"=(Р1",..,Рn"), такая что S'>S" (Рi'>Рi"), ТО Рi'= ω

4. В противном случае значение Рi' определяется на основе срабатывания перехода tj из состояния S

5. Вершина S переопределяется как внутренняя, вершина S' становится граничной. Алгоритм заканчивает работу, когда все вершины дерева тупиковые, дублирующие или внутренние.

Дерево достижимости

Проверка свойств сети Петри по дереву достижимости

- Сеть Петри является ограниченной тогда и только тогда, когда в её дереве достижимости отсутствует символ ω. Если сеть Петри ограничена, то по её дереву можно определить емкость каждой позиции как максимальное значение соответствующей компоненты состояния сети. Даже если сеть Петри не ограничена, то емкость можно определить для позиций, в которых отсутствует ω.

- Проверка сети Петри на тупиковые состояния по дереву достижимости не требует пояснений (неконечные состояния не должны быть тупиковыми).

- Сеть Петри содержит "ловушку" тогда, и только тогда, когда на ее дереве имеется простой путь (цепочка вершин, в которой из каждой вершины исходит только одна дуга), начинающийся и заканчивающийся дублирующими вершинами и не содержащий корневую вершину.

Применение сетей Петри для проверки корректности абстрактного сценария

Сеть Петри используется для выявления ошибок абстрактного сценария технических и бизнес-систем. С этой целью сценарий трансформируем в сеть Петри и далее проверяем свойства сети. Применительно к сценарию проверяются три свойства:

1. Сеть Петри должна быть ограниченной;

2. при работе сети Петри не должны появляться неконечные тупиковые состояния, в которых не активирован ни один переход;

2. при работе сети Петри не должно возникать "ловушек" - циклов без выхода (объект может попасть в "ловушку", циклически циркулировать в ней, но не может выйти из "ловушки").

Применение сетей Петри для проверки корректности абстрактного сценария

Проверка корректности сценария бизнес-системыможет быть

организовано 2 способами:

- глобальная процедура

- локальная процедура

Сценарий бизнес-системыбудем считать корректным, если:

- корректны все образующие его сценарные модули

- модули корректно согласованы