About
The WorkflowFM Composer consists of a Java-based server and GUI for formally verified process composition using the WorkflowFM Reasoner. It provides a visual, diagrammatic interface to specify processes based on their input and output resources, and compose them together to form more complex workflows.
Actions in the GUI of the Client are sent to the Server, which in turn is able to interact directly with the Reasoner. The Reasoner then performs the necessary logic-based inference within the rigorous environment of the HOL Light theorem prover.
The end result is a composite process that is provably correct and has the following 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.
Key Features
- Visual specification of processes based on ther input and output resources.
- Intuitive gestures for process composition.
- Formally verified composite processes based on rigorous logic-based reasoning.
- Simplified diagrammatic representation of complex logic-based deduction.
- Automated tracking of unused resources in compositions.
- Highlighting of matching resources.
- Workspaces for the development of multiple compositions at the same time.
- Workflow visuazliation using the PiVizTool.
- Export Scala code to execute workflows using the PEW engine.
- Export of PNG images.
Authors
Maintainer
Petros Papapanagiotou - 
- 
- 
Contributors
A big thank you to the following contributors in order of appearance:
- Jacques Fleuriot -
- Sean Wilson -
- James Vaughan
- Filip Smola
Groups & Organizations
| Artificial Intelligence Modelling Lab |
| Artificial Intelligence and its Applications Institute |
| School of Informatics, University of Edinburgh |
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. Papapanagoiotou, J. Fleuriot, S. Wilson. Diagrammatically-driven formal verification of Web-Services composition. Diagrams, 2012.
- P. Papapanagiotou. A formal verification approach to process modelling and composition. PhD Thesis, 2014.
License
Distributed under the Apache 2.0 license. See LICENSE for more information.
Copyright © 2009-2021 The University of Edinburgh and contributors