Symbolic model checking composite Web services using operational and control behaviors

Document Type

Article

Source of Publication

Expert Systems with Applications

Publication Date

2-1-2013

Abstract

This paper addresses the issue of verifying if composite Web services design meets some desirable properties in terms of deadlock freedom, safety (something bad never happens), and reachability (something good will eventually happen). Composite Web services are modeled based on a separation of concerns between business and control aspects of Web services. This separation is achieved through the design of an operational behavior, which defines the composition functioning according to the Web services' business logic, and a control behavior, which identifies the valid sequences of actions that the operational behavior should follow. These two behaviors are formally defined using automata-based techniques. The proposed approach is model checking-based where the operational behavior is the model to be checked against properties defined in the control behavior. The paper proves that the proposed technique allows checking the soundness and completeness of the design model with respect to the operational and control behaviors. Moreover, automatic translation procedures from the design models to the NuSMV model checker's code and a verification tool are reported in the paper. © 2012 Elsevier Ltd. All rights reserved.

ISSN

0957-4174

Publisher

Elsevier

Volume

40

Issue

2

First Page

508

Last Page

522

Disciplines

Computer Sciences

Keywords

Behavior, Completeness, Composite Web service, NuSMV, Soundness, Symbolic model checking

Scopus ID

84867683172

Indexed in Scopus

yes

Open Access

no

Link to Full Text

Share

COinS