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

Foreword

Preface

Acronyms

Contents

Introduction

Main Contributions of the Book

Specification of Open Declarative Interaction Models

Static Verification of Interaction Models

Run-Time Verification, Monitoring and Enactment Facilities

A-Posteriori Verification and Declarative Process Mining

Organization of the Book

Part I: Specification

Part II: Static Verification

Part III: Run-Time and A-Posteriori Verification

Part IV: Conclusion and Future Work

Web Site

Part I Specification

Declarative Open Interaction Models

An Informal Characterization of Interaction Models

Interaction Abstractions: Activity, Event, Execution Trace

Characterization of Time

Compliance

Flexibility

Openness

Business Process Management

Modeling Business Processes

Limits of Procedural Business Process Modeling

Service Oriented Computing

Service Oriented Architecture

Orchestration and Choreography

Limits of Procedural Choreography Modeling

Multi-Agent Systems

Clinical Guidelines

Basic Medical Knowledge and Clinical Guidelines

Semi-Openness of Clinical Guidelines

Lesson Learnt: Compliance vs. Flexibility

Desiderata for a Supporting Framework

Internal Life Cycle

Participation to an External Life Cycle

The CLIMB Framework

The ConDec Language

ConDec in a Nutshell

ConDec Models

Constraints

Existence Constraints

Choice Constraints

Relation Constraints

Negation Constraints

Branching Constraints

ConDec at Work

The Order Management Choreography in Natural Language

The Order Management Choreography as a Contract

Identification of Activities

Elicitation of Business Constraints

Completing the ConDec Model

Usability of ConDec

Linear Temporal Logic

LTL Models

Syntax of Linear Temporal Logic

Semantics of Linear Temporal Logic

Translating ConDec into Linear Temporal Logic

The Translation Function

LTL Entailment as a Compliance Evaluator

Linear Temporal Logic and Finite ConDec Traces

The CLIMB Rule-Based Language

The CLIMB Language in a Nutshell

The CLIMB Language

Event Occurrences and Execution Traces

Constraint Logic Programming

Expectations

Integrity Constraints

The Static Knowledge Base

SCIFF-lite and Composite Events

CLIMB Declarative Semantics

Abduction

Abductive Logic Programming

Formalizing Interaction Models and Their Executions

SCIFF-lite Specifications

CLIMB Abductive Explanations

On the Formal Definition of Compliance

Formal Properties

Equivalence Modulo Compliance

Compositionality Modulo Compliance

Replaceability of Rules

Translating ConDec into CLIMB

Translation of a ConDec Model

Translation of Events

Embedding a Qualitative Characterization of Time into a Quantitative Setting

Temporal Contiguity

Compact Execution Traces

Translation of ConDec Constraints

Translation of Existence Constraints

Translation of Choice Constraints

Translation of Relation and Negation Constraints

Dealing with Branching ConDec Constraints

Translation of a ConDec Choreography

Equivalence of ConDec Constraints

Soundness of the Translation

Trace Mapping

Behavioral Equivalence

Soundness

On the Expressiveness of SCIFF

Extending ConDec

Metric Constraints

Temporal Contiguity in a Quantitative Setting

Quantitative Formalization of Chain Constraints

Init Constraint

Extending ConDec with Quantitative Temporal Constraints

Data Aware Aspects

Examples of Data Aware Business Constraints

The MXML Meta Model

The Life Cycle of Non Atomic Activities in ConDec$^++$

Modeling Data in ConDec ++

Representing Non Atomic Activities and Data

Modeling Data Aware Conditions

Modeling the Submit&Review Process Fragment

Formalizing Data Aware Aspects in CLIMB

Formalizing Data and Data Aware Conditions

Formalizing the Effect of Roles

Formalizing the Activity Life Cycle

Related Work and Summary

Related Work

Business Process Management

Clinical Guidelines

Service Oriented Computing

Multi-Agent Systems

Summary of the Part

Part II Static Verification

Static Verification of Declarative Open Interaction Models

Desiderata for Static Verification Technologies

Verification of a Single Model vs. a Composition of Models

Static Verification of Properties

Existential vs. Universal Properties

General vs. Particular Properties

On the Safety-Liveness Classification

A ConDec Example

A-Priori Compliance Verification

Composing ConDec Models

Compatibility between Local Models

Augmenting ConDec with Roles and Participants

From Openness to Semi-Openness

Conformance with a Choreography

Proof Procedures

The SCIFF Proof Procedure

