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

Petros Papapanagiotou; Jacques Fleuriot

doi:10.1007/978-3-319-63046-5_22

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

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 language	English
Title of host publication	Automated Deduction – CADE 26
Publisher	Springer
Pages	357-370
Number of pages	14
ISBN (Electronic)	978-3-319-63046-5
ISBN (Print)	978-3-319-63045-8
DOIs	https://doi.org/10.1007/978-3-319-63046-5_22
Publication status	Published - 11 Jul 2017
Event	26th International Conference on Automated Deduction - Gothenburg, Sweden Duration: 6 Aug 2017 → 11 Aug 2017 http://www.cse.chalmers.se/~myreen/cade-26/index.html

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Volume	10395
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Automated Deduction
Abbreviated title	CADE-26
Country/Territory	Sweden
City	Gothenburg
Period	6/08/17 → 11/08/17
Internet address	http://www.cse.chalmers.se/~myreen/cade-26/index.html

Access to Document

10.1007/978-3-319-63046-5_22Licence: All Rights Reserved

CADE_26_paper_35-2Accepted author manuscript, 340 KB

https://link.springer.com/chapter/10.1007%2F978-3-319-63046-5_22Licence: All Rights Reserved

The integration and interaction of multiple mathematical Reasoning Processes
Bundy, A., Aspinall, D., Colton, S., Fleuriot, J., Gow, J., Grov, G., Ireland, A., Jackson, P., Mcneill, F., Michaelson, G. & Smaill, A.
EPSRC
1/11/15 → 31/10/19
Project: Research
ProofPeer: Collaborative Theorem Proving
Fleuriot, J. & Aspinall, D.
EPSRC
1/04/14 → 31/03/17
Project: Research
SOCIAM: the theory and proctice of social machines
Robertson, D. & Buneman, P.
EPSRC
1/06/12 → 31/05/17
Project: Research

Jacques Fleuriot
- jdfinf.ed.acuk
- School of Informatics - Personal Chair of Artificial Intelligence
- Artificial Intelligence and its Applications Institute
- Data Science and Artificial Intelligence
Person: Academic: Research Active

Cite this

@inproceedings{4f5a62a56a1b4467a45cae6260a8c6e8,

title = "WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition",

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.",

author = "Petros Papapanagiotou and Jacques Fleuriot",

year = "2017",

month = jul,

day = "11",

doi = "10.1007/978-3-319-63046-5_22",

language = "English",

isbn = "978-3-319-63045-8",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "357--370",

booktitle = "Automated Deduction – CADE 26",

note = "26th International Conference on Automated Deduction, CADE-26 ; Conference date: 06-08-2017 Through 11-08-2017",

url = "http://www.cse.chalmers.se/~myreen/cade-26/index.html",

}

TY - GEN

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

AU - Papapanagiotou, Petros

AU - Fleuriot, Jacques

PY - 2017/7/11

Y1 - 2017/7/11

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-63046-5_22

DO - 10.1007/978-3-319-63046-5_22

M3 - Conference contribution

SN - 978-3-319-63045-8

T3 - Lecture Notes in Computer Science

SP - 357

EP - 370

BT - Automated Deduction – CADE 26

PB - Springer

T2 - 26th International Conference on Automated Deduction

Y2 - 6 August 2017 through 11 August 2017

ER -

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

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Projects

The integration and interaction of multiple mathematical Reasoning Processes

ProofPeer: Collaborative Theorem Proving

SOCIAM: the theory and proctice of social machines

Profiles

Jacques Fleuriot

Cite this