jREC is a JAVA+Prolog-based tool for reasoning upon the dynamics of an event-based system with respect to an Event Calculus specification. More specifically, jREC dynamically acquires the event occurrences characterizing a running execution of the system and monitors their effects by updating the evolution of the corresponding fluents (i.e. properties varying over time) according to an Event Calculus theory. jREC is based on a lightweight axiomatization of Chittaro and Montanari's Cached Event Calculus (see the paper Efficient Temporal Reasoning in the Cached Event Calculus), which captures a form of proactive reasoning where the current fluents' maximal validity intervals are cached and then updated/revised as new event occurrences get to be known. In this way, the reasoner avoids restarting from scratch every time a new event happens (which is the case of classical EC deductive reasoners), thus tracking the system's execution efficiently.
jREC is composed of two subprojects: jREC (core) - the reasoner, jREC UI - a user interface that graphically depicts the fluents' evolution. A tester for jREC is also available, and two other tools are based on it: MOBUCON and ComMon.
The Event Calculus ontology (i.e. the predicates supported by the calculus and that can be defined and/or used in the domain-dependent theory) of jRec contains the following predicates:
initially(F)- fluent F holds in the initial state;
initiates(E,F,T)- event E is able to make F true at time T;
terminates(E,F,T)- event E is able to make F false at time T;
happens(E,T)- event E occurs at time T (also used ground inside the description of an execution trace);
holds_at(F,T)- fluent F is true at time T (usable only in the body of a clause as a tester);
status/2to model multi-valued fluents, where
Fhas current value
S. A simple domain-dependent theory can be downloaded here.
The reasoner interface
RecEngine contains the following methods:
public boolean setModel(String model) throws Exception- sets a domain-dependent theory (embedded in a string).
public FluentsModel start() throws Exception- starts the reasoner; the returned fluents' model contains all the fluents that hold initially.
public FluentsModel evaluateTrace(RecTrace trace) throws Exception- evaluates a chunk of event occurrences (i.e. a partial or complete trace) extending/revising the previously computed result and returning the fresh one; if the trace is closed, then the reasoner clears the cached result. Note that event occurrences can be also delivered out of order.
public long getStats()- returns the ms needed by the reasoner to process the last chunk of events.
public boolean shutDown() throws Exception- shuts down the reasoner.
The sources of jREC can be found here. The tool depends on TuProlog and on Log4J. Note that the tool is still under development, is undocumented and will print a lot of nonsense debug messages.
The sources of jREC can be found here. The package depends on JFreeChart, on the ui package SlickerBox developed by Fluxicon, and on the two ui packages
UITopiaResouces (see ProM 6). Note that the package is still under development.
resourcessubfolder with two property files for the coloring of normal and status fluents and with the file containing the domain-dependent theory. The screenshots above show the modeling and run panels of the tester. Note that:
savebutton will always work on that file (overwriting it). In order to preserve a certain domain theory, copy the
exec(Event)for representing events, while event occurrences are simply given in the run panel as
Event Time, one per row.
logbutton is pressed, all the event occurrences contained in the panel are delivered to the reasoner.
meta model- containing the Event Calculus formalization of ConDec templates extended with metric time,
model- containing a list of facts representing the specific ConDec model to be monitored,
run- the panel for delivering event occurrences and see the outcome. See the sample content to have a grasp about the approach.
meta model- containing the Event Calculus formalization of the lifecycle of timed commitments,
model- containing a list of facts representing the specific commitment model to be monitored,
run- the panel for delivering event occurrences and see the outcome. See the sample content to have a grasp about the approach (also a file
trace.txtis provided to show a sample trace).
CLIMB (Computational Logic for the verIfication and Modeling of Business constraints) is a framework based on computational logic (extensions of logic programming in particular) for the declarative, constraint-based specification of event-based systems (such as business processes, service interaction, clinical guidelines, multi-agent interaction protocols), and for providing reasoning and verification support along their entire lifecycle.
It is extensively described in Montali's book Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach.
CLIMB is composed of the following languages:
|The user selects an abstract business rule from a set of templates. Rules contain event patterns and expectations, which are in turn associated to an activity name, an event type (e.g. start, complete, abort of an activity), an originator and an execution time.|
|By clicking on the "customize" button, all the editable parts of the rule becomes visible and active. An element can be edited by fixing its value and/or adding specific constraints. Customized rules can be saved for future re-use.|
|Finally, the user can fix the time granularity used for the analysis and launch the analysis task. Such a task is carried out in Prolog, using the approach described in the paper Checking Compliance of Execution Traces to Business Rules. The final result is a partition of the input log into a compliant and noncompliant set. A new analysis phase can be then carried out by considering the whole log or only one of the two sets. Such sets can also separately feed other plug-ins.|
pluginscontains the jar of the plug-in (
SCIFFChecker.jar) and a subfolder (
SCIFFChecker) which includes two xml files that store the abstract rule templates and the user-defined rules. Both the jar and the subfolder must be copied into the
<Prom Distribution>/lib/plugins/folder of ProM.
externalcontains the external libraries required by SCIFF Checker, i.e. TuProlog and JFreeChart, which in turn requires JCommon. All these three jar files must be copied into the
<Prom Distribution>/lib/external/folder of ProM.
<ProM Distribution>/analyses.ini, adding a new line
<NEW KEY>is a unique alpha-numeric key. SCIFF Checker will consequently appear inside the analysis menu of ProM.