Fulfilled, Violated and Pending Expectations

Data Structures and Proof Tree

Transitions

Formal Properties of the SCIFF Proof Procedure

Soundness

Completeness

Termination

ConDec and Termination of the SCIFF Proof Procedure

The g-SCIFF Proof Procedure

Generation of Intensional Traces

Data Structures Revisited

Transitions Revisited

Linking the Proof Procedures

Formal Properties of the g-SCIFF Proof Procedure

Soundness

Completeness Modulo Trace Generation

Termination

Implementation of the Proof Procedures

Static Verification of ConDec Models with g-SCIFF

Existential and Universal Entailment in CLIMB

Specification of Properties with ConDec

Formalizing Existential and Universal Entailment

Verification of Existential Properties with g-SCIFF

Conflict Detection with g-SCIFF

Existential Entailment with g-SCIFF

Verification of Universal Properties with g-SCIFF

Complementation of Integrity Constraints

Reducing Universal to Existential Entailment

ConDec Loops and Termination of g-SCIFF

Constraints Reformulation

Looping ConDec Models

A Preprocessing Procedure

Experimental Evaluation

Verification Procedure with g-SCIFF

Scalability of the g-SCIFF Proof Procedure

The Branching Responses Benchmark

The Alternate Responses Benchmark

The Chain Responses Benchmark

Static Verification of ConDec Models as Model Checking

Existential and Universal Entailment of ConDec Properties in LTL

ConDec Properties Verification as Satisfiability and Validity Problems

Model Checking

Reduction of Validity and Satisfiability to Model Checking

Verification Procedure by Model Checking

Comparative Evaluation

The Order&Payment Benchmarks

Discussion

Related Work and Summary

Related Work

Verification of Properties

A-Priori Compliance Verification

Model Composition

Interoperability and Choreography Conformance

Summary of the Part

Part III Run-Time and A-Posteriori Verification

Run-Time Verification

The Run-Time Verification Task

SCIFF-Based Run-Time Verification

Reactive Behavior of the SCIFF Proof Procedure

Open Derivations

Semi-Open Reasoning

The SOCS-SI Tool

Speculative Run-Time Verification

The Need for Speculative Reasoning

Speculative Verification with the g-SCIFF Proof Procedure

Interleaving the Proof Procedures

Monitoring and Enactment with Reactive Event Calculus

Monitoring Issues and SCIFF

Event Calculus

The Event Calculus Ontology

Domain-Dependent vs. Domain-Independent Axioms

Reasoning with Event Calculus

The Reactive Event Calculus

Axiomatization of the Reactive Event Calculus

Monitoring an Event Calculus Specification with the SCIFF Proof Procedure

REC Illustrated: A Personnel Monitoring Facility

Formalizing the Personnel Monitoring Facility in REC

Monitoring a Concrete Instance

The Irrevocability Issue

Formal Properties of REC

Soundness, Completeness, Termination

Irrevocability of REC

Monitoring Optional ConDec Constraints with REC

Representing ConDec Optional Constraints in the Event Calculus

Identification and Reification of Violations

Compensating Violations

Monitoring Example

Enactment of ConDec Models

Showing Temporarily Violated Constraints

Blocking Non Executable Activities

Termination of the Execution

jREC: Embedding REC Inside a JAVA-Based Tool

Declarative Process Mining

Declarative Process Mining with ProM, SCIFF Checker and DecMiner

The SCIFF Checker ProM Plug-in

CLIMB Textual Business Constraints

A Methodology for Building Rules

Specification of Conditions

Trace Analysis with Logic Programming

Embedding SCIFF Checker in ProM

Case Studies

The Think3 Case Study

Conformance Verification of a Cervical Cancer Screening Process

Quality Assessment in Large Wastewater Treatment Plans

The DecMiner ProM Plug-in

Inductive Logic Programming for Declarative Process Discovery

Embedding DecMiner into the ProM Framework

The Checking–Discovery Cycle

Related Work and Summary

Related Work

Run-Time Verification and Monitoring

Enactment

Process Mining

Summary of the Part

Part IV Conclusion and Future Work

Conclusion and Future Work

Conclusion

Future Work

Termination of Static Verification and ConDec Extensibility

Reactive Event Calculus and Operational Support

Integration of Regulative and Constitutive Rules

Development of an Editor and Enactment Prototype

Service Contracting and Discovery in the Semantic Web

Integration of Declarative and Procedural Models

References

Index