Abstract
In recent years, a huge body of research has been devoted to the challenging problem of integrating data and processes to achieve a more comprehensive understanding on their concrete interplay within business process management. This requires to investigate how data influence the process behavior, and how the control flow of the process impacts on the data it queries and manipulates. The development of theoretical frameworks for the formalization and the verification of such Data-Aware Processes (DAPs) has consequently flourished. These frameworks present two main drawbacks: first, the results obtained are usually achieved at a quite abstract level, with strong assumptions on the underlying model that do not match those of front-end languages used in practice; second, the studied verification techniques, when concretely implemented, are developed ad hoc, without appealing to well-established automatic tools.
In this thesis, we tackle this twofold problem by attacking the verification of DAPs with solid techniques for the verification of infinite-state systems. To do so, we start from the observation that many approaches to symbolic reasoning for infinite-state systems have been developed in the realm of model checking, providing not only solid foundations to the verification tasks of interest, but also highly efficient technologies, such as those stemming from SMT solvers. In this respect, the thesis aims at bridging the gap existing between DAP verification and SMT-based infinite-state model checking, focusing in particular on safety. This amounts to establishing whether a system can reach an undesired, unsafe configuration. We propose a general framework for modeling and verifying DAPs that relies on model-theoretic algebra and on SMT solving. To make our verification machinery efficient, we develop sophisticated algorithmic techniques that build on and extend well-established automated reasoning methods. We demonstrate the feasibility of our approach by showing its implementation in the state-of-the-art MCMT model checker: we provide a preliminary evaluation by testing the MCMT capabilities against a DAP benchmark. Finally, we apply our general framework to business process management: we introduce formal and operational settings that are based on standard languages and/or can capture advanced modeling capabilities.