WorkflowFM Reasoner

A logic-based library for correct-by-construction process modelling and composition.

About

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.

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.

Modes

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.