Solving reachability problems on data-aware workflows

TL;DR

This paper introduces a formal verification framework for data-aware business processes, extending Workflow Nets and mapping their semantics to Action Languages, Planning, and Model Checking, with an empirical assessment of tool performance.

Contribution

It provides a novel, expressive, and empirically tractable class of data-aware process models and a rigorous mapping to formal reasoning paradigms for verification.

Findings

Effective verification of reachability on data-aware processes is feasible.

Mapping models to formal paradigms enables the use of existing verification tools.

Performance assessment shows practical viability of the approach.

Abstract

Recent advances in the field of Business Process Management have brought about several suites able to model complex data objects along with the traditional control flow perspective. Nonetheless, when it comes to formal verification there is still the lack of effective verification tools on imperative data-aware process models and executions: the data perspective is often abstracted away and verification tools are often missing. In this paper we provide a concrete framework for formal verification of reachability properties on imperative data-aware business processes. We start with an expressive, yet empirically tractable class of data-aware process models, an extension of Workflow Nets, and we provide a rigorous mapping between the semantics of such models and that of three important paradigms for reasoning about dynamic systems: Action Languages, Classical Planning, and Model Checking. Then we perform a comprehensive assessment of the performance of three popular tools supporting the above paradigms in solving reachability problems for imperative data-aware business processes, which paves the way for a theoretically well founded and practically viable exploitation of formal verification techniques on data-aware business processes.