Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Links to formal verification of BPMN / DMN

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

2020

Paper not available but can be requested

https://www.researchgate.net/publication/337568373_Verification_of_BPMN_Models

using NuSMV

2018

https://www.researchgate.net/publication/326103821_A_New_Approach_for_the_Verification_of_BPMN_Models_Using_Refinement_Patterns

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

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.

BProVe

2017

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

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

Screenshot 2020-01-21 at 9 27 39 PM

UPPAL

2016

Formal Verification of Time-Aware Cloud Resource Allication in Business Process

https://www.researchgate.net/publication/309228439_Formal_Verification_of_Time-Aware_Cloud_Resource_Allocation_in_Business_Process

2014

Enabling model checking for collaborative process analysis: from BPMN to ‘Network of Timed Automata

https://www.researchgate.net/publication/271757257_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

Promela

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.

EventB

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

Feel free to fork or send pull request. I'm interested in this topic myself.

Acknowledgements

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

@mengwong

This comment has been minimized.

Copy link

@mengwong mengwong commented Jan 22, 2020

https://hal.archives-ouvertes.fr/file/index/docid/921390/filename/iiWAS_2013.pdf uses UPPAAL to verify BPMN extended with temporals.

@simkimsia

This comment has been minimized.

Copy link
Owner Author

@simkimsia simkimsia commented Jan 22, 2020

https://hal.archives-ouvertes.fr/file/index/docid/921390/filename/iiWAS_2013.pdf uses UPPAAL to verify BPMN extended with temporals.

Added in revision #6

@aljoshakoecher

This comment has been minimized.

Copy link

@aljoshakoecher aljoshakoecher commented Apr 26, 2021

You might wanna add Enabling model checking for collaborative process analysis: from BPMN to ‘Network of Timed Automata’ to the UPPAAL section. The authors transform BPMN processes into UPPAAL Timed Automata and apply temporal logic formulas afterwards.

@aljoshakoecher

This comment has been minimized.

Copy link

@aljoshakoecher aljoshakoecher commented Apr 26, 2021

And while you're at it, you can add Formal Verification of Time-Aware Cloud Resource Allocation in Business Process to that same section (UPPAAL) 😃

@simkimsia

This comment has been minimized.

Copy link
Owner Author

@simkimsia simkimsia commented Apr 26, 2021

You might wanna add Enabling model checking for collaborative process analysis: from BPMN to ‘Network of Timed Automata’ to the UPPAAL section. The authors transform BPMN processes into UPPAAL Timed Automata and apply temporal logic formulas afterwards.

Added in revision #7

@simkimsia

This comment has been minimized.

Copy link
Owner Author

@simkimsia simkimsia commented Apr 26, 2021

And while you're at it, you can add Formal Verification of Time-Aware Cloud Resource Allocation in Business Process to that same section (UPPAAL) 😃

Added in revision #8

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment