Welcome to the InfoSci Platform
Reference Hub1
Applying Formal Methods to Verify Web Services Orchestration and Choreography

Applying Formal Methods to Verify Web Services Orchestration and Choreography

Zohra Sbai
Copyright: © 2018 |Pages: 23
ISBN13: 9781522559511|ISBN10: 1522559515|EISBN13: 9781522559528
DOI: 10.4018/978-1-5225-5951-1.ch011
Cite Chapter Cite Chapter

MLA

Sbai, Zohra. "Applying Formal Methods to Verify Web Services Orchestration and Choreography." Multidisciplinary Approaches to Service-Oriented Engineering, edited by Mehdi Khosrow-Pour, D.B.A., IGI Global, 2018, pp. 221-243. https://doi.org/10.4018/978-1-5225-5951-1.ch011

APA

Sbai, Z. (2018). Applying Formal Methods to Verify Web Services Orchestration and Choreography. In M. Khosrow-Pour, D.B.A. (Ed.), Multidisciplinary Approaches to Service-Oriented Engineering (pp. 221-243). IGI Global. https://doi.org/10.4018/978-1-5225-5951-1.ch011

Chicago

Sbai, Zohra. "Applying Formal Methods to Verify Web Services Orchestration and Choreography." In Multidisciplinary Approaches to Service-Oriented Engineering, edited by Mehdi Khosrow-Pour, D.B.A., 221-243. Hershey, PA: IGI Global, 2018. https://doi.org/10.4018/978-1-5225-5951-1.ch011

Export Reference

Mendeley
Favorite

Abstract

The contribution presented in this chapter is to provide a formal framework ensuring the model checking based verification of the Composition of Web Services (WSC). For this, the authors propose first to model the web services composition by an interaction of open workflow nets: a special class of Petri nets. Then, they detail how to check behavioral properties specified in temporal logic using the model checker NuSMV. A WSC is with added value only if the involved services are compatible. So, in this context, across the translation proposed, the authors develop a verification layer of the WSC compatibility. This work is developed in a framework named D&A4WSC which allows to model the WSC by oWF-nets and to check their compatibility by invoking the model checker NuSMV. Furthermore, the authors extended D&A4WSC so that it permits a web services choreography described in a WS-CDL specification. For this they developed a translation from WS-CDL to a composition of oWF-nets, so that one can verify this choreography by the aforementioned approach.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.