Integrating data and processes to understand their concrete interplay is a long-standing problem in business process management. We present a general framework for the formalization and verification of infinite-state transition systems that can interact with a persistent storage represented as relational databases. We develop sophisticated algorithmic techniques, based on automated reasoning and SMT solving, for the verification of safety properties. Building on top of these techniques, we apply our framework to business process management: we introduce general models for the safety verification of complex business processes enriched with real data. For those models, we devise formal and operational methods that are based on standard languages and/or can capture advanced modeling capabilities, considering in particular the BPMN standard and variants of Petri nets for the process control-flow, and SQL queries and updates for the interaction with data.
Data-Aware Processes. In recent years, a growing number of application domains asks for
process modeling languages paired with automated verification techniques that do not just
consider the control flow dimension, but also take into consideration the data dimension. From
a theoretical perspective, the development of formal, abstract frameworks for attacking the
problem of verifying so-called Data-Aware Processes (DAPs) has consequently flourished [
One may wonder whether formal frameworks for verifying DAPs can employ the techniques
used in finite-state model checking. Verification of DAPs should reflect the possibility of
expressing properties that simultaneously account for the data and the process perspectives,
and most importantly for their interaction. However, due to the presence of data, DAP models are
intrinsically infinite-state : the content of a relational database is finite but its size is unbounded
and unknown a priory (since a new tuple can always be added to some relation using data
elements taken from infinite domains); in addition, many real-world scenarios often require
the presence of possibly fresh data values (e.g., string, new identifiers, integer or real numbers)
injected into the process by external users. In such sophisticated settings, explicit model
checking is not possible anymore: due to the infinity of the state space, exhaustive search
cannot be applied. Moreover, traditional approaches in data management do not help here,
since they typically investigate static, structural aspects of a domain of interest, disregarding
dynamics [
Business Processes enriched with Data. While theoretical DAP frameworks were studied,
a huge body of research has been dedicated to the challenging problem of reconciling data and
business process management within contemporary organizations [
To overcome this fundamental limitation, many concrete languages and corresponding
formalisms have been proposed to represent business processes where the data and the
controllfow dimension are both considered as first-class citizens [
Moreover, currently there are few theoretical frameworks that also come with a corresponding implemented tool for concrete verification, which is one of the desiderata for every model checking application domain. Finally, an orthogonal challenging dimension regards the abstract lfavor of these frameworks and their modeling constructs, which often depart from those ofered by process and data modeling standard languages used in practice, such as the Business Process Model and Notation (BPMN) for processes, and the Structured Query Language (SQL) for persistent data. In fact, it is essential to rely on standard languages when dealing with real applications, considering that model checking should have a big impact in guaranteeing trustworthiness of concretely deployed systems.
Infinite-state Model Checking. In parallel, in the nineties, a completely separated line of
research started to investigate how to attack the problem of verifying infinite-state systems
in general, disregarding the data perspective. A particularly interesting class of infinite-state
systems is given by parameterized systems [
Another successful way for tackling infinite-state model checking consists of providing a
symbolic setting [
At the same time, many approaches to symbolic reasoning for infinite-state systems have been successfully applied to diferent models, such as parameterized systems. Most of these approaches provide not only a solid theoretical framework, but also the support of computationally eficient and highly engineered tools. This is the case of SMT solvers and model checkers based on them. Nevertheless, importing SMT-based model checking in the context of DAP verification is extremely challenging and cannot be done as is: it requires carrying out genuinely novel research for handling the data perspective, and to develop algorithmic techniques. In this work, we bridge the gap between DAP verification and infinite-state model checking : (i) we propose a theoretical SMT-based framework for DAP verification and, to make it efective in practice, we devise eficient algorithmic techniques based on automated reasoning; (ii) we apply the previous machinery to provide practical approaches for modeling and verifying business processes enriched with real data.
DAP Verification via SMT. We define a general model-theoretic/algebraic framework, called (Universal) RASs, for automated verification of DAPs based on SMT solving, focusing in particular on parameterized safety: this amounts to establishing whether a system can reach an undesired, unsafe configuration, irrespective of the specific content of its background data storage. Our approach relies on array-based systems: we incorporate the needed capabilities to formalize and reason about relational databases. We exhibit how arrays can represent read-write relations that can be queried and updated during the evolution of the system.
For this purpose, we develop sophisticated algorithmic techniques building on top of wellknown methods in automated reasoning. We also demonstrate the feasibility of our approach by showing these techniques in action thanks to the implementation in the state-of-the-art mcmt model checker, testing it against a concrete DAP benchmark: in this respect we provide a ifrst, preliminary experimental evaluation of our verification machinery.
Modeling and Verification of Data-Aware Business Processes. As a second, key contribution, we exploit the developed machinery to provide BPM-oriented practical approaches, strictly linked to other major research lines on modeling and verifying processes with data.
First, within the general framework of RASs, we propose Data-Aware BPMN models, called DABs, based on standard languages used in the BPM literature. These models natively combine process modeling and querying languages used in practice (BPMN+SQL) in terms of a significant subset of this combination, exhibiting how this subset can be both automatically translated into the formal verification framework of RASs. These models are implemented and executed in an operational framework called delta-BPMN, where a standard process execution engine (provided by Camunda) is enriched with data management features, i.e., with the support of relational databases and data manipulation capabilities.
Then, we introduce a theoretical formalism, called COA-nets, that captures expressive modeling capabilities in the recently born spectrum of so-called object-centric processes. COA-nets are in line with process modeling principles studied in process research, specifically Petri nets and their extensions, and represent an extension of Colored Petri nets that is able both to model data lfow in tokens and to access a relational database. Once again, the translation to the verification framework of Universal RASs is provided. We explicitly discuss ways of modeling process and data interactions along a comprehensive setting, where expressive modeling patterns are introduced and shown how to employed in practice without hampering verification guarantees.