WorkflowFM Reasoner

A logic-based library for correct-by-construction process modelling and composition.

Artificial Intelligence Modelling Lab

Artificial Intelligence and its Applications Institute

School of Informatics, University of Edinburgh

This is part of the WorkflowFM framework for correct-by-construction process and resource workflows.

More info and documentation can be found in the main webpage.

About

This is a logic-based library for the interactive theorem prover HOL Light that allows for rigorous, formally verified process specification and composition. The resulting workflows are correct-by-construction with the following verified properties:

• Systematic resource accounting: No resources appear out of nowhere or disappear into thin air.
• Deadlock and livelock freedom: The constructed workflows can be executed without fear for deadlocks or livelocks.
• Type checked composition: The correctness of the types of all connected resources is ensured via the logical proof.
• Fully asynchronous and concurrent execution: During workflow execution, each component process can be executed fully asynchronously (see the PEW engine for more details) and concurrently, without introducing any conflicts, race conditions, or deadlocks.

The constructed workflows can be exported either for visualization using the PiVizTool or as Scala code for execution using the PEW engine.

The references provide more in depth details of the theory behind the WorkflowFM Reasoner.

Key Features

• Process specification using Classical Linear Logic (CLL).
• Process composition using formally verified forward inference.
• Interactive theorem proving in CLL.
• Intuitive high-level actions for sequential, conditional, and parallel composition.
• Proof translation to π-calculus.
• Modular encoding allows different CLL translations (e.g. to session types), automatically reconstructing the entire process reasoning framework.
• Tracking of provenance metadata during proof to guide visualization.
• Export π-calculus to PiVizTool format.
• Export Scala code to execute workflows using the PEW engine.
• Modular API allows extensions with new composition actions, export options and commands.

Modes

The reasoner can run in 2 modes:

• Console: This mode is intended for standard use within HOL Light, i.e. at the OCaml toplevel. It provides a minimal console interface for process modelling and composition.
• JSON: This mode is intended for use within a server environment, to allow interaction with web applications (including UIs). It expects input and produces output encoded in JSON format.

Quick Install

Clone the following HOL Light fork: https://github.com/workflowfm/hol-light

git clone https://github.com/workflowfm/hol-light.git

Then make sure all the submodules are initialised and updated:

git submodule update --init --recursive

Install HOL Light following its standard installation instructions.

Once you have HOL Light up and running, you can load the reasoner in console mode using the following command:

loads (!hol_dir ^ "/workflowfm/make.console.ml");;

If you need to use the JSON mode, you can use this command instead:

loads (!hol_dir ^ "/workflowfm/make.ml");;

More detailed installation instructions are available at this link.

Authors

Maintainer

Petros Papapanagiotou - pe.p@ed.ac.uk - @PetrosPapapa

Contributors

A big thank you to the following contributors in order of appearance:

• Jacques Fleuriot

References

Please cite the following publication in reference to this project:

• P. Papapanagiotou, J. Fleuriot. WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition. CADE, 2017.

Sample of other relevant references:

• P. Papapanagiotou, J. Fleuriot. Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus. ECOWS, 2011.
• P. Papapanagiotou. A formal verification approach to process modelling and composition. PhD Thesis, 2014.
• P. Papapanagiotou, J. Fleuriot. A Pragmatic, Scalable Approach to Correct-by-construction Process Composition Using Classical Linear Logic Inference. LOPSTR, 2019.

License

Distributed under the Apache 2.0 license. See ./LICENSE for more information.

Copyright © 2009-2021 The University of Edinburgh and contributors