Specification and Verification of Declarative Open Interaction Models: A Logic-Based Approach

✍ Scribed by Marco Montali

• Publisher: Springer
• Year: 2010
• Tongue: English
• Leaves: 416
• Series: Lecture Notes in Business Information Processing
• Edition: 1st Edition.
• Category: Library

✦ Synopsis

Many novel application scenarios and architectures in business process management or service composition are characterized by a distribution of activities and resources, and by complex interaction and coordination dynamics. In this book, Montali answers fundamental questions on open and declarative modeling abstractions via the integration and extension of quite diverse approaches into a computational logic-based comprehensive framework. This framework allows non IT experts to graphically specify interaction models that are then automatically transformed into a corresponding formal representation and a set of fully automated sound and complete verification facilities. The book constitutes a revised and extended version of the author’s PhD thesis, which was honored with the 2009 “Marco Cadoli” prize, awarded by the Italian Association for Logic Programming for the most outstanding thesis focusing on computational logic, discussed between the years 2007 and 2009.

✦ Table of Contents

Cover......Page 1
Specification and Verification
of Declarative Open
Interaction Models......Page 3
Lecture Notes
in Business Information Processing 56......Page 2
ISBN-10 364214537X......Page 4
Foreword......Page 6
Preface......Page 8
Acronyms......Page 11
Contents......Page 13
1
Introduction......Page 21
Specification of Open Declarative Interaction Models......Page 23
Run-Time Verification, Monitoring and Enactment Facilities......Page 24
A-Posteriori Verification and Declarative Process Mining......Page 25
Part I: Specification......Page 26
Part II: Static Verification......Page 27
Web Site......Page 28
Part I Specification......Page 29
Interaction Abstractions: Activity, Event, Execution Trace......Page 30
Characterization of Time......Page 32
Compliance......Page 33
Flexibility......Page 35
Openness......Page 38
Business Process Management......Page 39
Modeling Business Processes......Page 41
Limits of Procedural Business Process Modeling......Page 42
Service Oriented Architecture......Page 44
Orchestration and Choreography......Page 45
Limits of Procedural Choreography Modeling......Page 48
Multi-Agent Systems......Page 53
Clinical Guidelines......Page 55
Basic Medical Knowledge and Clinical Guidelines......Page 56
Semi-Openness of Clinical Guidelines......Page 57
Lesson Learnt: Compliance vs. Flexibility......Page 58
Desiderata for a Supporting Framework......Page 60
Internal Life Cycle......Page 61
Participation to an External Life Cycle......Page 62
The CLIMB Framework......Page 63
ConDec in a Nutshell......Page 65
ConDec Models......Page 66
Existence Constraints......Page 67
Choice Constraints......Page 68
Relation Constraints......Page 69
Negation Constraints......Page 72
Branching Constraints......Page 74
ConDec at Work......Page 75
The Order Management Choreography as a Contract......Page 76
Identification of Activities......Page 77
Elicitation of Business Constraints......Page 78
Completing the ConDec Model......Page 81
Usability of ConDec......Page 82
Linear Temporal Logic......Page 85
Syntax of Linear Temporal Logic......Page 86
Semantics of Linear Temporal Logic......Page 87
The Translation Function......Page 88
LTL Entailment as a Compliance Evaluator......Page 89
Linear Temporal Logic and Finite ConDec Traces......Page 90
The CLIMB Language in a Nutshell......Page 94
Event Occurrences and Execution Traces......Page 96
Constraint Logic Programming......Page 98
Expectations......Page 100
Integrity Constraints......Page 102
The Static Knowledge Base......Page 107
SCIFF-lite and Composite Events......Page 110
CLIMB Declarative Semantics......Page 112
Abduction......Page 113
Abductive Logic Programming......Page 115
Formalizing Interaction Models and Their Executions......Page 116
SCIFF-lite Specifications......Page 118
CLIMB Abductive Explanations......Page 119
On the Formal Definition of Compliance......Page 122
Equivalence Modulo Compliance......Page 126
Compositionality Modulo Compliance......Page 127
Replaceability of Rules......Page 130
5
Translating ConDec into CLIMB......Page 132
Translation of a ConDec Model......Page 133
Temporal Contiguity......Page 134
Compact Execution Traces......Page 136
Translation of Existence Constraints......Page 138
Translation of Choice Constraints......Page 140
Translation of Relation and Negation Constraints......Page 142
Dealing with Branching ConDec Constraints......Page 145
Equivalence of ConDec Constraints......Page 147
Soundness of the Translation......Page 149
Trace Mapping......Page 150
Soundness......Page 151
On the Expressiveness of SCIFF......Page 154
Metric Constraints......Page 156
Temporal Contiguity in a Quantitative Setting......Page 157
Quantitative Formalization of Chain Constraints......Page 158
Extending ConDec with Quantitative Temporal Constraints......Page 159
Examples of Data Aware Business Constraints......Page 162
The MXML Meta Model......Page 164
The Life Cycle of Non Atomic Activities in ConDec++......Page 165
Representing Non Atomic Activities and Data......Page 166
Modeling Data Aware Conditions......Page 167
Modeling the Submit&Review Process Fragment......Page 171
Formalizing Data and Data Aware Conditions......Page 172
Formalizing the Effect of Roles......Page 173
Formalizing the Activity Life Cycle......Page 176
Business Process Management......Page 179
Clinical Guidelines......Page 182
Service Oriented Computing......Page 185
Multi-Agent Systems......Page 186
Summary of the Part......Page 188
Part II Static Verification......Page 190
Desiderata for Static Verification Technologies......Page 191
Verification of a Single Model vs. a Composition of Models......Page 193
Existential vs. Universal Properties......Page 194
General vs. Particular Properties......Page 195
On the Safety-Liveness Classification......Page 196
A ConDec Example......Page 198
A-Priori Compliance Verification......Page 200
Composing ConDec Models......Page 201
Compatibility between Local Models......Page 202
Augmenting ConDec with Roles and Participants......Page 204
From Openness to Semi-Openness......Page 206
Conformance with a Choreography......Page 210
9
Proof Procedures......Page 214
Fulfilled, Violated and Pending Expectations......Page 215
Data Structures and Proof Tree......Page 216
Transitions......Page 218
Soundness......Page 227
Completeness......Page 228
Termination......Page 229
The g-SCIFF Proof Procedure......Page 231
Generation of Intensional Traces......Page 232
Data Structures Revisited......Page 233
Transitions Revisited......Page 234
Linking the Proof Procedures......Page 235
Completeness Modulo Trace Generation......Page 236
Termination......Page 238
Implementation of the Proof Procedures......Page 240
Specification of Properties with ConDec......Page 241
Formalizing Existential and Universal Entailment......Page 243
Verification of Existential Properties with g-SCIFF......Page 244
Existential Entailment with g-SCIFF......Page 245
Complementation of Integrity Constraints......Page 246
Reducing Universal to Existential Entailment......Page 248
ConDec Loops and Termination of g-SCIFF......Page 251
Constraints Reformulation......Page 252
Looping ConDec Models......Page 253
A Preprocessing Procedure......Page 258
Verification Procedure with g-SCIFF......Page 262
The Branching Responses Benchmark......Page 264
The Alternate Responses Benchmark......Page 266
The Chain Responses Benchmark......Page 269
Existential and Universal Entailment of ConDec Properties in LTL......Page 272
ConDec Properties Verification as Satisfiability and Validity Problems......Page 273
Model Checking......Page 275
Reduction of Validity and Satisfiability to Model Checking......Page 277
Verification Procedure by Model Checking......Page 279
The Order&Payment Benchmarks......Page 280
Discussion......Page 281
Verification of Properties......Page 287
A-Priori Compliance Verification......Page 291
Model Composition......Page 293
Interoperability and Choreography Conformance......Page 294
Summary of the Part......Page 295
Part III Run-Time and A-Posteriori Verification......Page 297
13
Run-Time Verification......Page 298
The Run-Time Verification Task......Page 299
SCIFF-Based Run-Time Verification......Page 300
Open Derivations......Page 301
Semi-Open Reasoning......Page 304
The SOCS-SI Tool......Page 307
The Need for Speculative Reasoning......Page 309
Speculative Verification with the g-SCIFF Proof Procedure......Page 310
Interleaving the Proof Procedures......Page 312
Monitoring Issues and SCIFF......Page 314
Event Calculus......Page 316
The Event Calculus Ontology......Page 317
Domain-Dependent vs. Domain-Independent Axioms......Page 318
Reasoning with Event Calculus......Page 319
Axiomatization of the Reactive Event Calculus......Page 321
Monitoring an Event Calculus Specification with the SCIFF Proof Procedure......Page 324
Formalizing the Personnel Monitoring Facility in REC......Page 325
Monitoring a Concrete Instance......Page 327
The Irrevocability Issue......Page 328
Soundness, Completeness, Termination......Page 329
Irrevocability of REC......Page 330
Monitoring Optional ConDec Constraints with REC......Page 333
Representing ConDec Optional Constraints in the Event Calculus......Page 334
Identification and Reification of Violations......Page 337
Compensating Violations......Page 340
Monitoring Example......Page 341
Enactment of ConDec Models......Page 344
Blocking Non Executable Activities......Page 345
Termination of the Execution......Page 348
jREC: Embedding REC Inside a JAVA-Based Tool......Page 349
15
Declarative Process Mining......Page 351
Declarative Process Mining with ProM, SCIFF Checker and DecMiner......Page 353
The SCIFF Checker ProM Plug-in......Page 354
CLIMB Textual Business Constraints......Page 355
A Methodology for Building Rules......Page 356
Specification of Conditions......Page 357
Trace Analysis with Logic Programming......Page 358
Embedding SCIFF Checker in ProM......Page 359
Case Studies......Page 361
The Think3 Case Study......Page 362
Conformance Verification of a Cervical Cancer Screening Process......Page 365
Quality Assessment in Large Wastewater Treatment Plans......Page 366
Inductive Logic Programming for Declarative Process Discovery......Page 369
Embedding DecMiner into the ProM Framework......Page 370
The Checking–Discovery Cycle......Page 372
Run-Time Verification and Monitoring......Page 374
Enactment......Page 379
Process Mining......Page 380
Summary of the Part......Page 382
Part IV Conclusion and Future Work......Page 384
Conclusion......Page 385
Termination of Static Verification and ConDec Extensibility......Page 386
Integration of Regulative and Constitutive Rules......Page 387
Development of an Editor and Enactment Prototype......Page 388
Integration of Declarative and Procedural Models......Page 389
References......Page 390