The WorkflowFM Reasoner is a logic-based library for correct-by-construction process modelling and composition.
It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/workflowfm-reasoner
Website and documentation is available here: http://docs.workflowfm.com/workflowfm-reasoner/
It is implemented as 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.