Master Thesis Defense - December 17, 2015: Model Checking Commitment-Governed Compositions of Web Services

Ana Vazquez Urbina

Thursday, December 17, 2015 at 10:30 a.m.
Room EV001.162

You are invited to attend the following M.A.Sc. (Quality Systems Engineering) thesis examination.

Examining Committee

Dr. A. Ben Hamza, Chair
Dr. J. Bentahar, Supervisor
Dr. R. Dssouli, CIISE Examiner
Dr. J. Rilling, External Examiner (CSE)

Abstract

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.