WorkflowFM Reasoner
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/
About
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.
The constructed workflows can be exported either for visualization using the PiVizTool or as Scala code for execution using the PEW engine.
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.