DPN-Soundness-Verification

В репозитории опубликован код для проверки корректности моделей процессов, зависящих от данных, представленных в виде сетей Петри с данными (Data Petri Nets, DPN). Авторы рассматривают более реалистичный сценарий, где поведение процесса определяется не только его структурой, но и значениями переменных. Главный результат работы — новый алгоритм проверки так называемой корректности с учётом данных. Авторы показывают, что один из прежних алгоритмов в общем случае даёт неверный результат и может не замечать некоторые случаи зацикливания. Чтобы исправить это, они предлагают сначала уточнить модель, разбивая переходы, которые изменяют переменные внутри циклов, затем добавить специальные немые переходы и после этого построить систему переходов с метками, где вершина описывает не одно конкретное состояние, а целое множество состояний с одинаковой маркировкой и разными значениями переменных. Метод реализован в виде исследовательского прототипа — настольного приложения на .NET с импортом моделей, визуализацией сети и проверкой через SMT-решатель Z3. Эксперименты показывают, что для моделей размером до 30 переходов проверка обычно занимает меньше 20 секунд, а для моделей до 60 переходов — меньше 10 минут. Код инструмента опубликован в открытом репозитории DataPetriNet. Работа будет полезна исследователям в области анализа и верификации процессов, формальных методов и process mining, а также разработчикам систем, где ход выполнения зависит от данных и условий принятия решений, а значит требует более строгой проверки, чем обычные модели бизнес-процессов.

статья | код