Useful links for Formal Verification of BPMN and DMN
The following papers are ordered by date of publication in descending order. If there should be a better way to organize, do advise.
Verification of BPMN Models
Paper not available but can be requested
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. "
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.
A formal verification framework for business process models. The 13 page paper available at https://orbit.dtu.dk/files/140314916/08115708.pdf
Event Log Based approach
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
Formal Verification of Time-Aware Cloud Resource Allication in Business Process
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.
Toward a Time-centric modeling of Business Processes in BPMN 2.0
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
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann.
Two papers using EventB
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.)
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 Aljosha for contributing 2 suggestions for UPPAL