Login | Register

Model Checking Commitment-Governed Compositions of Web Services


Model Checking Commitment-Governed Compositions of Web Services

Vazquez, Ana (2015) Model Checking Commitment-Governed Compositions of Web Services. Masters thesis, Concordia University.

[thumbnail of Vazquez_MASc_S2016.pdf]
Text (application/pdf)
Vazquez_MASc_S2016.pdf - Accepted Version


We propose a new approach towards verifying compositions of web services using model checking. In order to perform such a verification, we transform the web service composition into a Multi-Agent System (MAS) model where the process in charge of the composition and the participating services are represented by agents. We model the behavior of the resulting MAS using the extended Interpreted Systems Programming Language (ISPL+), the dedicated language of the MCMAS+ model checker for MAS. We use commitments between agents to regulate and reason about messages between composite web services. The properties against which the compositions are verified are expressed in the Computation Tree Logic of Commitments (CTLC), an extension of the branching logic CTL that supports commitment modalities.

We describe BPEL2ISPL+, a tool we developed to perform the automatic transformation from the web service composition described in Business Process Execution Language (BPEL) into a verifiable MAS model described in ISPL+. The BPEL2ISPL+ tool is applied to a concrete BPEL web service composition and its accurate representation in ISPL+ is obtained. The CTLC properties used to verify the compositions regulated by commitments are represented along with the agents abstracting the participating web services. The MCMAS+ model checker is used to verify the model against these properties, providing thus a new approach to model check agent-based web service compositions governed by commitments.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering
Item Type:Thesis (Masters)
Authors:Vazquez, Ana
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Quality Systems Engineering
Date:December 2015
Thesis Supervisor(s):Bentahar, Jamal
ID Code:980754
Deposited On:16 Jun 2016 14:30
Last Modified:18 Jan 2018 17:51
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top