WorkflowFM Composer
The WorkflowFM Composer is a a diagrammatic tool for formally verified process modelling and composition.
It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/workflowfm-composer
Website and documentation is available here: http://docs.workflowfm.com/workflowfm-composer/
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 visualization using the PiVizTool.
- Export Scala code to execute workflows using the PEW engine.
- Export of PNG images.