Reference

Welcome to the WorkflowFM Reasoner documentation. This is a HOL Light library that allows for rigorous, formally verified process specification and composition. Processes can be specified based on the types of their input and output resources, using Classical Linear Logic (CLL) sequents. Composition can then be achieved using forward chaining/inference of CLL rules.

Inference can be applied directly using the standard HOL Light interactive proof setting and the embed library. Alternatively, the WorkflowFM Reasoner also provides its own interface with intuitive commands that greatly facilitate process specification and composition.

CLL proofs are annotated with π-calculus process terms based on the proofs-as-processes paradigm. These provide an executable translation of the logical composition. The resulting workflows are correct-by-construction with the following verified properties:

• Systematic resource accounting: The linearity of CLL guarantees that no resources appear out of nowhere or disappear into thin air.
• Deadlock and livelock freedom: The proofs-as-processes paradigm guarantees that the constructed workflows have no deadlocks or livelocks.
• Type checked composition: Even though the generated π-calculus term is untyped, the correctness of the types of all connected resources is ensured via the logical proof.
• Fully asynchronous and concurrent execution: The π-calculus naturally offers a workflow execution style where 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.