WorkflowFM: A logic-based framework for formal process specification and composition, by Petros Papapanagiotou and Jacques Fleuriot It presents a logic-based system for process specification and composition named WorkflowFM. It relies on an embedding of Classical Linear Logic and the so-called proofs-as-processes paradigm within the proof assistant HOL Light. This enables the specification of abstract processes as logical sequents and their composition via formal proof. The result is systematically translated to an executable workflow with formally verified consistency, rigorous resource accounting, and deadlock freedom. The 3-tiered server/client architecture of WorkflowFM allows multiple concurrent users to interact with the system through a purely diagrammatic interface, while the proof is performed automatically on the server. WorkflowFM is actively being used to model healthcare processes and patient pathways in collaboration with a number of clinical teams. The 26th International Conference of Automated Deduction (CADE-26) will be held 6-11 August 2017 in Gothenburg, Sweden. This article was published on 2024-11-22
