DPNVerifier

В репозитории опубликован код DPN Verifier — инструментария для проверки и исправления бездефектности моделей процессов с данными. Работа рассматривает Data Petri Nets, расширение сетей Петри, где переходы зависят не только от разметки, но и от значений переменных. Такая постановка нужна для процессов, в которых данные напрямую меняют поток управления, а ошибки могут проявляться как deadlock, livelock, неограниченный рост ресурсов или действия, которые никогда не выполняются. Авторы предлагают более быстрый метод проверки DPN, который требует не больше двух построений пространства состояний. Существующие подходы часто опираются на многократное построение графов, из-за чего методы плохо масштабировались и оставались ближе к исследовательским прототипам. DPN Verifier реализует новую роцедуру, добавление tau-переходов и анализ абстрактных пространств состояний, включая ARG, ACG и ACT. Сам DPN Verifier поставляется как desktop-приложение, консольная утилита и библиотека классов, поэтому его можно использовать вручную, подключать к пайплайнам моделирования или брать как основу для экспериментов с DPN. Работа будет полезна исследователям process mining, разработчикам инструментов формальной верификации и командам, которые работают с процессными моделями, где поведение зависит от данных, а проверка корректности должна быть не демонстрацией на малом примере, а частью нормального инженерного пайплайна.

статья | код