Formal Verification of WS-BPEL Using Timed Trace Theory

2014 ◽  
Vol 931-932 ◽  
pp. 1452-1456 ◽  
Author(s):  
Wutthipong Kongburan ◽  
Denduang Pradubsuwun

A web service composition is able to create a new service by incorporating some existing web services. Currently, Web Service Business Process Execution Language or WS-BPEL is a promising language used to describe the web service composition. Since in the real world most of business processes have been involved temporal context and they are quite complex interaction, it is impossible to completely eliminate all failures in them. Therefore, a formal verification is required to assure the correctness and reliability of the web service composition. In this paper, timed trace theory has been applied to verify the web service composition with temporal constraints. Both safety and timing failures can be examined. Experimenting with a ticket reservation system, the proposed approach shows its effectiveness.

2009 ◽  
Vol 18 (02) ◽  
pp. 225-260 ◽  
Author(s):  
VALERIA DE CASTRO ◽  
ESPERANZA MARCOS ◽  
ROEL WIERINGA

In recent years, the automation of business processes has become one of the most prominent and promising uses of Web service technology. Consequently several languages have been created for the execution of business processes, making it possible to define new and more complex services or business processes which are implemented for example by means of Web service composition. Nevertheless, these kinds of languages are not suitable for use in the early stages of the development process of information systems. Special methodologies or techniques are therefore necessary to allow systems analysts to understand services from a business point of view, while facilitating the design and development of Web service composition. In this paper, we present a service-oriented approach to information system development that starts by identifying, through business modeling, the services required by the customers of a business, to make it possible to create a Web service composition model. This model will facilitate the transformation to specific languages for business process execution, thereby reducing the development efforts made in service-oriented applications. The method proposed is illustrated by means of a Web application for the management of medical images, which we have taken as a case study.


Author(s):  
W. L. Yeung

Business collaboration is increasingly conducted over the Internet. Trading parties require business-level protocols for enabling their collaborative processes and a number of standardised languages, and approaches have been proposed for specifying business-level protocols. To illustrate the specification of web services based collaborative processes, three inter-related specification languages, namely, the ebXML Business Process Specification Schema (BPSS), the Web Service Business Process Execution Language (WSBPEL), and the Web Services Conversations Language (WSCL) are discussed in this chapter. A contract negotiation protocol is used as an example to illustrate the concepts involved in the specification. The chapter also discusses different strategies for deploying these specification languages.


Web Services ◽  
2019 ◽  
pp. 1530-1550
Author(s):  
Chao-Qun Yuan ◽  
Fang-Fang Chua

Web Service Composition is one of the technologies in Service Oriented Architecture which significantly increases the flexibility and reusability of developing service-oriented system. One of the major problems which occurs in web service composition is the difficulties of maintaining the existing running web service composition solutions due to the changes of business requirements, deployment environment, and other dynamic factors. In this proposed work, an automated system had been built to autonomously execute the web service composition. To achieve this objective, the authors had embedded semantic engine and Prolog in C# program to automatically and dynamically discover, compose and execute web service composition, i.e. a web service composition could be self-configured to automatically recover from execution failure and automatically re-generate composition solution due to business protocol changes.


Sign in / Sign up

Export Citation Format

Share Document