Verification of Data-Aware Processes via Satisfiability Modulo Theories

In this chapter, we provide the basic preliminaries from first-order logic that are needed for the first part of the book. We also present some notations employed in this work and some notions from model theory that will be extensively used for the technical treatment. Finally, we summarize basic notions on classical relational databases.

In this chapter, we introduce Array-based Artifact Systems – a rich and powerful theoretical framework for the formal specification and verification of Data-Aware Processes (DAPs). Specifically, we present Simple Artifact Systems (SASs), Relational Artifact Systems (RASs) and Universal Relational Artifact Systems (U-RASs).

In this chapter, we study how to guarantee termination of the SMT-based backward reachability procedures for SASs and RASs in some notable cases. Termination is a difficult problem to attack in general, in the context of array-based systems. We provide guarantees of termination in three cases. The first one is for SASs, and requires that the DB schema is “acyclic”. The other two are about suitable subclasses of RASs, for which termination is proved by exploiting arguments based on well-quasi-orders (wqos). These two classes of RASs present orthogonal features: the first one, called “RASs with Local Updates”, restricts the syntax of transition formulae but only imposes that the DB signature is acyclic (as in the case of SASs); the second one, called “RASs with Tree-like Signatures”, does not pose restrictions on the syntactic format of the logical formulae of the system, but dictates that the (artifact setting over the) DB signature has a more restrictive shape, i.e., it is a tree. Both cases are sufficiently expressive to capture interesting and concrete DAP models.

In this chapter, we provide preliminaries and basic notions on the logical notion of (uniform) interpolation. We also relate it to other well-known concepts in logic and automated reasoning, such as the equality interpolating condition and Beth Definability.

This second part of the book is devoted to studying sophisticated automated reasoning techniques to solve efficiently the problem of eliminating quantifiers in model completions. In order to do so, we first show that eliminating quantifiers in model completions \(T^*\) is equivalent to the problem of computing \(T\)-covers. The notion of cover has been studied in symbolic model checking in the context of program synthesis and verification; covers are well-known also in the tradition of non-classical logics, but under the name of “uniform interpolants”. Given this equivalence, we can lift our focus to computing covers: in this chapter, we argue how computing covers is not only essential for verifying Artifact Systems, but also for slightly more general systems (that we call “declarative transition systems”) comprising different frameworks from the literature. We dedicate the majority of this chapter to attacking the problem of finding practical and efficient cover algorithms for useful theories for DB schemas.

In this chapter, we attack the problem of computing covers in theory combinations. Theory combination is an important topic in automated reasoning, and computing combined covers is particularly interesting in view of DAP verification. We would like to investigate a general method that works for combination of DB schemas for which cover algorithms exist: in this way, whenever we get such algorithms for the component theories, we can easily combine them so as to get a combined cover algorithm for the combined DB schema. In this chapter, we theoretically study the problem of combined covers from a general perspective, by identifying the equality interpolating property as the sufficient (and, in some sense, also necessary) condition. We do so by exhibiting a concrete combined algorithm (called \(\mathsf{ConvexCombCover}\)) that modularly exploits the cover algorithms for the component theories. The key feature of this algorithm relies on the extensive usage of the Beth Definability property. We conclude the chapter by giving a combined cover algorithm (called \(\mathsf{TameCombCover}\)) for possibly non-convex theories, in case the combination is ‘tame’: \(\mathsf{TameCombCover}\) has important applications in DAP verification because it can be used in case of DB extended-schemas.

In this chapter, we give an overview of \(\mathsf{mcmt}\), the model checker that implements a prototype of our backward reachability algorithm for artifact systems, and we describe its working in the `database-driven' setting, which is the one employed for DAP verification. Finally, we provide an experimental evaluation consisting of running \(\mathsf{mcmt}\) over an interesting and significant benchmark of data-aware processes encoded into RASs.

In this chapter we provide a brief overview of the fundamental notions on the BPMN language, and basic concepts from Colored Petri nets that are useful for the BPM applications.

In this chapter, we present the first application of our verification framework to business processes. Specifically, we define a general model of Data-Aware Processes, called DAB, which is a theoretical extension of the BPMN language with full-fledged relational data. We also show how DABs can be translated into RASs, so as to transfer the verification results for RASs to this BPMN-oriented model. DABs are similar in spirit to artifact systems concerning the treatment of relational data, but employ a fragment of the BPMN language to express the process schema.

This chapter concludes the book, summarizes the contributions, and discusses future work. In this book, we provided the foundations of Data-Aware Process (DAP) safety verification based on Satisfiability Modulo Theories (SMT) solving and on automated reasoning methods. To do so, we proposed a novel general framework that relies on model-theoretic algebra. In this framework, complex processes enriched with data can be faithfully modeled as symbolic array-based transition systems. These are dynamic systems that evolve over time, where the sets of states and transitions are described symbolically, specifically using logical formulae involving arrays: in such systems, data are formalized using an algebraic representation of relational databases. We verify DAPs against safety properties by employing an extension of the backward reachability procedure. This extension requires the development of sophisticated algorithmic techniques for the treatment of the quantified data variables that are used in transitions. The procedure has been implemented in the state-of-the-art \(\mathsf{mcmt}\) model checker. We showed how this framework can be successfully applied in the context of BPM to model and verify concrete data-aware business processes: to do so, we introduced different formalisms that on the one hand build on top of standard languages used in practice, on the other hand are able to capture expressive modeling capabilities.