Semantic Methods for Execution-level Business Process Modeling (eBook)

Foreword 5
Preface 7
Contents 9
Part I Foundations 13
1 Introduction 14
1.1 Motivation and Overview 14
1.2 Hypotheses 17
1.3 Methodology 18
1.4 Details of the Solution Approach 20
1.4.1 Verification of Annotated Process Models 20
1.4.2 Composition of Execution-level Artifacts 21
1.5 Structure of This Book 21
2 Background 23
2.1 Business Process Management 23
2.1.1 The Path to Business Process Management 24
2.1.2 Definitions 27
2.1.3 Overview and Methodology for BPM 28
2.1.4 Process Formalisms 35
2.1.5 Workflow Patterns 37
2.1.6 Current Challenges in BPM 37
2.2 Service-Oriented Computing 38
2.2.1 Service-Oriented Architecture 38
2.2.2 Web Services 39
2.2.3 Service-Orientation Design Principles 41
2.2.4 An Orchestration Language: WSBPEL 42
2.3 Semantic Technologies 44
2.3.1 Ontologies and Reasoning 46
2.3.2 Frame Logic 47
2.3.3 Description Logics 48
2.3.4 Semantic Web Services 49
2.3.5 Semantic Business Process Management 52
2.4 Chapter Summary 54
Part II Modeling Support through Verification and Composition 55
3 Requirements Analysis and Conceptual Framework 56
3.1 The Problem of Supporting Composition in BPM 56
3.2 Requirements for Composition Support in Business Process Modeling 59
3.2.1 Modeling Extension Requirements 60
3.2.2 Fundamental Requirements 62
3.2.3 Non-functional Requirements 65
3.2.4 Situational Requirements 68
3.3 Requirements Discussion 71
3.4 Conceptual Framework Overview 71
3.4.1 Semantics of Annotated Process Models 72
3.4.2 Annotating Preconditions and Effects 74
3.4.3 Refined Problem Description 74
3.5 High-Level Architecture and Components 76
3.5.1 Component Overview and Explanation 76
3.5.2 Discovery 78
3.5.3 Task Composition 80
3.5.4 Auto-completion 82
3.5.5 Data Mediation 84
3.5.6 Validation 86
3.6 Methodological Guidance for the Semantic BPM Life- Cycle 88
3.6.1 Overview 89
3.6.2 The Modeling Phase 91
3.6.3 The Configuration Phase 94
3.6.4 Discussion of the Methodology 97
3.7 Automatic Process Composition Algorithm 98
3.8 Related Work 100
3.8.1 Related 101
3.8.2 Related Work for the Conceptual Framework 102
3.9 Summary and Discussion 103
4 Verification of Annotated Process Models 106
4.1 Overview 107
4.2 Annotated Process Graphs 112
4.2.1 Process Graphs 112
4.2.2 Semantic Annotations 117
4.3 Verification Tasks 124
4.4 Checking Precondition and Effect Conflicts 126
4.5 Computational Hardness of Executability and Reachability Checking 133
4.6 Polynomial-Time Executability Checking for Basic Processes 139
4.7 Resolving Inconsistencies 147
4.7.1 Executability 148
4.7.2 Precondition and Effect Conflicts 149
4.8 Related Work 150
4.8.1 Petri Nets 151
4.8.2 Model Checking 153
4.8.3 Beyond Control-Flow 153
4.9 Chapter Conclusion and Discussion of Open Questions 155
5 Task Composition 158
5.1 Overview 159
5.2 Design and Main Algorithms 163
5.2.1 Overall Arrangement 164
5.2.2 Forward Search 167
5.2.3 A Non-deterministic Search Algorithm 170
5.3 Formalizing Web Service Composition 174
5.3.1 WSC Syntax 174
5.3.2 WSC Semantics 175
5.4 Update Reasoning 177
5.4.1 Basic Aspects of the Search 178
5.4.2 General and Horn Background Theory 178
5.4.3 Binary Background Theory 180
5.4.4 Approximate Update Reasoning 181
5.5 Heuristic Function 183
5.5.1 Main Approach of the Heuristic Function 184
5.5.2 Building an Approximated Composition Graph 185
5.5.3 Extracting an Approximated Solution 190
5.6 Peripherals 193
5.6.1 Information Gathering 193
5.6.2 Discovery 197
5.7 Related Work 201
5.7.1 AI Planning 202
5.7.2 Update Problems 203
5.7.3 Web Service Composition 206
5.8 Chapter Conclusion 209
Part III Finale 210
6 Evaluation 211
6.1 Evaluation Overview 211
6.2 Prototypes 215
6.2.1 Back-End Components 215
6.2.2 Integrated Prototypes 216
6.3 Empirical Results for Task Composition 221
6.3.1 Performance with Deterministic Simulated Services 222
6.4 Process Case Studies 226
6.4.1 General Observations 226
6.4.2 Overview of the Process Case Studies 227
6.4.3 Findings 229
6.5 Chapter Summary 232
7 Conclusions and Outlook 234
7.1 Summary 234
7.2 Open Problems 236
7.3 Future Research Topics 237
7.4 Reflection 237
Appendix: A Proofs 239
A.1 Proofs for the Verification Technique 239
A.1.1 Correctness of M-Propagation 239
Lemma A.1. 239
Proof: 239
Lemma A.2. 240
Proof: 240
Lemma A.3. 241
Proof: 241
Lemma A.4. 242
Proof: 242
Base case. 242
Inductive case. 242
Lemma A.5. 244
Proof: 244
Base case. 244
Inductive case. 244
Theorem 4.14. 245
Proof: 245
A.1.2 Binary Theories Can Be Compiled Away 246
Lemma A.6. 246
Proof: 246
A.1.3 Correctness of I-Propagation 248
Lemma A.7. 248
Proof: 248
Base case. 248
Inductive case. 248
Lemma A.8. 251
Proof: 251
Lemma A.9. 253
Proof: 253
Theorem 4.21. 255
Proof: 255
A.1.4 I-Propagation Can Be Used for Executability Checking 255
Lemma 4.22. 255
Proof: 256
Theorem 4.23. 256
Proof: 256
Theorem 4.24. 257
Proof: 257
A.1.5 Complexity Results 257
Lemma A.10. 257
.p 257
coNP-hard 257
Sp 257
NP- 257
Proof: 257
.p 258
Sp 258
.p 260
Sp 260
Lemma A.11. 260
coNP- 260
Proof: 260
. . . 260
Fig. A.1. 260
Lemma A.12. 262
coNP- 262
Proof: 262
Lemma A.13. 263
coNP- 263
NP- 263
Proof: 263
Theorem 4.18. 265
.p 265
coNP- 265
Proof: 265
Theorem 4.19. 265
Sp 265
NP- 265
Proof: 265
A.2 Proofs for Task Composition 266
Theorem 5.2. 266
coNP- Proof: 266
coNP: 266
NP 266
Theorem 5.3. 269
Proof: 269
Lemma 5.4. 270
Proof: 270
Lemma 5.5. 270
Proof: 270
Lemma 5.6. 271
Proof: 271
Theorem 5.7. 271
Proof: 272
Theorem 5.8. 272
Proof: 272
Lemma 5.9. 272
Proof: 272
Lemma 5.10. 273
Proof: 273
Lemma 5.11. 274
Proof: 274
Observation 5.14. 274
Observation 5.15. 275
References 276
Index 296