Традиционный подход к моделированию процессов, ориентированный на поток управления, всё чаще дополняется перспективой данных для обеспечения более точного и глубокого анализа поведения процесса. В докладе рассматриваются возможности формального представления интегрированных моделей, включающих в себя как поток управления,так и поток данных, а также возможности проверки свойства бездефектности для таких моделей. Модель процесса называется бездефектной, если она всегда корректно завершается и каждое действие модели присутствует хотя бы в одном в экземпляре процесса. Верификация данного свойства сразу после проектирования процесса позволяет выявить и устранить ошибки проектирования до его реализации.В докладе демонстрируются как методы верификации бездефектности, так и методы автоматического исправления некорректных моделей с данными, позволяющие исключить исполнения процесса, ведущие к точкам отказа. В качестве формализма используются сети Петри с данными — расширение сетей Петри, где каждый переход сопровождается ограничением, определяющим входные и выходные условия назначения переменных.

Литература:

1. 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. 2024. Vol. 138. 100953.
2. Suvorov N. M., Lomazova I. A. Soundness Correction of Data Petri Nets // IEEE Access. 2025. Vol. 13. P. 149142-149157.
3. P. Felli, M. de Leoni, and M. Montali, "Soundness verification of data-aware process models with variable-to-variable conditions", Fundam. Informaticae, vol. 182, no. 1, pp. 1–29, 2021.
4. P. Felli, M. Montali, and S. Winkler, "Repairing soundness properties in data-aware processes" 2023 5th International Conference on Process Mining (ICPM), 2023, pp. 41–48.
5. P. Felli, M. Montali, and S. Winkler, "Soundness of data-aware processes with arithmetic conditions", in Advanced Information Systems Engineering, X. Franch, G. Poels, F. Gailly, and M. Snoeck, Eds., Cham:Springer International Publishing, 2022, pp. 389–406.
6. M. Zavatteri, D. Bresolin, and M. de Leoni, "Repair of unsound data-aware process models", in Business Process Management Workshops, J. De Weerdt and L. Pufahl, Eds. Cham: Springer Nature Switzerland, 2024, pp.383–395.
7. I. Lomazova, L. Popova-Zeugmann, and A. Bartels, "Controlling boundedness for live petri nets", in 2017 4th International Conference on Control, Decision and Information Technologies (CoDIT), 2017, pp.0236–0241.
8. N. Sidorova, C. Stahl, and N. Trcka, "Soundness verification for conceptual workflow nets with data: Early detection of errors with the most precision possible", Information Systems, vol. 36, no. 7,pp. 1026–1043, Nov. 2011.
9. W. M. P. van der Aalst, "Verification of workflow nets", Application and Theory of Petri Nets 1997, P. Azema and G. Balbo,Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 407–426

Слайды доклада

Видео доклада (Youtube)

Видео доклада (VK Видео)