Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben

2010 | Buch

Introduction Kapitel lesen Erstes Kapitel lesen

Specification and Verification of Declarative Open Interaction Models

A Logic-Based Approach

verfasst von: Marco Montali

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Business Information Processing

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

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.

Inhaltsverzeichnis

Frontmatter

Introduction

Introduction
Abstract
The advent of distributed and heterogeneous systems has laid the foundation for the birth of new architectural paradigms, which enable to attack the complexity of the targeted domain by splitting it up into several interacting components. In the field of software engineering, the difference between these paradigms and the classical centralized and monolithic ones has been identified since 1975, when DeRemer and Kron conied the two terms of programmingin- the-small vs programming-in-the-large [91].
Marco Montali

Part I Specification

Frontmatter
Declarative Open Interaction Models
Abstract
In this Chapter, we provide an informal yet precise characterization of open declarative interaction models along different dimensions, namely modeling abstractions, time, compliance, degree of flexibility and degree of openness. We then give an overview of several application domains in which interaction plays a central role: Business Process Management (BPM), Service Oriented Computing (SOC), Clinical Guidelines (CGs) and Multi-Agent Systems (MASs). We discuss the drawbacks of procedural and closed approaches when dealing with such settings, motivating why we claim that they should be complemented with an open and declarative perspective. Finally, we describe a generic framework for managing the life cycle of open declarative interaction models, spanning from their design to their execution, monitoring and a-posteriori verification, and propose how to fill its building blocks.
Marco Montali
The ConDec Language
Abstract
ConDec is a graphical language proposed by Pesic and van der Aalst for the declarative and open modeling of Business Processes (BPs)[192, 191]. It fits with complex, unpredictable processes, where a good balance between support and flexibility must be found. Two variants of ConDec have been proposed for specifying service flows [242], as well as for dealing with Clinical Guidelines (CGs) [181].
In this Chapter, we present a critical overview of the language and recall its constructs. We show its application on a representative case study, and discuss its style of modeling in the light of the cognitive dimensions framework [122]. We then introduce the framework of propositional Linear Temporal Logic (LTL) [99], summarizing how it has been exploited in [192, 191, 173] to provide the first formalization of the ConDec constructs.
Marco Montali
The CLIMB Rule-Based Language
Abstract
The CLIMB (Computational Logic for the verIfication and Modeling of Business constraints) language is a declarative rule-based language for the specification of interaction models. This chapter describes syntax and features of the language, showing how it can suitably deal with static as well as dynamic aspects of EBSs; the declarative semantics of the language is presented, providing a formal characterization of compliance; finally, some interesting properties, such as compositionality of CLIMB specifications, are investigated.
The CLIMB language is a first-order logic-based language; quantification is left implicit in the language, in order to facilitate readability and usability.We will briefly discuss in an informal way and by means of examples how variables are quantified. For an exhaustive description concerning the quantification of variables and the restrictions imposed on the language the interested reader may refer to [8, 58].
In the remainder of the book, we will assume that the reader is familiar with First Order Logic (FOL), Logic Programming (LP) and Prolog. A good introduction to LP is the book by Lloyd [154]; good introductions to Prolog are the books by Sterling and Shapiro [227] and by Bratko [49].
Marco Montali
Translating ConDec into CLIMB
Abstract
In Chaps. 3 and 4, we have discussed two different approaches for the specification of interaction models: CLIMB and ConDec, together with their abductive and LTL-based semantics. On the one hand, the two approaches have complementary scopes and objectives: while ConDec adopts an intuitive graphical notation and pays particular attention to the usability by non-IT savvy, CLIMB is based on a rigorous, rule-based language, which gives a formal account to compliance, and is therefore apt to verification. On the other hand, the two approaches share the same, underlying paradigm: they both rely on the notion of (business) constraint as the fundamental abstraction to specify interaction following an open and declarative style of modeling. This chapter exploits these similarities to provide a complete formalization of ConDec in terms of CLIMB. Thus, it lays the foundation for the verification of ConDec models along their entire lifecycle, which will be matter of the next parts of this book.
Marco Montali
Extending ConDec
Abstract
In this chapter, we investigate how the first-order nature of the CLIMB language can be exploited to extend the expressiveness of ConDec along different dimensions, towards the support of:
  • quantitative (metric) temporal constraints;
  • activity data and data aware conditions;
  • a non atomic model of activities.
We call the extended language ConDec++. ConDec++ reconciles ConDec with MXML, a well known meta model proposed by van Dongen and van der Aalst for standardizing the representation and storing of event logs [253].
Marco Montali
Related Work and Summary
Abstract
Related work concerning the specification languages for interaction models is presented. Then, the major contributions of this part of the book are briefly summarized.
Marco Montali

Part II Static Verification

Frontmatter
Static Verification of Declarative Open Interaction Models
Abstract
Static verification offers design-time support for guaranteeing that an interaction model will meet, during the execution, certain desired properties, enabling the early identification of errors and undesired situations. It is therefore exploited a-priori, before the execution. The positive outcome of static verification can be used as a proof attesting the trustworthiness and reliability of the developed model.
This chapter provides an introductory characterization of the static verification of declarative open interaction models, specified using the ConDec notation. We discuss the desiderata that a static verification technology must accomplish, and then focus on two specific problems:
  • static verification of properties, carried out on a single model;
  • static verification of a composition of local models, and conformance checking of a set of local models with a global (choreographic) model.
