Welcome to the InfoSci Platform
Reference Hub5
CTL Model Checking of Web Services Composition based on Open Workflow Nets Modeling

CTL Model Checking of Web Services Composition based on Open Workflow Nets Modeling

Zohra Sbaï, Rawand Guerfel
Copyright: © 2016 |Volume: 7 |Issue: 1 |Pages: 16
ISSN: 1947-959X|EISSN: 1947-9603|EISBN13: 9781466690943|DOI: 10.4018/IJSSMET.2016010102
Cite Article Cite Article

MLA

Sbaï, Zohra, and Rawand Guerfel. "CTL Model Checking of Web Services Composition based on Open Workflow Nets Modeling." IJSSMET vol.7, no.1 2016: pp.27-42. http://doi.org/10.4018/IJSSMET.2016010102

APA

Sbaï, Z. & Guerfel, R. (2016). CTL Model Checking of Web Services Composition based on Open Workflow Nets Modeling. International Journal of Service Science, Management, Engineering, and Technology (IJSSMET), 7(1), 27-42. http://doi.org/10.4018/IJSSMET.2016010102

Chicago

Sbaï, Zohra, and Rawand Guerfel. "CTL Model Checking of Web Services Composition based on Open Workflow Nets Modeling," International Journal of Service Science, Management, Engineering, and Technology (IJSSMET) 7, no.1: 27-42. http://doi.org/10.4018/IJSSMET.2016010102

Export Reference

Mendeley
Favorite Full-Issue Download

Abstract

Web services composition (WSC) has an enormous potential for the organizations in the B2B area. In fact, different services collaborate through the exchange of messages to implement complex business processes. BPEL is one of the most used languages to develop such cooperation. However, it has been proved that its use is complex and can require some expertise in XML syntax. Even its graphical representation is not evident to handle. This is why the authors propose to model Web services using oWF-nets, a subclass of Petri nets, and then, to translate them to BPEL. Whilst, a WSC is with added value only if the involved services are compatible. So in this context, across the translation proposed the researchers develop a verification layer of the WSC compatibility. Hence, they propose a framework named D&A4WSC which allows to model the WSC by oWF-nets, to check their compatibility with the model checker NuSMV and to translate them if they are compatible in BPEL processes using the oWFN2BPEL compiler. D&A4WSC permits, furthermore, to formally analyze a BPEL process.

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.