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

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

1. Sidorova N., Stahl C., Trcka N. Soundness verification for conceptual workflow nets with data: Early detection of errors with the most precision possible. Information Systems, 36(7), 2011, pp. 1026-1043.

2. Tao X., Liu G., Yang B., Yan C., Jiang C., Workflow nets with tables and their soundness. IEEE Transactions on Industrial Informatics, 16(3), 2020, pp. 1503-1515.

3. de Leoni M., van der Aalst W. M. P. Data-aware process mining: Discovering decisions in processes using alignments. In Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013, pp. 1454-1461.

4. Aagesen G., Krogstie J. Bpmn 2.0 for modeling business processes. Handbook on Business Process Management 1: Introduction, Methods, and Information Systems. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 219-250.

5. van der Aalst W. M. P. Verification of workflow nets. In Application and Theory of Petri Nets 1997, 1997, pp. 407-426.

6. de Leoni M., Felli P., Montali M. A holistic approach for soundness verification of decision-aware process models. In Conceptual Modeling, 2018, pp. 219-235.

7. Felli P., de Leoni M., Montali M. Soundness verification of data-aware process models with variable-to-variable conditions. Fundamenta Informaticae, 182(1), 2021, pp. 1-29.

8. Felli P., Montali M., Winkler S. Soundness of data-aware processes with arithmetic conditions. In Advanced Information Systems Engineering, 2022, pp. 389-406.

9. Suvorov N. M., Lomazova I. A. Verification of data-aware process models: Checking soundness of data petri nets. Journal of Logical and Algebraic Methods in Programming, vol. 138, 2024, 100953.

10. Suvorov N. M., Lomazova I. A. Soundness Correction of Data Petri Nets. IEEE Access, vol. 13, 2025, pp. 149142-149157.

11. Zavatteri M., Bresolin D., de Leoni M. Repair of unsound data-aware process models. Business Process Management Workshops. Cham: Springer Nature Switzerland, 2024, pp. 383-395.

12. Felli P., Montali M., Winkler S. Repairing soundness properties in data-aware processes. In 2023 5th International Conference on Process Mining (ICPM), 2023, pp. 41 48.

13. Suvorov N. M., Lomazova I. A. Relaxed Lazy Soundness Verification for Data Petri nets. Proceedings of the Institute for System Programming of the RAS, 37(4), 2025, pp. 69-84.

14. Mendling J., Neumann G., van der Aalst W. Understanding the occurrence of errors in process models based on metrics. In Proceedings of the 2007 OTM Confederated International Conference on the Move to Meaningful Internet Systems: CoopIS, DOA, ODBASE, GADA, and IS Volume Part I, ser. OTM’07. Berlin, Heidelberg: Springer-Verlag, 2007, p. 113-130.

15. Roy S., Sajeev A., Bihary S., Ranjan A. An empirical study of error patterns in industrial business process models. IEEE Transactions on Services Computing, 7(2), 2014, pp. 140-153.

16. Roy S., Sajeev A., Gopichand A., Bhattacharya A. An empirical analysis of diagnosis of industrial business processes at sub-process levels. In 2016 IEEE International Conference on Services Computing (SCC), 2016, pp. 195-202.

17. Mendling J., Verbeek H., van Dongen B., van der Aalst W. M. P., Neumann G. Detection and prediction of errors in EPCs of the sap reference model. Data and Knowledge Engineering, 64(1), 2008, pp. 312-329.

18. de Leoni M., Munoz-Gama J., Carmona J., van der Aalst W. M. P. Decomposing alignment-based conformance checking of data-aware process models. In On the Move to Meaningful Internet Systems: OTM 2014 Conferences. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 3-20.

19. Felli P., Gianola A., Montali M., Rivkin A., Winkler S., Data-aware conformance checking with smt. Information Systems, vol. 117, 2023, 102230.

20. van der Aalst W. M. P., van Dongen B. F., Günther C. W., et al. Prom 4.0: Comprehensive support for real process analysis. In Petri Nets and Other Models of Concurrency. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 484-494.

21. Berti A., van Zelst S., Schuster D. PM4PY: A process mining library for python. Software Impacts, vol. 17, 2023, 100556.

22. Billington J., Christensen S., Van Hee K., et al. The petri net markup language: Concepts, technology, and tools. In Proceedings of the 24th International Conference on Applications and Theory of Petri Nets, ser. ICATPN’03, Eindhoven, The Netherlands: Springer-Verlag, 2003, pp. 483-505.

23. de Moura L., Bjørner N. Z3: An efficient smt solver. In TACAS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337-340.

24. Murata T. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4), 1989, pp. 541 580.

25. Mannhardt F. Multi-perspective process mining. Ph.D. dissertation, Eindhoven University of Technology, 2018.