Marco Montali
Proof Procedures
Abstract
This chapter introduces two abductive proof procedures for reasoning upon SCIFF (and therefore also CLIMB) specifications: sciff and g-sciff.
The sciff proof procedure checks whether an execution trace complies with a SCIFF specification, providing a concrete operational framework for:
  • generating positive and negative expectations starting from a trace and a specification;
  • checking whether the generated expectations are fulfilled by the actual occurring events (hypotheses confirmation step).
sciff is able reason upon a complete execution trace, or upon a growing trace, by dynamically acquiring and processing occurring events as they happen.
Marco Montali
Static Verification of ConDec Models with g-SCIFF
Abstract
This chapter is devoted to discuss how the g-sciff proof procedure can be adopted for the static verification of ConDec models. The scalability of the approach will be investigated in the next chapter.
The first part of the chapter demonstrates how existential and universal properties, as defined in Sect. 8.3.1, can be expressed in CLIMB and verified with g-sciff. Thanks to this possibility, g-sciff can be exploited to deal with all the static verification tasks introduced in Chap. 8:
  • conflict detection;
  • discovery of dead activities;
  • compliance verification;
  • a-priori
  • checking the executability of composite models;
  • verification of conformance to a choreography.
The second part of the chapter is instead focused on termination issues; as sketched in Sect. 9.4.3, the termination of g-sciff cannot be generally guaranteed when reasoning upon CLIMB specifications, and therefore an ad-hoc solution for ConDec must be provided.
Marco Montali
Experimental Evaluation
Abstract
In Chap. 10, it has been shown how g-sciff can deal with the static verification of ConDec models. In order to assess the usability of the proposed approach, it is necessary to evaluate its performance and scalability, comparing it with other verification techniques. This chapter aims at showing that g-sciff is an effective technology when it comes to the static verification of ConDec models. An extensive experimental evaluation is presented, stressing g-sciff and emphasizing its performance results in both favorable and unfavorable cases. After having discussed how the static verification task can be also interpreted as a model checking problem, we compare g-sciff with state-of-the-art explicit and symbolic model checkers, providing an empirical discussion of their benefits and drawbacks.
The presented benchmarks will stress the scalability and performance of the verification techniques along two significant dimensions:
  • size of the model (number of mandatory constraints contained in the model);
  • cardinality on activities (presence of existence constraints requiring a minimum number of executions of some activity in the model).
All experiments have been performed on a MacBook Intel CoreDuo 2 GHz machine, and considering the SICStus-based implementation of g-sciff.
Marco Montali
Related Work and Summary
Abstract
Related work concerning the static verification of interaction models is presented. Then, the major contributions of this part of the book are briefly summarized.
Marco Montali

Part III Run-Time and A-Posteriori Verification

Frontmatter
Run-Time Verification
Abstract
Static verification techniques are useful to assess the correctness, safety and consistency of the designed models. However, they suppose that all the business constraints of the model are completely accessible, i.e., they assume that the model is a white box.
Marco Montali
Monitoring and Enactment with Reactive Event Calculus
Abstract
In Chap. 13, we have shown how sciff can be used to perform run-time verification of a running execution with respect to some ConDec model. When providing execution support, it is not only important to offer compliance verification facilities, but also to give a constant feedback to the interacting entities, keeping them informed about the evolving state of affairs and reporting undesired situations. This task is called monitoring and is illustrated in Fig. 14.1. Monitoring aims at dynamically observing the behavior of interacting entities, tracking its impact on the monitored specification and capturing violations without terminating the computation; the detection of a violation could lead to generate a corresponding alarm, to warn the system administrator or even to start a special course of interaction, aimed at fixing the violation.
In this chapter, we show how a reactive form of the Event Calculus (EC) [146] can be encoded as a SCIFF-lite program, enabling the possibility of
  • monitoring ConDec optional constraints;
  • introducing compensation constructs in ConDec, modeling business constraints that express which countermeasures should be taken when an optional constraint is violated, and that are enforced only in such an exceptional situation;
  • tracking the evolution of constraints’ states as events occur.
The latter topic provides the basis for supporting the enactment of ConDec models, which is discussed in the last part of the chapter.
Marco Montali
Declarative Process Mining
Abstract
When Event-Based Systems (EBSs) are executed inside a company, it is usually the case that all relevant event occurrences are collected and stored inside an information system. All the modern Business Process Management (BPM) systems used in the industry provide logging facilities.
Marco Montali
Related Work and Summary
Abstract
Related work concerning the enactment, run-time verification, monitoring and mining of interaction models is presented. Then, the major contributions of this part of the book are briefly summarized.
Marco Montali

Part IV Conclusion and Future Work

Frontmatter
Conclusion and Future Work
Conclusion
We have put forwards significant evidence to support that declarativeness and openness are needed to deal with a plethora of systems, composed by several autonomous entities which collaborate and interact to the aim of achieving complex goals, impossible to be accomplished on their own. We have considered four challenging settings, namely Business Process Management, Clinical Guidelines, Service Oriented and Multi-Agent Systems. We have argued that all these application domains require a suitable balance between compliance and flexibility, a goal that can be achieved only by complementing closed and procedural interaction models with an open, declarative counterpart. The Computational Logic-based CLIMB framework has been proposed to cover the entire life cycle of open declarative interaction models, supporting their specification and verification.
Marco Montali
Backmatter
Metadaten
Titel
Specification and Verification of Declarative Open Interaction Models
verfasst von
Marco Montali
Copyright-Jahr
2010
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-14538-4
Print ISBN
978-3-642-14537-7
DOI
https://doi.org/10.1007/978-3-642-14538-4

Premium Partner

    Bildnachweise