SCIFF

The SCIFF Proof Procedure is a transition system which implements the operational proof-theoretic counterpart of SCIFF declarative semantics. It adopts a depth-first strategy and has been developed in SICSTUS Prolog and CHR. At a certain time:

it firstly matches a specification w.r.t. the already happened events, generating a set of (positive and negative) expectations;
it then verifies whether generated expectations are effectively fulfilled by the concrete execution, i.e., whether each positive (negative resp.) expectation has (does not have resp.) a corresponding happened event.

The latest version of SCIFF can be downloaded from here. Each specification is embedded into a so-called SCIFF project. For CLIMB, an example project is available. To support run-time verification, the proof is able to run in two different modalities:

open. Current pending expectations are suspended, waiting for further events. A positive expectation is pending if it has not yet been fulfilled but it is still satisfiable, whereas a negative expectation is pending if it is still possible to violate it. To run SCIFF in open modality, type the query :-run_open in SICSTUS.
closed. The proof makes the hypotheses that no further event can happen (i.e., that the current execution is completed). As a consequence, it evaluates pending expectations: negative pending expectations are fulfilled, whereas positive pending expectations are violated. To run SCIFF in closed modality, type :-run in SICSTUS.

g-SCIFF extends the proof procedure by modifying fulfillment of expectations: after having analyzed the (partial) execution trace given as input (if any), it tries to complete it by considering positive pending expectations and simulating corresponding happened events (which may trigger new rules). g-SCIFF is invoked like SCIFF, but by previously activating fulfillment’s extension (with the command :-set_option(fulfiller, on)).
As specified in the Static Verification section, the CLIMB framework exploits g-SCIFF for detecting conflicts and discovering the presence of dead activities. To this purpose, two queries are respectively supported in the CLIMB example project: :-conflicts and :-deadActivities.

Please check instructions on the right to download, install and configure CLIMB projects inside SCIFF.

CLIMB Projects

To install the basic CLIMB example project:

Create a folder which will contain the different SCIFF (and CLIMB) projects.
Compile a file called defaults.pl in the SCIFF directory, by inserting the path of the project directory. This is done by specifying a fact of the type default_dir(Directory)
Download the example project.
Expand the project in the projects folder. The folder containing the project also defines its “name”.
Configure SCIFF to use the r_solver (see SCIFF’s developer manual).
Open SICSTUS and consult the file sciff.pl (contained in the SCIFF root directory).
Load the project by calling the query :-project(Prj) where Prj is the name of the project to be loaded.
Perform different kind of verifications by invoking queries from the SICSTUS console.

CLIMB Models

To specify a CLIMB model in SCIFF starting from the example project:

Insert model’s constraints (as SCIFF rules) in the file called climbModel.txt.
Insert the background knowledge of the model into the file called climbKB.pl
Modify the activities contained into climbKB.pl by specifying the list of all activities involved in the model (this fact is used to evaluate dead activities).

If the purpose is to verify conformance of an execution trace:

Insert the different happened events into the file climbHistory.pl. Each happened event is a fact of the type hap(Event, T), where T is an integer and Event, for CLIMB, is bound to performed(A) (being A the performed activity at time T).

Interoperability

Interoperability can be seamlessly addressed by specifying the CLIMB models of choreography and local parties, each in a separate file (contained inside the project folder). To join all constraints, simply modify project.pl by adding a fact of the type ics_file(FileName) for each file.

CLIMB

Computational Logic for the verIfication and Modeling of Business processes and choreographies

Sections

Acknowledgments

SCIFF

CLIMB Projects

CLIMB Models

Interoperability