Specification and Verification of Declarative Open Interaction Models (eBook)

A Logic-Based Approach

Marco Montali (Autor)

eBook Download: PDF

2010 | 1. Auflage
416 Seiten
Springer-Verlag
978-3-642-14538-4 (ISBN)

Infos

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. TOC:Introduction.-Declarative Open Interaction Models.-The ConDec Language.-The CLIMB Rule-Based Language.-Translating ConDec into CLIMB.-Extending ConDec.-Related Work and Summary.-Static Verification of Declarative Open Interaction Models.-Proof Procedure.-Static Verification of ConDec Models With g-SCIFF.-Experimental Evaluation.-Related Work and Summary.-Run-time Verification.-Monitoring and Enactment with Reactive Event Calculus.-Declarative Process Mining.-Related Work and Summary.-Conclusion and Future Work

Inhalt

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

Produkt-Details

• Erscheint lt. Verlag: 1.1.2010
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Datenbanken
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• ISBN-10: 3-642-14538-8 / 3642145388
• ISBN-13: 978-3-642-14538-4 / 9783642145384