Mobucon

Monitoring Business Constraints with Linear Temporal Logic

Today’s information systems record real-time information about business processes. This enables the monitoring of business constraints at runtime. In [1, 2], the authors introduce a novel runtime verification framework based on linear temporal logic. The framework continuously verifies compliance with respect to a predefined constraint model. Moreover, it is able to provide meaningful diagnostics even after a constraint is violated. This is important as in reality people and organizations will deviate and in many situations it is not desirable or even impossible to circumvent constraint violations.

The proposed framework has been implemented as an Operational Support provider in the process mining tool ProM: Mobucon LTL.

Mobucon LTL

The Mobucon (MOnitoring BUsiness CONstraints) LTL provider is part of ProM 6.1. Mobucon LTL is an Operational Support provider that allows the user to monitor a case w. r. t. a set of business constraints. These constraints are Declare constraints and their formal semantics is expressed by using LTL. The Mobucon Client allows the user to handle several cases at the same time and to show the monitor results in an easy and intuitive way. The Mobucon Client can be downloaded here.

The functionality of the provider and of the client can best be described by an example.

Example use of the framework

To use Mobucon LTL, first the Operational Support Service 2.0 in ProM must be started. After that, the Mobucon LTL provider can be started using the Operational Support Service as input. Now, Mobucon LTL is listening on the port specified in the Operational support Service (1202 by default).

Configuration file for the Mobucon Client

At this point, the Mobucon Client can be started. When the client is started an XML file for configuration must be specified as parameter of the java application. An example configuration file can be downloaded here. The tags to specify in the configuration file are:

• host (string): host where the client will be listening for online streams from external cases;
• port (integer): port on which the client will be listening;

Pressing Start, the Mobucon Client starts listening on the port specified in the configuration file.

Messages format

A case running on an external system (like Declare) can communicate with the Mobucon Client via socket (by using host and port specified in the configuration file). When a Declare process is executed through the Declare Framework, the Declare Framework automatically opens a socket to communicate with a possible instance of the Mobucon Client via text stream. Any external system can, however, communicate with the client by using the right text stream format. A file including a possible text stream can be downloaded here. The first thing that the system must send is an XML file (see the example stream) including additional configuration parameters and the reference Declare model, i.e., the model w.r.t. which the case must be monitored. In the following we explain the meaning of the tags to specify in the configuration file:

• id (string): it represents an identifier of the reference Declare model sent;
• model (complex): it is the reference Declare model;
• constraints (complex): set of constraint elements corresponding to the constraints included in the reference Declare model;
  • constraint (complex): it gives information about a constraint included in the reference Declare model;
    • id (string): identifier of this constraint. This identifier must correspond to an identifier of one of the constraints included in the reference Declare model;
    • weight (integer): constraints with a higher weight have more influence (when violated) on the overall value of the health of the case;
• timeWindow (integer): the last timeWindow events will be considered to evaluate the health of each case (considering the older ones as obsolete);

After that, events can be sent through messages encoded by using the following format:
<?xml version=”1.0″?> <Entry>
<ProcessID>put here the process ID of the case</ProcessID>
<ProcessInstanceID>put here the process instance ID of the case</ProcessInstanceID>
<ModelID>put here the identifier of one of the Declare models specified in the configuration file w. r. t. which the
case must be monitored</ModelID>
<WorkflowModelElement> put here the name of the event associated to this message</WorkflowModelElement>
<Timestamp>put here the timestamp (in milliseconds) of the event associated to this message</Timestamp>
<EventType>put here the type of the event associated to this message</EventType></Entry>

When the Mobucon Client receives events from external cases, it forwards the requests to the Mobucon LTL provider. The provider sends back information for each specific case about the state of each constraint included in the corresponding reference Declare model and about the health of the case.

The following picture illustrates the Mobucon Client GUI:

On the left side of the GUI, the list of the monitored cases is shown.

A case id is labelled by “WARNING”, if the health of the case (which is a number between 0 and 1) is lower than a given threshold (the default threshold is 1).

It is possible to filter the case id list by using the options:

• show All: to list all the case ids,
• show warnings: to list all the case ids labelled by “WARNING”, and
• search ID: to search a specific case id (specified in the corresponding text field).

On the right side of the GUI, it is possible to read the reference Declare model used by the selected case (in the picture above the reference model for the selected case Westergaard is investment). The tabbed frame on the same side includes the following views:

1. Monitor,
2. Diagnostics.

In the following, these views are described in detail.

The monitor

On the right side of the GUI, the monitor tab includes the list of the monitored Declare constraints. These constraints compose the reference model for the selected case.

When a constraint is in a possibly violated state, it means that the case is currently not compliant with the constraint, but it is possible to satisfy it by generating some event. For example, in the picture above, when money occurs (timestamp 07/29/2011 20:13:26:53), the constraint alternate response is possibly violated because it is waiting for the event bonds or stocks. When stocks occurs (timestamp 07/29/2011 20:13:31:53), the constraint becomes possibly satisfied. When a constraint is in a possibly satisfied state, it means that the case is currently compliant with the constraint, but it is possible to violate it in the future. On the other hand, when a constraint is in a satisfied state, it means that the case is permanently compliant with the constraint. For example, in the picture above, when stocks occurs (timestamp 07/29/2011 20:13:31:53), the constraint precedence becomes satisfied because the case is compliant with the constraint and it is no longer possible to violate it. When a constraint is in a violated state, it means that the case is permanently not compliant with the constraint. For example, in the picture above, when money occurs (timestamp 07/29/2011 20:13:51:54), the constraint alternate response is possibly violated. When money occurs again (timestamp 07/29/2011 20:14:01:55), the constraint becomes violated. Note that in correspondence of this violation the health decreases.

In fact, to implement the monitor, a mechanism for recovery from failures has been implemented. In particular, a constraint, after being violated, is reset to the initial state. In this way, it is possible to count the violations and evaluate the health of a case over the time. The health is evaluated within the timeWindow specified in the configuration file (the health is evaluated considering only the last timeWindow events), so that old behaviours are discarded in the health evaluation and the value of the health can increase over the time. In particular, the Mobucon LTL provider uses the formula:

where w_i is the weight and v_i is the number of violation for the i^th constraint; ev is the number of considered events (corresponding to timeWindow)

Mobucon LTL can also detect non local violations generated by the interplay of constraints, i.e., violations which cannot be attributed to a single constraint in isolation, but result from combinations of conflicting constraints. In a running case, a set of constraints is conflicting if, for any possible continuation of the instance, at least one of such constraints will be eventually violated. In the following picture, an example of conflicting constraints is shown. In particular, event low_risk (timestamp 07/29/2011 20:18:08:904) leads to a non local violation caused by the interplay of the constraints not co-existence and response. The conflict is due to the fact that the first forbids and the other requires the presence of event bonds. Also in this case (in correspondence of the conflict), the health decreases. However, whereas the weight of a non local violation is always 1 (the minimum possible value), a violation of the constraint alternate response influences the health more.

Diagnostics

The diagnostics tab includes diagnostics for each violation occurred for the selected case. For example, when the non local violation is detected in the Westergaard case in the picture above (timestamp 07/29/2011 20:18:08:904), in the diagnostics tab it is possible to read:

• the observed event, i.e., low_risk, and
• the expected behaviour for the corresponding reference model (investment), i.e., money, stocks, or high_yield

@incollection{colored_automata,
Author = {F.M. Maggi and M. Montali and M. Westergaard and W.M.P. van der Aalst},
Title = {{Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata}},
Year = {2011},
Publisher = {Springer-Verlag},
Series = {LNCS},
Booktitle = {{Proc. of BPM}},
}

@incollection{5values,
Author = {F.M. Maggi and M. Westergaard and M. Montali and W.M.P. van der Aalst},
Title = {{Runtime Verification of LTL-Based Declarative Process Models}},
Year = {2011},
Publisher = {Springer-Verlag},
Series = {LNCS},
Booktitle = {{Proc. of RV}},
}