Verifying BPEL Workflows Under Authorisation Constraints

Date of this Version

September 2006

Document Type

Book Chapter

Publication Details

Xiangpeng, Zhao, Cerone, Antonio and Krishan, Padmanabhan (2006) Verifying BPEL workflows under authorisation constraints was presented at the Business Process Management 2006 International Workshops, 4-7 September 2006, Vienna, Austria.
This conference paper has been published as a book chapter and is available in Business Process Management Workshops

2006 HERDC submission


Business Process Execution Language (BPEL), or Web Services BPEL (WS-BPEL), is the standard for specifying workflow process definition using web services. Research on formal modelling and verificiation of BPEL has largely concentrated on control flow and data flow, while security related properties have received little attention. In this work, we present a formal framework that integrates Role Based Access Control (RBAC) into BPEL and allows us to express authorisation constraints, using temporal logic. Using this framework, we show how model-checking can be applied to verify that a given BPEL process satisfies the security constraints.

This document is currently not available here.



This document has been peer reviewed.