DPN Verifier: A Toolkit for Faster Soundness Verification and Repair of Process Models with Data

DPN Verifier: A Toolkit for Faster Soundness Verification and Repair of Process Models with Data

Suvorov N.M. (NRU HSE, Moscow, Russia)

Abstract

Data Petri Nets (DPNs) extend classical Petri nets to model processes where data directly influences control-flow, enabling a comprehensive view of system behavior and possibility to detect failure points that could otherwise be hidden. Soundness is a correctness criterion that captures such failure points as deadlocks and livelocks as well as model boundedness and absence of dead activities. This paper introduces a novel soundness verification technique for DPNs that achieves significant efficiency by requiring only two state space constructions. This advancement makes soundness verification and repair applicable to larger, more complex models. We have implemented verification and repair algorithms using this technique in the DPN Verifier toolkit, a versatile tool that supports multi-perspective model analysis through various state-space structures and abstraction levels. For practicality and interoperability, the toolkit imports and exports DPNs and state-spaces using dedicated formats proposed in this paper and is delivered as a desktop application, a console application, and a class library, moving beyond a mere research prototype to offer a multifaceted platform ready for both academic and industrial use. The results of performance evaluation demonstrate that our implementation achieves lower verification and repair times for most DPNs from the literature compared to existing solutions, confirming its practical value for realistic applications.

Keywords

process models; data-aware processes; data Petri nets; soundness verification; soundness repair.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 3, part 2, 2026, pp. 49-66

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

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

For citation

Suvorov N.M. DPN Verifier: A Toolkit for Faster Soundness Verification and Repair of Process Models with Data. Proceedings of the Institute for System Programming, vol. 38, issue 3, part 2, 2026, pp. 49-66 DOI: 10.15514/ISPRAS-2026-38(3)-21.

Full text of the paper in pdf Back to the contents of the volume