Рассматривается механизм верификации рабочих потоков приложений, построенных по спецификации Windows Workflow Foundation и способных изменять бизнес-логику на этапе выполнения. Предложен механизм преобразования рабочих потоков в нотации сетей Петри и приведён пример такого преобразования. Для верификации предлагается использовать математический аппарат сетей Петри, анализируя свойства бездефектности замкнутой эквивалентной сети Петри. Дано определение требований, характеризующих бездефектную сеть Петри. Ключевые слова: сети Петри, Windows Workflow Foundation, рабочие потоки, бездефектность, формальная верификация.
