Toggle Main Menu Toggle Search

Open Access padlockePrints

The Newcastle University research output collection, currently available on ePrints, will shortly be moving to a new open repository platform, Figshare. To prepare for the data migration we have paused adding new content to ePrints, and will resume once the new repository is launched. During this time you will continue to have access to ePrints (but no new content will appear). We will share updates here when available.

A Tool for the Automatic Verification of BPMN Choreographies

Lookup NU author(s): Dr Ellis SolaimanORCiD, Dr Carlos Molina-Jimenez

Downloads

Licence

This is the final published version of a report that has been published in its final definitive form by School of Computing Science, University of Newcastle upon Tyne, 2015.

For re-use rights please refer to the publisher's terms and conditions.

Abstract

The Business Process Model Notation (BPMN) provides a standard graphical language that can be used by business analysts for modeling business process choreographies. A challenging task is to formally verify that constructed choreography models are logically correct with respect to safety, liveness, and various application-specific correctness requirements. To aid with this important task, we present a model checker based framework to automate the verification process. The main component of our framework is the BPMNverifier, a tool that can automatically convert BPMN choreography models into PROMELA, the input language of the SPIN model checker. We describe the implementation and functionality of the BPMNverifier, and how the tool eases the task of expressing Linear Temporal Logic (LTL) correctness requirements, through its LTL Manager component.

Publication metadata

Author(s): Solaiman E, Sun W, Molina-Jimenez C

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2015

Pages: 11

Online publication date: 01/04/2015

Report Number: 1464

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1464.pdf

Share