Information Technology Reference
In-Depth Information
[49], Kongdenfha et al. [50] propose the use of an aspect-oriented
programming (AOP) approach to weave adaptor code into services.
Brogi and Popescu [51] present a method to automatically generate a
mediator between two BPEL services. Nezhad et al. [52,53] propose
an automata-based method to synthesize partial compatible services.
1.3.3 Verification of Service-Based Workflows
The issue of verification is not a new topic in workflow research [54].
However, in an SOA paradigm, this problem has unique features to be
explored. First, the model elements in specifications such as BPEL are
much more complicated than those in traditional workflow specifications
such as XPDL. BPEL concepts such as correlation set, dead path
elimination, compensation, and fault handling are unique, which brings
complexity in verification. Second, because service-based workflows
usually interact with each other bymessage exchange, the correctness of a
workflow relies on not only its internal logic, but also how its partners
collaborate with it. Even if a workflow is correct from a single-process
point of view, its composition with another one may still fail because
these two workflows do not agree on their interactions.
Based on the formal methods used, the researches in this area can be
classified into several categories, that is, Petri net, automata, and
process algebra-based ones.
Petri Net-Based Verification
Ouyang et al. [55] propose a comprehensive Petri net formalism for
various BPEL model elements, including basic activities, structured
activities, event handler, control link, and fault handling. Martens et al.
[56] try to verify the choreography of multiple BPEL processes. Hinz
et al. [57] transform BPEL into Petri nets, and then use CTL (Compu-
tational Tree Logic) and a model-checking tool to verify various
temporal properties.
Automata-Based Verification
Su et al. [58,59] focus on the automaton model for services and apply
model checking via LTL (linear temporal logic). A special contribution
of their research is a technique called synchronizability analysis to
tackle the problem of state space explosion brought about by
Search WWH ::




Custom Search