IRMA-International.org: Creator of Knowledge
Information Resources Management Association
Advancing the Concepts & Practices of Information Resources Management in Modern Organizations

A Formal Approach for the Validation of Web Service Orchestrations

A Formal Approach for the Validation of Web Service Orchestrations
View Sample PDF
Author(s): Wael Sellami (ReDCAD, FSEGS, University of Sfax, Sfax, Tunisia), Hatem Hadj Kacem (ReDCAD, FSEGS, University of Sfax, Sfax, Tunisia)and Ahmed Hadj Kacem (ReDCAD, FSEGS, University of Sfax, Sfax, Tunisia)
Copyright: 2013
Volume: 5
Issue: 1
Pages: 14
Source title: International Journal of Web Portals (IJWP)
DOI: 10.4018/jwp.2013010104

Purchase

View A Formal Approach for the Validation of Web Service Orchestrations on the publisher's website for pricing and purchasing information.

Abstract

A web service composition is considered as a real revolution in SOA (Service Oriented Architecture). It is based on assembling independent and loosely coupled services to build a composed web service. This composition can be described from both a local or a global perspective by respective orchestration or choreography. The validation of web service orchestrations is the main topic of this work. It is based on the verification of two classes of properties: generic and specific properties. The former can be checked for any invoked web services whereas the specific properties are different interdependence relationships between activities within an orchestration process. These properties cannot be directly verified on the orchestration process, so, the authors have to use formal techniques. In this paper, they propose a formal approach for the validation of web service orchestrations. This work adopts WS-BPEL 2.0 as the language to describe the web service orchestration and uses the SPIN model-checker for the verification engine. The WS-BPEL specification is translated into Promela code which is the input language for the SPIN model-checker, in order to check generic and specific properties expressed with LTL (Linear Temporal Logic).

Related Content

Lata Jaywant Sankpal, Suhas H. Patil. © 2022. 23 pages.
Amna Alsalem, Emad Ahmed Abu-Shanab. © 2022. 20 pages.
Bimal aklesh Kumar. © 2022. 12 pages.
Nikola Vlahovic, Andrija Brljak, Mirjana Pejic-Bach. © 2021. 19 pages.
Ahmed Aloui, Okba Kazar. © 2021. 20 pages.
Ilhem Feddaoui, Faîçal Felhi, Fahad Algarni, Jalel Akaichi. © 2021. 22 pages.
Fernando Almeida, José Augusto Monteiro. © 2021. 12 pages.
Body Bottom