Montali Specification and Verification of Declarative Open Interaction Models

A Logic-Based Approach
1. Auflage 2010
ISBN: 978-3-642-14538-4
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 56, 416 Seiten

Reihe: Lecture Notes in Business Information Processing

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

Autoren/Hrsg.

Montali, Marco

Inhaltsverzeichnis

1;Foreword;6
2;Preface;8
3;Acronyms;11
4;Contents;13
5;Introduction;21
5.1;Main Contributions of the Book;23
5.1.1;Specification of Open Declarative Interaction Models;23
5.1.2;Static Verification of Interaction Models;24
5.1.3;Run-Time Verification, Monitoring and Enactment Facilities;24
5.1.4;A-Posteriori Verification and Declarative Process Mining;25
5.2;Organization of the Book;26
5.2.1;Part I: Specification;26
5.2.2;Part II: Static Verification;27
5.2.3;Part III: Run-Time and A-Posteriori Verification;28
5.2.4;Part IV: Conclusion and Future Work;28
5.3;Web Site;28
6;Part I Specification;29
6.1;Declarative Open Interaction Models;30
6.1.1;An Informal Characterization of Interaction Models;30
6.1.1.1;Interaction Abstractions: Activity, Event, Execution Trace;30
6.1.1.2;Characterization of Time;32
6.1.1.3;Compliance;33
6.1.1.4;Flexibility;35
6.1.1.5;Openness;38
6.1.2;Business Process Management;39
6.1.2.1;Modeling Business Processes;41
6.1.2.2;Limits of Procedural Business Process Modeling;42
6.1.3;Service Oriented Computing;44
6.1.3.1;Service Oriented Architecture;44
6.1.3.2;Orchestration and Choreography;45
6.1.3.3;Limits of Procedural Choreography Modeling;48
6.1.4;Multi-Agent Systems;53
6.1.5;Clinical Guidelines;55
6.1.5.1;Basic Medical Knowledge and Clinical Guidelines;56
6.1.5.2;Semi-Openness of Clinical Guidelines;57
6.1.6;Lesson Learnt: Compliance vs. Flexibility;58
6.1.7;Desiderata for a Supporting Framework;60
6.1.7.1;Internal Life Cycle;61
6.1.7.2;Participation to an External Life Cycle;62
6.1.8;The CLIMB Framework;63
6.2;The ConDec Language;65
6.2.1;ConDec in a Nutshell;65
6.2.2;ConDec Models;66
6.2.3;Constraints;67
6.2.3.1;Existence Constraints;67
6.2.3.2;Choice Constraints;68
6.2.3.3;Relation Constraints;69
6.2.3.4;Negation Constraints;72
6.2.3.5;Branching Constraints;74
6.2.4;ConDec at Work;75
6.2.4.1;The Order Management Choreography in Natural Language;76
6.2.4.2;The Order Management Choreography as a Contract;76
6.2.4.3;Identification of Activities;77
6.2.4.4;Elicitation of Business Constraints;78
6.2.4.5;Completing the ConDec Model;81
6.2.5;Usability of ConDec;82
6.2.6;Linear Temporal Logic;85
6.2.6.1;LTL Models;86
6.2.6.2;Syntax of Linear Temporal Logic;86
6.2.6.3;Semantics of Linear Temporal Logic;87
6.2.7;Translating ConDec into Linear Temporal Logic;88
6.2.7.1;The Translation Function;88
6.2.7.2;LTL Entailment as a Compliance Evaluator;89
6.2.7.3;Linear Temporal Logic and Finite ConDec Traces;90
6.3;The CLIMB Rule-Based Language;94
6.3.1;The CLIMB Language in a Nutshell;94
6.3.2;The CLIMB Language;96
6.3.2.1;Event Occurrences and Execution Traces;96
6.3.2.2;Constraint Logic Programming;98
6.3.2.3;Expectations;100
6.3.2.4;Integrity Constraints;102
6.3.2.5;The Static Knowledge Base;107
6.3.2.6;SCIFF-lite and Composite Events;110
6.3.3;CLIMB Declarative Semantics;112
6.3.3.1;Abduction;113
6.3.3.2;Abductive Logic Programming;115
6.3.3.3;Formalizing Interaction Models and Their Executions;116
6.3.3.4;SCIFF-lite Specifications;118
6.3.3.5;CLIMB Abductive Explanations;119
6.3.3.6;On the Formal Definition of Compliance;122
6.3.4;Formal Properties;126
6.3.4.1;Equivalence Modulo Compliance;126
6.3.4.2;Compositionality Modulo Compliance;127
6.3.4.3;Replaceability of Rules;130
6.4;Translating ConDec into CLIMB;132
6.4.1;Translation of a ConDec Model;133
6.4.2;Translation of Events;134
6.4.3;Embedding a Qualitative Characterization of Time into a Quantitative Setting;134
6.4.3.1;Temporal Contiguity;134
6.4.3.2;Compact Execution Traces;136
6.4.4;Translation of ConDec Constraints;138
6.4.4.1;Translation of Existence Constraints;138
6.4.4.2;Translation of Choice Constraints;140
6.4.4.3;Translation of Relation and Negation Constraints;142
6.4.5;Dealing with Branching ConDec Constraints;145
6.4.6;Translation of a ConDec Choreography;147
6.4.7;Equivalence of ConDec Constraints;147
6.4.8;Soundness of the Translation;149
6.4.8.1;Trace Mapping;150
6.4.8.2;Behavioral Equivalence;151
6.4.8.3;Soundness;151
6.4.8.4;On the Expressiveness of SCIFF;154
6.5;Extending ConDec;156
6.5.1;Metric Constraints;156
6.5.1.1;Temporal Contiguity in a Quantitative Setting;157
6.5.1.2;Quantitative Formalization of Chain Constraints;158
6.5.1.3;Init Constraint;159
6.5.1.4;Extending ConDec with Quantitative Temporal Constraints;159
6.5.2;Data Aware Aspects;162
6.5.2.1;Examples of Data Aware Business Constraints;162
6.5.2.2;The MXML Meta Model;164
6.5.2.3;The Life Cycle of Non Atomic Activities in ConDec$^++$;165
6.5.3;Modeling Data in ConDec ++;166
6.5.3.1;Representing Non Atomic Activities and Data;166
6.5.3.2;Modeling Data Aware Conditions;167
6.5.3.3;Modeling the Submit&Review Process Fragment;171
6.5.4;Formalizing Data Aware Aspects in CLIMB;172
6.5.4.1;Formalizing Data and Data Aware Conditions;172
6.5.4.2;Formalizing the Effect of Roles;173
6.5.4.3;Formalizing the Activity Life Cycle;176
6.6;Related Work and Summary;179
6.6.1;Related Work;179
6.6.1.1;Business Process Management;179
6.6.1.2;Clinical Guidelines;182
6.6.1.3;Service Oriented Computing;185
6.6.1.4;Multi-Agent Systems;186
6.6.2;Summary of the Part;188
7;Part II Static Verification;190
7.1;Static Verification of Declarative Open Interaction Models;191
7.1.1;Desiderata for Static Verification Technologies;191
7.1.2;Verification of a Single Model vs. a Composition of Models;193
7.1.3;Static Verification of Properties;194
7.1.3.1;Existential vs. Universal Properties;194
7.1.3.2;General vs. Particular Properties;195
7.1.3.3;On the Safety-Liveness Classification;196
7.1.3.4;A ConDec Example;198
7.1.4;A-Priori Compliance Verification;200
7.1.5;Composing ConDec Models;201
7.1.5.1;Compatibility between Local Models;202
7.1.5.2;Augmenting ConDec with Roles and Participants;204
7.1.5.3;From Openness to Semi-Openness;206
7.1.6;Conformance with a Choreography;210
7.2;Proof Procedures;214
7.2.1;The SCIFF Proof Procedure;215
7.2.1.1;Fulfilled, Violated and Pending Expectations;215
7.2.1.2;Data Structures and Proof Tree;216
7.2.1.3;Transitions;218
7.2.2;Formal Properties of the SCIFF Proof Procedure;227
7.2.2.1;Soundness;227
7.2.2.2;Completeness;228
7.2.2.3;Termination;229
7.2.2.4;ConDec and Termination of the SCIFF Proof Procedure;231
7.2.3;The g-SCIFF Proof Procedure;231
7.2.3.1;Generation of Intensional Traces;232
7.2.3.2;Data Structures Revisited;233
7.2.3.3;Transitions Revisited;234
7.2.3.4;Linking the Proof Procedures;235
7.2.4;Formal Properties of the g-SCIFF Proof Procedure;236
7.2.4.1;Soundness;236
7.2.4.2;Completeness Modulo Trace Generation;236
7.2.4.3;Termination;238
7.2.5;Implementation of the Proof Procedures;240
7.3;Static Verification of ConDec Models with g-SCIFF;241
7.3.1;Existential and Universal Entailment in CLIMB;241
7.3.1.1;Specification of Properties with ConDec;241
7.3.1.2;Formalizing Existential and Universal Entailment;243
7.3.2;Verification of Existential Properties with g-SCIFF;244
7.3.2.1;Conflict Detection with g-SCIFF;245
7.3.2.2;Existential Entailment with g-SCIFF;245
7.3.3;Verification of Universal Properties with g-SCIFF;246
7.3.3.1;Complementation of Integrity Constraints;246
7.3.3.2;Reducing Universal to Existential Entailment;248
7.3.4;ConDec Loops and Termination of g-SCIFF;251
7.3.4.1;Constraints Reformulation;252
7.3.4.2;Looping ConDec Models;253
7.3.5;A Preprocessing Procedure;258
7.4;Experimental Evaluation;262
7.4.1;Verification Procedure with g-SCIFF;262
7.4.2;Scalability of the g-SCIFF Proof Procedure;264
7.4.2.1;The Branching Responses Benchmark;264
7.4.2.2;The Alternate Responses Benchmark;266
7.4.2.3;The Chain Responses Benchmark;269
7.4.3;Static Verification of ConDec Models as Model Checking;272
7.4.3.1;Existential and Universal Entailment of ConDec Properties in LTL;272
7.4.3.2;ConDec Properties Verification as Satisfiability and Validity Problems;273
7.4.3.3;Model Checking;275
7.4.3.4;Reduction of Validity and Satisfiability to Model Checking;277
7.4.3.5;Verification Procedure by Model Checking;279
7.4.4;Comparative Evaluation;280
7.4.4.1;The Order&Payment Benchmarks;280
7.4.4.2;Discussion;281
7.5;Related Work and Summary;287
7.5.1;Related Work;287
7.5.1.1;Verification of Properties;287
7.5.1.2;A-Priori Compliance Verification;291
7.5.1.3;Model Composition;293
7.5.1.4;Interoperability and Choreography Conformance;294
7.5.2;Summary of the Part;295
8;Part III Run-Time and A-Posteriori Verification;297
8.1;Run-Time Verification;298
8.1.1;The Run-Time Verification Task;299
8.1.2;SCIFF-Based Run-Time Verification;300
8.1.2.1;Reactive Behavior of the SCIFF Proof Procedure;301
8.1.2.2;Open Derivations;301
8.1.2.3;Semi-Open Reasoning;304
8.1.3;The SOCS-SI Tool;307
8.1.4;Speculative Run-Time Verification;309
8.1.4.1;The Need for Speculative Reasoning;309
8.1.4.2;Speculative Verification with the g-SCIFF Proof Procedure;310
8.1.4.3;Interleaving the Proof Procedures;312
8.2;Monitoring and Enactment with Reactive Event Calculus;314
8.2.1;Monitoring Issues and SCIFF;314
8.2.2;Event Calculus;316
8.2.2.1;The Event Calculus Ontology;317
8.2.2.2;Domain-Dependent vs. Domain-Independent Axioms;318
8.2.2.3;Reasoning with Event Calculus;319
8.2.3;The Reactive Event Calculus;321
8.2.3.1;Axiomatization of the Reactive Event Calculus;321
8.2.3.2;Monitoring an Event Calculus Specification with the SCIFF Proof Procedure;324
8.2.4;REC Illustrated: A Personnel Monitoring Facility;325
8.2.4.1;Formalizing the Personnel Monitoring Facility in REC;325
8.2.4.2;Monitoring a Concrete Instance;327
8.2.4.3;The Irrevocability Issue;328
8.2.5;Formal Properties of REC;329
8.2.5.1;Soundness, Completeness, Termination;329
8.2.5.2;Irrevocability of REC;330
8.2.6;Monitoring Optional ConDec Constraints with REC;333
8.2.6.1;Representing ConDec Optional Constraints in the Event Calculus;334
8.2.6.2;Identification and Reification of Violations;337
8.2.6.3;Compensating Violations;340
8.2.6.4;Monitoring Example;341
8.2.7;Enactment of ConDec Models;344
8.2.7.1;Showing Temporarily Violated Constraints;345
8.2.7.2;Blocking Non Executable Activities;345
8.2.7.3;Termination of the Execution;348
8.2.8;jREC: Embedding REC Inside a JAVA-Based Tool;349
8.3;Declarative Process Mining;351
8.3.1;Declarative Process Mining with ProM, SCIFF Checker and DecMiner;353
8.3.2;The SCIFF Checker ProM Plug-in;354
8.3.2.1;CLIMB Textual Business Constraints;355
8.3.2.2;A Methodology for Building Rules;356
8.3.2.3;Specification of Conditions;357
8.3.2.4;Trace Analysis with Logic Programming;358
8.3.2.5;Embedding SCIFF Checker in ProM;359
8.3.3;Case Studies;361
8.3.3.1;The Think3 Case Study;362
8.3.3.2;Conformance Verification of a Cervical Cancer Screening Process;365
8.3.3.3;Quality Assessment in Large Wastewater Treatment Plans;366
8.3.4;The DecMiner ProM Plug-in;369
8.3.4.1;Inductive Logic Programming for Declarative Process Discovery;369
8.3.4.2;Embedding DecMiner into the ProM Framework;370
8.3.5;The Checking–Discovery Cycle;372
8.4;Related Work and Summary;374
8.4.1;Related Work;374
8.4.1.1;Run-Time Verification and Monitoring;374
8.4.1.2;Enactment;379
8.4.1.3;Process Mining;380
8.4.2;Summary of the Part;382
9;Part IV Conclusion and Future Work;384
9.1;Conclusion and Future Work;385
9.1.1;Conclusion;385
9.1.2;Future Work;386
9.1.2.1;Termination of Static Verification and ConDec Extensibility;386
9.1.2.2;Reactive Event Calculus and Operational Support;387
9.1.2.3;Integration of Regulative and Constitutive Rules;387
9.1.2.4;Development of an Editor and Enactment Prototype;388
9.1.2.5;Service Contracting and Discovery in the Semantic Web;389
9.1.2.6;Integration of Declarative and Procedural Models;389
10;References;390
11;Index;408