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

被引：4
|
作者：
Papapanagiotou, Petros [1 ]
Fleuriot, Jacques [1 ]
机构：
[1] Univ Edinburgh, Sch Informat, 10 Crichton St, Edinburgh EH8 9AB, Midlothian, Scotland
来源：
AUTOMATED DEDUCTION - CADE 26 | 2017年 / 10395卷
基金：
英国工程与自然科学研究理事会;
关键词：
Process modelling; Workflows; Theorem proving; Classical linear logic; LINEAR LOGIC; HEALTH-CARE; PROPOSITIONS;
D O I：
10.1007/978-3-319-63046-5_22
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
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.
引用
收藏
页码：357 / 370
页数：14
相关论文
共 50 条
  • [21] A Logic-Based Framework for Verifying Consensus Algorithms
    Dragoi, Cezara
    Henzinger, Thomas A.
    Veith, Helmut
    Widder, Josef
    Zufferey, Damien
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION: (VMCAI 2014), 2014, 8318 : 161 - 181
  • [22] Quantitative logic-based framework for agile methodologies
    Pedrycz, Witold
    JOURNAL OF SYSTEMS ARCHITECTURE, 2006, 52 (11) : 700 - 707
  • [23] A formal framework for agent itinerary specification, security reasoning and logic analysis
    Lu, SY
    Xu, CZ
    25TH IEEE INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS, PROCEEDINGS, 2005, : 580 - 586
  • [24] A Framework for Formal Specification Considering Review and Specification-Based Testing
    Nakatsugawa, Yasumasa
    Kurita, Taro
    Araki, Keijiro
    TENCON 2010: 2010 IEEE REGION 10 CONFERENCE, 2010, : 2444 - 2448
  • [25] Designing and Applying a Framework for Logic-Based Model Querying
    Dohrmann, Patrick
    Herold, Sebastian
    36TH EUROMICRO CONFERENCE ON SOFTWARE ENGINEERING AND ADVANCED APPLICATIONS, 2010, : 164 - 171
  • [26] COOPLAN - A LOGIC-BASED FRAMEWORK FOR COOPERATIVE RESPONSE GENERATION
    NUNES, MGV
    COMPUTERS AND ARTIFICIAL INTELLIGENCE, 1993, 12 (05): : 461 - 474
  • [27] A logic-based framework for reasoning support in software evolution
    Vescoukis, VC
    Papaspyrou, N
    Skordalakis, E
    ADVANCED INFORMATION SYSTEMS ENGINEERING, 1996, 1080 : 44 - 59
  • [28] Complexity of logic-based argumentation in Schaefer's framework
    Creignou, Nadia
    Egly, Uwe
    Schmidt, Johannes
    COMPUTATIONAL MODELS OF ARGUMENT, 2012, 245 : 237 - +
  • [29] A Logic-Based Computational Framework for Inferring Cognitive Affordances
    Sarathy, Vasanth
    Scheutz, Matthias
    IEEE TRANSACTIONS ON COGNITIVE AND DEVELOPMENTAL SYSTEMS, 2018, 10 (01) : 26 - 43
  • [30] Complexity of logic-based argumentation in Post's framework
    Creignou, Nadia
    Schmidt, Johannes
    Thomas, Michael
    Woltran, Stefan
    ARGUMENT & COMPUTATION, 2011, 2 (2-3) : 107 - 129
12345