=Paper=
{{Paper
|id=Vol-548/paper-1
|storemode=property
|title=Analyzing Orchestration of BPEL Specified Services with Model Checking
|pdfUrl=https://ceur-ws.org/Vol-548/paper1.pdf
|volume=Vol-548
}}
==Analyzing Orchestration of BPEL Specified Services with Model Checking==
https://ceur-ws.org/Vol-548/paper1.pdf
Analyzing Orchestration of BPEL Specified
Services with Model Checking
Joseph C. Okika⋆
Supervised by Prof. Anders P. Ravn
Computer Science Dept. Aalborg University, Aalborg, Denmark
Abstract. This project investigates, implements and evaluates tool sup-
port for analysis of SOA-Based service contracts using Model Checking.
The specification language for the contract is Business Process Execu-
tion Language (BPEL). It captures the behavior of services and allows
developers to compose services without dependence on any particular
implementation technology. A behavior specification is extracted from a
BPEL program for formal analysis. One of the key conditions is that it
reflects the intended semantics for BPEL, and in order to make it com-
prehensible, it is specified in a functional language. The resulting tool
suite is hosted on an Eclipse platform.
1 Research Question and Its Significance
Service Oriented Architectures (SOAs) are applicable when multiple applications
running on varied technologies and platforms need to communicate with each
other. In this way, enterprises can mix and match services to perform business
transactions with less programming effort. However, a service operates under
a contract/agreement which will set expectations, and a particular ontological
standpoint that influences its semantics [14]. Services are first class citizens and
are autonomous as well as distributed in nature. They can be composed to form
higher level services or applications to solve business goals. Of course, this raises
a lot of issues such as managing composed services, monitoring their interac-
tion, analyzing the behavior of interacting services, verifying the functionality
of individual services as well as composed services.
So far, service development has used traditional testing which are inefficient
when dealing with distributed systems. Thus, there is a clear need to employ
and integrate successful analysis techniques like model checking in the design
of support tools for effectively solving these problems as well as in the imple-
mentation of high quality SOA-based services. Therefore, a detailed contractual
description of services and corresponding semantics is of great importance.
BPEL offers a programming model for specifying the orchestration of web
services through several activities. Activities are categorized into two; basic and
⋆
Partially supported by the Nordunet3 project COSoDIS - “Contract-Oriented Soft-
ware Development for Internet Services“. E-mail: ojc@cs.aau.dk
structured. Basic activities (for instance invoke, receive, etc.) define the interac-
tion capabilities of BPEL processes whereas the structured activities are made
up of constructs such as flow (for synchronization), compensate, and pick among
other activities.
Current Results In [4] we have demonstrated a viable solution to the problem
of checking for some functional and behavioural properties of individual services.
This is done through translation of the specifications to timed automata followed
by model checking for relevant properties. In [2] we consider the problem of
consistency across specifications and identified a need to set up a correspondence
between the individual automata. The novel contribution in that paper is to
make such a consistency check practical by translating the automata to CCS,
the input language for the Concurrency Work Bench. As demonstrated by a case
study, this technique is applicable and gives a handle for automating yet another
consistency check for web services.
2 Current knowledge and the existing solutions
In this section, we present several efforts geared toward formalizing/analyzing
services specified using BPEL - one of the most widely used orchestration lan-
guage. The overall observation about these works is that they all deal with three
major issues; semantics definition, mapping to an analysis language and appli-
cability. In Figure 1, δ represents those efforts that cover semantics definition
and mostly applying Petri net simulation while µ represents those that focus on
mapping/translation to an analysis language.
The issue with most of these results is that they cover only fragments of
the language and for some of them, there is not explicit statement about the
underlying analysis language and possibility of automation.
[19, 11, 17, 8]
BP EL SBP EL
δ
µ [5 − −7, 15] ?
X SX
?
Fig. 1. BPEL Formalizations
Abstract state machines are used in [16] to define an abstract operational
semantics for BPEL for version 1.1. The work focuses on formal verification of
service implementations and resolving inconsistencies in the standard. Abouzaid
and Mullins [1] propose a BPEL-based semantics for a new specification lan-
guage based on the π-calculus, which will serve as a reverse mapping to the
π-calculus based semantics introduced by Lucchi and Mazzara [10]. Their map-
ping is implemented in a tool integrating the toolkit HAL and generating BPEL
code from a specification given in the BP-calculus. Unlike in our approach, this
work covers the verification of BPEL specifications through the mappings while
the consistency of the new language and the generated BPEL code is yet to be
considered. As a future work, the authors plan to investigate a two way mapping.
Several model checking approaches have been employed to provide some form
of analysis. An overview of most of the semantics foundation is given in [18]. An
illustrative example which is well-explained is [11]. It deals with specification
of both the abstract model and executable model of BPEL. The approach is
based on Petri nets where a communication graph is generated representing a
process’s external visible behavior. It verifies the simulation between concrete
and abstract behavior by comparing the corresponding communication graphs.
Continuing with Petri net, an algebraic high-level Petri net semantics of BPEL
is presented in [17]. The idea here is to use the Petri patterns of BPEL activities
in model checking certain properties of BPEL process descriptions. The model
is feature complete for BPEL 1.1. Lohmann extends this work with a feature-
complete Petri net semantics for BPEL 2.0 [8].
As there exists several BPEL formalizations including a comprehensive and
rigorously defined mapping of BPEL constructs onto Petri net structures pre-
sented in [19, 13] a detailed comparison and evaluation of Petri Net semantics
for BPEL is presented in [9]. The comparison reveals different modelling deci-
sions with a discussion on their consequences together with an overview of the
different properties that can be verified on the resulting models.
In the case of using labeled transition systems as models for formalizing
BPEL, few efforts is found in the literature which focuses on some fragments of
BPEL constructs. For instance, Geguang et al. present a language µ-BPEL [15]
where a full operational semantics using a labeled transition system is defined
for this language and its constructs to Extended Timed Automata. The language
constructs are mapped to a simplified version of BPEL 1.1. Fu et al. presented
a translation from BPEL to guarded automata in their work [5]; the guarded
automata is further translated into Promela specification which is the language
for the SPIN model. Similar approaches are also followed in [6, 7]. All these
efforts points to the fact that there is an important need for service contracts to
be specified and analyzed.
3 Proposed Ideas
As mentioned in the previous section, many theoretical results have considered
the semantics analysis of BPEL. However, there are several issues around these
semantics. First, there is the issue of coverage - that is to say, is the full BPEL
language covered or some fragments of it? Most of the efforts using automata as
presented in the previous section covers only some fragments of BPEL. A few of
the efforts using Petri net covers a feature-complete BPEL. We point this out
because it is worthwhile to have a comparison with another full coverage in a
different formalism like automata. Second, there is the issue of translation where
one may ask: is it semantic preserving? There is also the third issue of whether
it is manual, semi-automated or automated.
Figure 2 shows the proposed approach; mapping BPEL to timed automata
(TA). This defines a semantics for BPEL with a clear description of what is
included and what is abstracted in the mapping and thus answers the issues
raised above.
BP EL sem
SBP EL
γ◦α
β ?
β γ
γ BP EL U ppAal ST A
U ppAal ST A
given
Fig. 2. The new Approach Fig. 3. Functional Composition
Looking at Figure 2, starting from BPEL, we consider a full behavior of
BPEL syntax and define the semantics based on UppAal, SBP EL . We follow a
functional approach where we define a function β mapping BPEL to UppAal.
We use timed automata for the formal model but with a rendering to UppAal
because it is a mature model checking tool with wider audience and supported
in our research environment. It can be a different choice (for example SPIN) in
another environment. Note that the function given which takes care of the TA
semantics is given with the UppAal tool and it’s transition system semantics.
Composing these two functions as shown in Figure 3 relates BP EL to ST A .
In effect, having defined the function mapping BPEL to UppAal, we achieve
a semantic preserving extraction/translation. That is, taking the inverse of the
function gives us the result.
In [12] we give a classification of service contract specification languages based
on application families and aspects. The classification identifies competing lan-
guages across aspects. It shows where a language may fit into the development of
service based applications as well as the ones that allow for desired analyses, for
instance match of functionality, protocol compatibility or performance match.
In addition, we use the classification to survey analysis approaches. Further-
more, the classification may assist in planning of development activities, where
an application involves services with contracts that span across families. Such
scenarios are to be expected as service oriented applications spread. Another
paper [3] focuses on analyzing behavioral properties for web service contracts
formulated in Business Process Execution Language (BPEL) and Choreography
Description Language (CDL). The key result reported is an automated technique
to check consistency between protocol aspects of the contracts. The contracts
are abstracted to (timed) automata and from there a simulation is set up, which
is checked using automated tools for analyzing networks of finite state processes.
Fig. 4. Plug-in Architecture
4 Contribution to the problem domain and Discussion
The project offers three distinct contributions in the development of analysis and
verification tools for SOA-based services. 1) The technique employed is a rigor-
ous use of the power of functional languages in defining a property preserving
mapping for the full behavior of BPEL. 2) Model checking of behavior properties
of BPEL. General properties such as those related to deadlock and reachability
as well as application specific properties are considered. Eg., services should not
deadlock even with faults and compensation. 3) A prototype Integrated tool.
The supporting tool will allow developers to leverage the already existing IDE
such as Eclipse to design, specify and analyze SOA-based services.
Tool Development: We focus on building a theory based tool that gives devel-
opers of SOA-based services a clear understanding of BPEL processes. We are
implementing the integrated supporting tool as a plug-in in the Eclipse frame-
work. A model (UML) of the various components of the analysis tool is shown
in Figure 4.
Discussion: The main novelty is to solve the issue of semantics unrelated to
analysis tools. This is achieved by defining the extraction function using a func-
tional language. As a side effect to this, we develop a functional XML parser/un-
parser for Standard ML. As this is an ongoing work, further effort will be geared
toward tuning the tool. We plan to build a service based point of sale system
using ActiveVOS orchestration system to demonstrate analysis of properties.
References
1. Faisal Abouzaid and John Mullins. A Calculus for Generation, Verification and Re-
finement of BPEL Specifications. Electron. Notes Theor. Comput. Sci., 200(3):43–
65, 2008.
2. Emilia Cambronero, Joseph C. Okika, and Anders P. Ravn. Analyzing Web Service
Contracts - An Aspect Oriented Approach. In Proceedings of the International
Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies
(UBICOMM’2007), pages 149 – 154. IEEE Computer Society Press, November
2007.
3. Emilia Cambronero, Joseph C. Okika, and Anders P. Ravn. Consistency Checking
of Web Service Contracts. Int’l Journal On Advances in Systems and Measure-
ments, 1(1):29–39, 2008.
4. G. Diaz, J. J. Pardo, M. E. Cambronero, V. Valero, and F. Cuartero. Verification
of Web Services with Timed Automata. In Proceedings of First International
Workshop on Automated Specification and Verification of Web Sites, volume 157,
pages 19–34. Springer Verlags Electronics Notes Theor. Computer Sci. series, 2005.
5. Xiang Fu, Tevfik Bultan, and Jianwen Su. Analysis of interacting BPEL web
services. In WWW ’04: Proceedings of the 13th international conference on World
Wide Web, pages 621–630, New York, NY, USA, 2004. ACM.
6. Xiang Fu, Tevfik Bultan, and Jianwen Su. WSAT: A Tool for Formal Analysis of
Web Services. In Proc. of 16th Int. Conf. on Computer Aided Verification, pages
510–514. Springer, 2004.
7. Xiang Fu, Tevfik Bultan, and Jianwen Su. Synchronizability of conversations
among web services. IEEE Transactions on Software Engineering, 31(12):1042–
1055, December 2005.
8. Niels Lohmann. A feature-complete Petri net semantics for WS-BPEL 2.0.
In Kees van Hee, Wolfgang Reisig, and Karsten Wolf, editors, Proceedings of
the Workshop on Formal Approaches to Business Processes and Web Services
(FABPWS’07), pages 21–35. University of Podlasie, June 2007.
9. Niels Lohmann, H.M.W. Verbeek, Chun Ouyang, and Christian Stahl. Compar-
ing and evaluating Petri net semantics for BPEL. IJBPIM, 2008. (Accepted for
publication).
10. Roberto Lucchi and Manuel Mazzara. A pi-calculus based semantics for WS-BPEL.
J. Log. Algebr. Program., 70(1):96–118, 2007.
11. Axel Martens. Consistency between executable and abstract processes. In EEE
’05: Proceedings of the 2005 IEEE International Conference on e- Technology, e-
Commerce and e-Service (EEE’05) on e-Technology, e-Commerce and e-Service,
pages 60–67, Washington, DC, USA, 2005. IEEE Computer Society.
12. Joseph C. Okika and Anders P. Ravn. Classification of SOA Contract Specification
Languages. Web Services, IEEE International Conference on, 0:433–440, 2008.
13. Chun Ouyang, Eric Verbeek, Wil M. P. van der Aalst, Stephan Breutel, Marlon
Dumas, and Arthur H. M. ter Hofstede. Formal semantics and analysis of control
flow in WS-BPEL. Sci. Comput. Program., 67(2-3):162–198, 2007.
14. R. Perrey and M. Lycett. Service-oriented architecture. Applications and the
Internet Workshops, 2003. Proceedings. 2003 Symposium on, pages 116–119, 2003.
15. Geguang Pu, Xiangpeng Zhao, Shuling Wang, and Zongyan Qiu. Towards the
Semantics and Verification of BPEL4WS. Electr. Notes Theor. Comput. Sci.,
151(2):33–52, 2006.
16. D. Fahland W. Reisig. ASM-based semantics for BPEL: The negative Control
Flow. In Proc. 12th International Workshop on Abstract State Machines, pages
131–151, 2005.
17. Christian Stahl. A Petri Net Semantics for BPEL. Informatik-Berichte 188,
Humboldt-Universitt zu Berlin, July 2005.
18. Frank van Breugel and Maria Koshika. Models and Verification of BPEL, 2005.
http://www.cse.yorku.ca/ franck/research/drafts/tutorial.pdf.
19. M. T. Wynn, H. M. W. Verbeek, Aalst, Ter A. H. M. Hofstede, and D. Edmond.
Business process verification - finally a reality! Business Process Mgmt. Journal,
15(1):74–92.