WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present a logic-based system for process specication 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 work ow 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.
Original languageEnglish
Title of host publicationAutomated Deduction – CADE 26
PublisherSpringer, Cham
Number of pages14
ISBN (Electronic)978-3-319-63046-5
ISBN (Print)978-3-319-63045-8
Publication statusPublished - 11 Jul 2017
Event26th International Conference on Automated Deduction - Gothenburg, Sweden
Duration: 6 Aug 201711 Aug 2017

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference26th International Conference on Automated Deduction
Abbreviated titleCADE-26
Internet address


Dive into the research topics of 'WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition'. Together they form a unique fingerprint.

Cite this