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.
- 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.
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.
Petros Papapanagiotou - - -
A big thank you to the following contributors in order of appearance:
Groups & Organizations
|Artificial Intelligence Modelling Lab|
|Artificial Intelligence and its Applications Institute|
|School of Informatics, University of Edinburgh|
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.
Distributed under the Apache 2.0 license. See LICENSE for more information.