A First-Order Logic verification framework for communication-parametric and time-aware BPMN collaborations

作者：

Highlights：

• A direct formal semantics for a subset of BPMN, including sub-processes, communication and time constructs.

• Automated verification of intra-organization workflows and inter-organization collaborations.

• Seven models for communication, two models for time.

• Communication models and properties of interest are easily extensible.

• Open source and freely available tools and model repository.

摘要

•A direct formal semantics for a subset of BPMN, including sub-processes, communication and time constructs.•Automated verification of intra-organization workflows and inter-organization collaborations.•Seven models for communication, two models for time.•Communication models and properties of interest are easily extensible.•Open source and freely available tools and model repository.

论文关键词：BPMN,Formal semantics,Collaboration,Communication,Time,Verification,First-Order Logic,TLA+,Tool

论文评审过程：Received 3 February 2020, Revised 11 March 2021, Accepted 15 March 2021, Available online 24 March 2021, Version of Record 23 November 2021.

论文官网地址：https://doi.org/10.1016/j.is.2021.101765