Verification of Data-Aware Processes via Satisfiability Modulo Theories (Lecture Notes in Business Information Processing)

✍ Scribed by Alessandro Gianola

• Publisher: Springer
• Year: 2023
• Tongue: English
• Leaves: 335
• Category: Library

✦ Synopsis

This book is a revised version of the PhD dissertation written by the author at the Free University of Bozen-Bolzano in Italy.

It presents a new approach to safety verification of a particular class of infinite-state systems, called Data-Aware Processes (DAPs). To do so, the developed technical machinery requires to devise novel results for uniform interpolation and its combination in the context of automated reasoning. These results are then applied to the analysis of concrete business processes enriched with real data.

In 2022, the PhD dissertation won the “BPM Dissertation Award”, granted to outstanding PhD theses in the field of Business Process Management.

✦ Table of Contents

Preface
Contributions
Book Structure
Detailed Index of Main Notions
Acknowledgements
Contents
Acronyms
Chapter 1 Introduction
1.1 Overview
1.1.1 Finite-State Model Checking
1.1.2 Verification of Data-Aware Processes
1.1.3 Infinite-State Model Checking: from Parameterized Systems to SMT Verification
1.1.4 Main Goal of the Book
1.2 Related Literature
1.2.1 Formal Models for Data-Aware (Business) Processes
1.2.2 Verification of Data-Aware Processes
1.2.3 Model Checking for Infinite-State Systems using SMT-based Techniques
1.3 Contributions of the Book
1.3.1 Contributions of the First Part
1.3.2 Contributions of the Second Part
1.3.3 Contributions of the Third Part
Part I Foundations of SMT-based Safety Verification of Artifact Systems
Chapter 2 Preliminaries from Model Theory and Logic
2.1 Preliminaries
2.2 Substructures and Embeddings
2.3 Robinson Diagrams and Amalgamation
2.4 Model Completions
2.5 Satisfiability Modulo Theories (SMT)
2.6 Definable Extensions and λ-Notations
2.7 Typed Relational Databases with Constraints
Chapter 3 Array-Based Artifact Systems: General Framework
3.1 Read-Only DB Schemas
3.1.1 Relational View of DB Schemas
3.1.2 DB Extended-Schemas
3.2 Array-Based Artifact Systems
3.2.1 Simple Artifact Systems
3.2.2 Universal Relational Artifact Systems
Chapter 4 Safety Verification of Artifact Systems
4.1 Model-Theoretic Requirements of DB Schemas
4.1.1 Finite Model Property
4.1.2 The Constraint Satisfiabilty Problem Is Decidable
4.1.3 Model Completion of DB Theories
4.1.4 Assumption for the Technical Machinery
4.2 Parameterized Safety via Backward Reachability for SASs
4.3 Parameterized Safety via Backward Reachability for U-RASs and RASs
4.4 Handling U-RASs via SMT-based Backward Reachability
4.4.1 Eliminating Universal Quantifiers from U-RASs
4.4.2 Modified SMT-based Backward Search for U-RASs
4.5 Effectiveness and Soundness for BReachRAS
4.6 Examples of DB Schemas Satisfying the Assumption
4.6.1 Examples of DB Theories with the Finite Model Property
4.6.2 Examples of Model Completions of DB Theories
4.7 Discussion
4.7.1 Model Checking via Quantifier Elimination in Model Completions
4.7.2 Freshness and Related Approaches
Chapter 5 Decidability Results via Termination of the Verification Machinery
5.1 Termination Result for SASs
5.2 Termination Results for RASs
5.2.1 Termination with Local Updates
5.2.2 Proof of Theorem 5.2 and an Example of (Strongly) Local RAS
5.2.3 Termination with Tree-Like Signatures
5.2.4 Proof of Theorem 5.4 and an Example of Tree-Like RAS
5.3 Operations Representable as Strongly Local Transitions
5.3.1 Deletion Updates
5.3.2 Insertion Updates
5.3.3 Propagation Updates
5.3.4 Bulk Updates
5.4 A Summary of the Comparison with Related DAP Formalisms
Part II Automated Reasoning Techniques for Data-Aware Process Verification
Chapter 6 Preliminaries for (Uniform) Interpolation
6.1 General Preliminaries
6.1.1 Preliminaries on Uniform Interpolants or Covers
6.2 Preliminaries on the Equality Interpolating Condition and Beth Definability
Chapter 7 Uniform Interpolation for Database Theories (and Beyond)
7.1 Uniform Interpolation, Covers and Model Completions
7.2 Model-Checking Applications
7.2.1 Covers for Database Schemas
7.3 Covers via Constrained Superposition
7.4 Complexity Analysis of the Fragment for Database-Driven Applications
7.5 An Extension of the Constrained Superposition Calculus
7.6 Remarks on MCMT Implementation
Chapter 8 Combination of Uniform Interpolants for DAPs Verification
8.1 Interpolation, Equality Interpolating Condition and Beth Definability
8.2 Convex Theories
8.3 The Convex Combined Cover Algorithm
8.3.1 The Necessity of the Equality Interpolating Condition.
8.3.2 An Example of Cover Computation
8.4 The Non-Convex Case: a Counterexample
8.5 Tame Combinations
8.5.1 An Example of Combined Covers for the Tame Combination
8.6 Discussion on Related Works on Covers
Chapter 9 MCMT: a Concrete Model Checker for DAPs
9.1 MCMT: a Brief Overview
9.2 Basic Syntax of MCMT
9.3 MCMT Specifications: Database-Driven Mode
9.3.1 DB Schema Declaration
9.3.2 Initialization
9.3.3 Unsafe States
9.3.4 Elimination of Existentially Quantified Variables
9.3.5 Transitions
9.3.6 Universal Quantifiers in Guards
9.4 Running MCMT
9.4.1 Displayed Information
9.5 Experiments on Concrete Data-Aware Processes
Part III Applications
Chapter 10 Business Process Management and Petri Nets: Preliminaries
10.1 Business Process Management
10.1.1 BPMN Basic Blocks and Concepts
10.1.2 Process Cases and Execution Semantics: an Informal View
10.1.3 Complex BPMN blocks
10.2 Colored Petri Nets
10.2.1 Data Types
10.2.2 Preliminary Notions for Colored Petri Nets
10.2.3 Definition of Colored Petri Nets
10.2.4 Semantics of CPNs
10.2.5 Execution Semantics of CPNs
Chapter 11 DABs: a Theoretical Framework for Data-Aware BPMN
11.1 Data-Aware BPMN: Main Contributions
11.2 Data-Aware BPMN
11.2.1 The Data Schema
11.2.2 Tasks, Events, and Impact on Data
11.2.3 Process Schema
11.2.4 Execution Semantics
11.3 Parameterized Safety Verification of DABs
11.3.1 Array-Based Artifact Systems and Safety Checking: a Brief Summary
11.3.2 Verification Problems for DABs
11.3.3 Translating DABs into Array-Based Artifact Systems
11.3.4 Verification Results
11.4 First Experiments with MCMT
Chapter 12 delta-BPMN: the Operational and Implemented Counterpart of DABs
12.1 From DABs to delta-BPMN
12.1.1 DABs: a Symbolic Bridge Between RASs and delta-BPMN
12.2 Requirement Analysis for delta-BPMN and Related Existing Tools
12.3 The PDMML Language
12.3.1 Sources of Data and their Definition
12.3.2 The Process Component of delta-BPMN
12.3.3 Inspecting and Manipulating Data with PDMML
12.3.4 Guards for Conditional Flows
12.4 delta-BPMN in Action
12.4.1 Modeling delta-BPMN Processes with Camunda
12.4.2 Encoding delta-BPMN Camunda Processes in MCMT
12.5 A Brief Discussion on Limitations of DABs and delta-BPMN
Chapter 13 Catalog Object-Aware Nets
13.1 The COA-net Formal Model
13.1.1 Modeling Capabilities
13.2 From COA-nets to MCMT
13.2.1 Universal RASs: a Summary
13.2.2 Encoding COA-nets into MCMT
13.2.3 Encoding Example
13.3 Unsafety Checking of COA-nets and its Formal Properties
13.3.1 Unsafety Properties
13.3.2 Verification Problem
13.3.3 Soundness and Completeness
13.3.4 Conservative COA-nets
13.3.5 Bounded COA-nets
13.3.6 Discussion on Undecidability of COA-nets
13.4 Comparison to Other Models
Chapter 14 Conclusions
14.1 Overview of the First Part and Relevant FutureWork
14.2 Overview of the Second Part and Relevant FutureWork
14.3 Conclusions for the Third Part and Relevant FutureWork
14.3.1 Data-Aware BPMN and delta-BPMN
14.3.2 COA-nets
14.4 Additional Open Directions
14.4.1 Verification of Artifact Systems Under Ontologies
14.4.2 Safety Verification of (Data-Aware) Multi-Agent Systems
14.5 Final Considerations
Correction to: Verification of Data-Aware Processes via Satisfiability Modulo Theories
Correction to: A. Gianola: Verification of Data-Aware Processes via Satisfiability Modulo Theories, LNBIP 470, https://doi.org/10.1007/978-3-031-42746-6
References