Semantic Methods for Execution-level Business Process Modeling - Modeling Support Through Process Verification and Service Composition

Foreword

Preface

Contents

Part I Foundations

1 Introduction

1.1 Motivation and Overview

1.2 Hypotheses

1.3 Methodology

1.4 Details of the Solution Approach

1.4.1 Verification of Annotated Process Models

1.4.2 Composition of Execution-level Artifacts

1.5 Structure of This Book

2 Background

2.1 Business Process Management

2.1.1 The Path to Business Process Management

2.1.2 Definitions

2.1.3 Overview and Methodology for BPM

2.1.4 Process Formalisms

2.1.5 Workflow Patterns

2.1.6 Current Challenges in BPM

2.2 Service-Oriented Computing

2.2.1 Service-Oriented Architecture

2.2.2 Web Services

2.2.3 Service-Orientation Design Principles

2.2.4 An Orchestration Language: WSBPEL

2.3 Semantic Technologies

2.3.1 Ontologies and Reasoning

2.3.2 Frame Logic

2.3.3 Description Logics

2.3.4 Semantic Web Services

2.3.5 Semantic Business Process Management

2.4 Chapter Summary

Part II Modeling Support through Verification and Composition

3 Requirements Analysis and Conceptual Framework

3.1 The Problem of Supporting Composition in BPM

3.2 Requirements for Composition Support in Business Process Modeling

3.2.1 Modeling Extension Requirements

3.2.2 Fundamental Requirements

3.2.3 Non-functional Requirements

3.2.4 Situational Requirements

3.3 Requirements Discussion

3.4 Conceptual Framework Overview

3.4.1 Semantics of Annotated Process Models

3.4.2 Annotating Preconditions and Effects

3.4.3 Refined Problem Description

3.5 High-Level Architecture and Components

3.5.1 Component Overview and Explanation

3.5.2 Discovery

3.5.3 Task Composition

3.5.4 Auto-completion

3.5.5 Data Mediation

3.5.6 Validation

3.6 Methodological Guidance for the Semantic BPM Life- Cycle

3.6.1 Overview

3.6.2 The Modeling Phase

3.6.3 The Configuration Phase

3.6.4 Discussion of the Methodology

3.7 Automatic Process Composition Algorithm

3.8 Related Work

3.8.1 Related

3.8.2 Related Work for the Conceptual Framework

3.9 Summary and Discussion

4 Verification of Annotated Process Models

4.1 Overview

4.2 Annotated Process Graphs

4.2.1 Process Graphs

4.2.2 Semantic Annotations

4.3 Verification Tasks

4.4 Checking Precondition and Effect Conflicts

4.5 Computational Hardness of Executability and Reachability Checking

4.6 Polynomial-Time Executability Checking for Basic Processes

4.7 Resolving Inconsistencies

4.7.1 Executability

4.7.2 Precondition and Effect Conflicts

4.8 Related Work

4.8.1 Petri Nets

4.8.2 Model Checking

4.8.3 Beyond Control-Flow

4.9 Chapter Conclusion and Discussion of Open Questions

5 Task Composition

5.1 Overview

5.2 Design and Main Algorithms

5.2.1 Overall Arrangement

5.2.2 Forward Search

5.2.3 A Non-deterministic Search Algorithm

5.3 Formalizing Web Service Composition

5.3.1 WSC Syntax

5.3.2 WSC Semantics

5.4 Update Reasoning

5.4.1 Basic Aspects of the Search

5.4.2 General and Horn Background Theory

5.4.3 Binary Background Theory

5.4.4 Approximate Update Reasoning

5.5 Heuristic Function

5.5.1 Main Approach of the Heuristic Function

5.5.2 Building an Approximated Composition Graph

5.5.3 Extracting an Approximated Solution

5.6 Peripherals

5.6.1 Information Gathering

5.6.2 Discovery

5.7 Related Work

5.7.1 AI Planning

5.7.2 Update Problems

5.7.3 Web Service Composition

5.8 Chapter Conclusion

Part III Finale

6 Evaluation

6.1 Evaluation Overview

6.2 Prototypes

6.2.1 Back-End Components

6.2.2 Integrated Prototypes

6.3 Empirical Results for Task Composition

6.3.1 Performance with Deterministic Simulated Services

6.4 Process Case Studies

6.4.1 General Observations

6.4.2 Overview of the Process Case Studies

6.4.3 Findings

6.5 Chapter Summary

7 Conclusions and Outlook

7.1 Summary

7.2 Open Problems

7.3 Future Research Topics

7.4 Reflection

Appendix: A Proofs

A.1 Proofs for the Verification Technique

A.1.1 Correctness of M-Propagation

Lemma A.1.

Proof:

Lemma A.2.

Proof:

Lemma A.3.

Proof:

Lemma A.4.

Proof:

Base case.

Inductive case.

Lemma A.5.

Proof:

Base case.

Inductive case.

Theorem 4.14.

Proof:

A.1.2 Binary Theories Can Be Compiled Away

Lemma A.6.

Proof:

A.1.3 Correctness of I-Propagation

Lemma A.7.

Proof:

Base case.

Inductive case.

Lemma A.8.

Proof:

Lemma A.9.

Proof:

Theorem 4.21.

Proof:

A.1.4 I-Propagation Can Be Used for Executability Checking

Lemma 4.22.

Proof:

Theorem 4.23.

Proof:

Theorem 4.24.

Proof:

A.1.5 Complexity Results

Lemma A.10.

.p

coNP-hard

Sp

NP-

Proof:

.p

Sp

.p

Sp

Lemma A.11.

coNP-

Proof:

. . .

Fig. A.1.

Lemma A.12.

coNP-

Proof:

Lemma A.13.

coNP-

NP-

Proof:

Theorem 4.18.

.p

coNP-

Proof:

Theorem 4.19.

Sp

NP-

Proof:

A.2 Proofs for Task Composition

Theorem 5.2.

coNP- Proof:

coNP:

NP

Theorem 5.3.

Proof:

Lemma 5.4.

Proof:

Lemma 5.5.

Proof:

Lemma 5.6.

Proof:

Theorem 5.7.

Proof:

Theorem 5.8.

Proof:

Lemma 5.9.

Proof:

Lemma 5.10.

Proof:

Lemma 5.11.

Proof:

Observation 5.14.

Observation 5.15.

References

Index