Edinburgh Research Explorer

WorkflowFM: A logic-based framework for formal process specification and composition

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://link.springer.com/chapter/10.1007%2F978-3-319-63046-5_22
Original languageEnglish
Title of host publication Automated Deduction – CADE 26
Subtitle of host publicationProceedings of the 26th International Conference on Automated Deduction (CADE 26)
PublisherSpringer, Cham
Pages357-370
Number of pages11
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

Conference

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

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.

Event

26th International Conference on Automated Deduction

6/08/1711/08/17

Gothenburg, Sweden

Event: Conference

Download statistics

No data available

ID: 36676830