?
DPN Verifier: A Toolkit for Faster Soundness Verification and Repair of Process Models with Data
Сети Петри с данными (DPN) являются расширением классических сетей Петри, позволяющим моделировать процессы, где данные влияют на поток управления, обеспечивая комплексное представление о поведении системы и возможность обнаружения точек отказа, которые в противном случае были бы скрыты. Одним из критериев корректности для моделей процессов является бездефектность. Модель процесса называется бездефектной, если она всегда корректно завершается и каждое действие модели представлено хотя бы в одном исполнении процесса. В данной статье представлен новый метод проверки бездефектности DPN, который требует не более двух построений пространства состояний, что существенно ниже по сравнению с предложенными и реализованными ранее алгоритмами. Это усовершенствование делает проверку бездефектности и исправление дефектных моделей применимым к моделям достаточно больших размеров. Мы реализовали алгоритмы верификации и исправления, использующие этот метод, в DPN Verifier – универсальном инструменте, поддерживающем анализ моделей посредством различных структур пространств состояний и уровней абстракции. Инструментарий позволяет импортировать и экспортировать как DPN, так и структуры пространств состояний с использованием специальных форматов, предложенных в данной статье, и поставляется в виде настольного приложения, консольного приложения и библиотеки классов, что делает инструмент применимым как для академического, так и для промышленного использования. Результаты экспериментов демонстрируют более высокую скорость нашей реализации алгоритмов верификации и исправления для большинства DPN, описанных в литературе, по сравнению с существующими решениями, что подтверждает практическую ценность предложенного нами решения для реальных приложений.