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

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

Abstract

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
Pages357-370
Number of pages14
ISBN (Electronic)978-3-319-63046-5
ISBN (Print)978-3-319-63045-8
DOIs
Publication statusPublished - 11 Jul 2017
Event26th International Conference on Automated Deduction - Gothenburg, Sweden
Duration: 6 Aug 201711 Aug 2017
http://www.cse.chalmers.se/~myreen/cade-26/index.html

Publication series

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

Conference

Conference26th International Conference on Automated Deduction
Abbreviated titleCADE-26
Country/TerritorySweden
CityGothenburg
Period6/08/1711/08/17
Internet address

Fingerprint

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