Skip to main content
Verifying BPEL Workflows Under Authorisation Constraints
Information Technology papers
  • Zhao Xiangpeng, Peking University, Beijing, China
  • Antonio Cerone, UNU-IIST Macau, China
  • Padmanabhan Krishnan, Bond University
Date of this Version
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.
Citation Information
Zhao Xiangpeng, Antonio Cerone and Padmanabhan Krishnan. "Verifying BPEL Workflows Under Authorisation Constraints" (2006)
Available at: