Information Technology Reference
In-Depth Information
asynchronous messaging. Their result shows that, if a composite Web
service is synchronizable, its conversation set remains the same when
asynchronous communication is replaced with synchronous communi-
cation. Thus, a synchronous communication model can be used in LTL
model checking. Kazhamiakin et al. [60] develop a set of parametric
communication models in service composition. These models range
from synchronous communications to asynchronous ones with complex
buffer structures. In addition, they develop a technique to associate a
service composition with the most adequate communication model that
is sufficient to capture all the behaviors of the composition. Using this
model, the analysis before the actual verification can speed up the
verification.
Process Algebra-Based Verification
Process algebra [61] is an algebraic approach to the modeling and
analysis of concurrent processes. Its advantage is that it provides not
only temporal logic model checking, but also bisimulation analysis
through which whether two processes have equivalent behaviors can be
determined. Foster et al. transform BPEL into a kind of process algebra
called a finite state process (FSP), and then use a model checking tool to
verify properties like whether the implementation satisfies the abstract
design specifications [62], whether two services are compatible [63],
and whether the composition of BPEL services satisfies the properties
defined in WS-CDL [64]. A formal BPEL model based on
p
-calculus (a
kind of process algebra based on Calculus of Communicating Systems)
can be found in [65]; a
p
-calculus-based technique to analyze the
behavioral substitution of Web services is proposed in [66].
1.3.4 Decentralized Execution of Workflows
Workflow systems are often built on a client/server architecture in
which a single engine takes the responsibility for the operation of a
whole process. In many circumstances, this sort of centralized systems
may not fully meet the requirements when a workflow is across
organizations or security boundaries. Partitioning an integrated work-
flow into small fragments, each of which is orchestrated by one engine,
is a preliminary requirement for its decentralized execution. A team
from IBM India Research Lab has conducted a series of studies in the
