Journal
AUTOMATED DEDUCTION - CADE 26
Volume 10395, Issue -, Pages 357-370Publisher
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-319-63046-5_22
Keywords
Process modelling; Workflows; Theorem proving; Classical linear logic
Categories
Funding
- EPSRC [EP/N014758/1, EP/J017728/1, EP/L011794/1]
- EPSRC [EP/J017728/2, EP/N014758/1, EP/L011794/1] Funding Source: UKRI
Ask authors/readers for more resources
We present 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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available