Login | Register

Specifying and Verifying Contract-driven Composite Web Services: a Model Checking Approach


Specifying and Verifying Contract-driven Composite Web Services: a Model Checking Approach

Bataineh, Ahmed (2014) Specifying and Verifying Contract-driven Composite Web Services: a Model Checking Approach. Masters thesis, Concordia University.

Text (application/pdf)
Bataineh_MASc_F2014.pdf - Accepted Version


As a promising computing paradigm in the new era of cross-enterprise e-applications, web services technology works as plugin mode to provide a value-added to applications using Service-Oriented Computing (SOC) and Service-Oriented Architecture (SOA). Verification is an important issue in this paradigm, which focuses on abstract business contracts and where services’ behaviors are generally classified in terms of compliance with / violation of their contracts. However, proposed approaches fail to describe in details both compliance and violation behaviors, how the system can distinguish between them, and how the system reacts after each violation. In this context, specifying and automatically generating verification properties are challenging key issues. This thesis proposes a novel approach towards verifying the compliance with contracts regulating the composition of web services. In this approach, properties against which the system is verified are generated automatically from the composition’s implementation. First, Business Process Execution Language (BPEL)that specifies actions within business processes with web services is extended to create custom activities, called labels. Those labels are used as means to represent the specifications and mark the points the developer aims to verify. A significant advantage of this labeling is the ability to target specific points in the design to be verified, which makes this verification very focused. Second, new translation rules from the extended BPEL into ISPL, the input language of the MCMAS model checker, are provided so that model checking the behavior of our contract-driven compositions is possible. The verification properties are expressed in the CTLC logic, which provides a powerful representation for modeling composition contracts using commitment-based multiagent interactions. A detailed case study with experimental results are also reported ins the thesis.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science
Item Type:Thesis (Masters)
Authors:Bataineh, Ahmed
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Bentahar, Jamal and Dssouli, Rachida
ID Code:978987
Deposited On:03 Nov 2014 14:38
Last Modified:18 Jan 2018 17:48
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

Back to top Back to top