Symbolic model checking composite Web services using operational and control behaviors

Jamal Bentahar, Hamdi Yahyaoui, Melissa Kova, Zakaria Maamar

Research output: Contribution to journalArticlepeer-review

44 Scopus citations

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.

Original languageBritish English
Pages (from-to)508-522
Number of pages15
JournalExpert Systems with Applications
Volume40
Issue number2
DOIs
StatePublished - 1 Feb 2013

Keywords

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

Fingerprint

Dive into the research topics of 'Symbolic model checking composite Web services using operational and control behaviors'. Together they form a unique fingerprint.

Cite this