Behavior modeling and automated verification of Web services

Document Type

Article

Source of Publication

Information Sciences

Publication Date

2-10-2014

Abstract

Cloud computing has been rapidly adopted over the last few years. However, techniques on Web services, one of the most important enabling technologies for cloud computing, are still not mature yet. In this paper, we propose a novel approach that supports dependable development of Web services. Our approach includes a new Web service model that separates service behaviors into operational and control behaviors. The coordination of operational and control behaviors at runtime is facilitated by conversational messages. We also propose an automated service verification approach based on symbolic model checking. In particular, our approach extracts the checking properties, in the form of temporal logic formulas, from control behaviors, and automatically verifies the properties in operational behaviors using the NuSMV model checker. The approach presented in this paper has been implemented using a number of state-of-the-art technologies. We conducted a number of experiments to study the performance of our proposed approach in detecting design problems in services. The results show that our automated approach can successfully detect service design problems. Our system offers a set of tools assisting service developers in specifying, debugging, and monitoring service behaviors. © 2013 Elsevier Inc. All rights reserved.

ISSN

0020-0255

Publisher

Elsevier

Volume

258

First Page

416

Last Page

433

Disciplines

Computer Sciences | Mathematics

Keywords

Cloud computing, Conversation message, Service behavior, Symbolic model checking, Web service

Scopus ID

84889084078

Indexed in Scopus

yes

Open Access

no

Link to Full Text

Share

COinS