Monitoring and Enactment with Reactive Event Calculus

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.