DPN Verifier: Инструментарий для ускоренной верификации и исправления дефектных моделей процессов с данными

DPN Verifier: Инструментарий для ускоренной верификации и исправления дефектных моделей процессов с данными

Суворов Н. М. (НИУ ВШЭ, Москва, Россия)

Аннотация

Сети Петри с данными (DPN) являются расширением классических сетей Петри, позволяющим моделировать процессы, где данные влияют на поток управления, обеспечивая комплексное представление о поведении системы и возможность обнаружения точек отказа, которые в противном случае были бы скрыты. Одним из критериев корректности для моделей процессов является бездефектность. Модель процесса называется бездефектной, если она всегда корректно завершается и каждое действие модели представлено хотя бы в одном исполнении процесса. В данной статье представлен новый метод проверки бездефектности DPN, который требует не более двух построений пространства состояний, что существенно ниже по сравнению с предложенными и реализованными ранее алгоритмами. Это усовершенствование делает проверку бездефектности и исправление дефектных моделей применимым к моделям достаточно больших размеров. Мы реализовали алгоритмы верификации и исправления, использующие этот метод, в DPN Verifier – универсальном инструменте, поддерживающем анализ моделей посредством различных структур пространств состояний и уровней абстракции. Инструментарий позволяет импортировать и экспортировать как DPN, так и структуры пространств состояний с использованием специальных форматов, предложенных в данной статье, и поставляется в виде настольного приложения, консольного приложения и библиотеки классов, что делает инструмент применимым как для академического, так и для промышленного использования. Результаты экспериментов демонстрируют более высокую скорость нашей реализации алгоритмов верификации и исправления для большинства DPN, описанных в литературе, по сравнению с существующими решениями, что подтверждает практическую ценность предложенного нами решения для реальных приложений.

Ключевые слова

слова: модели процессов; процессы, обогащенные данными; сети Петри с данными; верификация бездефектности; исправление дефектных моделей.

Издание

Труды Института системного программирования РАН, том 38, вып. 3, часть 2, 2026, стр. 49-66.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(3)-21

Для цитирования

Суворов Н. М. DPN Verifier: Инструментарий для ускоренной верификации и исправления дефектных моделей процессов с данными. Труды Института системного программирования РАН, том 38, вып. 3, часть 2, 2026, стр. 49-66. DOI: 10.15514/ISPRAS-2026-38(3)-21.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома