Reasoning with Data-Centric Business Processes

TL;DR

This paper introduces a novel approach for modeling and reasoning about data-centric business processes using a fragment-based method and first-order logic, enabling more flexible verification of process correctness.

Contribution

It extends existing model checking techniques by allowing reasoning over process fragments with data constraints, utilizing a tableau procedure and theorem provers for verification.

Findings

Developed a fragment-based modeling approach for data-centric processes.

Created a tableau-based model checking method reducing problems to first-order logic.

Performed initial experiments demonstrating the approach's feasibility.

Abstract

We describe an approach to modelling and reasoning about data-centric business processes and present a form of general model checking. Our technique extends existing approaches, which explore systems only from concrete initial states. Specifically, we model business processes in terms of smaller fragments, whose possible interactions are constrained by first-order logic formulae. In turn, process fragments are connected graphs annotated with instructions to modify data. Correctness properties concerning the evolution of data with respect to processes can be stated in a first-order branching-time logic over built-in theories, such as linear integer arithmetic, records and arrays. Solving general model checking problems over this logic is considerably harder than model checking when a concrete initial state is given. To this end, we present a tableau procedure that reduces these model checking problems to first-order logic over arithmetic. The resulting proof obligations are passed on to appropriate "off-the-shelf" theorem provers. We also detail our modelling approach, describe the reasoning components and report on first experiments.