Two sections: papers and software
https://github.com/pascalpoizat/fbpmn
The following papers are ordered by date of publication in descending order. If there should be a better way to organize, do advise.
2020
Paper not available but can be requested
https://www.researchgate.net/publication/337568373_Verification_of_BPMN_Models
2018
this paper proposed "new methodology for the specification and the verification of business processes based on BPMN and refinement, and using NuSMV model checker for the verification. This allows the developer to guarantee that the properties of a business process are conserved by the different refinement patterns. We won’t make an automatic re- finement because until now it’s an interactive step of our approach. "
2017
https://hal.inria.fr/hal-01591665/document is a paper on automated verification of bpmn processes where the software is available at https://pascalpoizat.github.io/vbpmn-web/ as VBPMN.
VBPMN supports formal modelling and automated analysis of business processes using formal verification tools. It features a web interface for comparing BPMN 2.0 models.
2017
A formal verification framework for business process models. The 13 page paper available at https://orbit.dtu.dk/files/140314916/08115708.pdf
2016
https://www.researchgate.net/publication/313878941_Verification_of_BPMN_20_Process_Models_An_Event_Log-based_Approach PAPER AVAILABLE at webpage by scrolling downwards
Their approach seems to be using Activiti Engine a Java based BP Automation engine and run event log to verify
2016
Formal Verification of Time-Aware Cloud Resource Allication in Business Process
2014
Enabling model checking for collaborative process analysis: from BPMN to ‘Network of Timed Automata
The authors transform BPMN processes into UPPAAL Timed Automata and apply temporal logic formulas afterwards.
2013
Toward a Time-centric modeling of Business Processes in BPMN 2.0
https://hal.archives-ouvertes.fr/file/index/docid/921390/filename/iiWAS_2013.pdf
UPPAAL is is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). Requires commercial license but can get a non-commercial license for academia
2012
http://homepages.cs.ncl.ac.uk/carlos.molina/home.formal/JimDissertation2012.pdf
using Promela
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann.
Two papers using EventB
2019
https://ieeexplore.ieee.org/abstract/document/8754325
Paper not available (but I got a copy somehow but I respect the authors so not putting it up as public link. Ask me for it if need it.)
2010
https://t.co/n66qXhAlhk Formal Analysis of BPMN models using Event-B
https://en.wikipedia.org/wiki/Rodin_tool The Rodin tool is a tool for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling.
Feel free to fork or send pull request. I'm interested in this topic myself.
Thanks to Meng and his original thread on this topic for finding most of the links here.
Thanks to Aljosha for contributing 2 suggestions for UPPAL
https://hal.archives-ouvertes.fr/file/index/docid/921390/filename/iiWAS_2013.pdf uses UPPAAL to verify BPMN extended with temporals.