Contract n° 507953
WP N°10: DBE Test Automation
D10.2: DBE Test Automation Framework
(Formal Foundations)
Project funded by the European
Community under the “Information
Society Technology” Programme
Contract Number: 507953
Project Acronym: DBE
Title: Digital Business Ecosystem
Deliverable N°: D10.2
Due date: 31/10/2006
Delivery Date: 16/02/2007
Short Description:
The purpose of this deliverable is to provide a report on the theoretical framework
that underpins the Test Automation Framework, D10.2, that is now available as a
plug-in for the DBEStudio. The software plug-in constitutes the main part of this
deliverable. However, this report is an important complement to it.
Partners owning: UniS
Partners contributed: UniS
Made available to: public
VERSIONING
VERSION
AUTHOR, ORGANISATION
1.0
YONGYAN ZHENG
2.0
YONGYAN ZHENG, PAUL KRAUSE
Quality check
Internal Reviewer: John Kennedy, Intel
Internal Reviewer: Paul Malone, Waterford Institute of Technology
This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 2.5
License. To view a copy of this license, visit : http://creativecommons.org/licenses/by-nc-sa/2.5/ or
send a letter to Creative Commons, 543 Howard Street, 5th Floor, San Francisco, California, 94105,
USA.
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
Executive Summary
This report describe s the theorectical foundation of the WP10.2 softwre deliverable
’test-case-generator’ plug-in of the DBEStudio. Some of the work presented in this
report has been published in the following papers:
Yongyan Zheng, Jiong Zhou, Paul Krause. A Model Checking based Test Gener-
ation Framework for Web Services. In proc of IEEE ITNG2007.
Yongyan Zheng, Paul Krause. Automata Semantics and Analysis of BPEL. In
proc of IEEE DEST2007.
Yongyan Zheng, Paul Krause. Asynchronous Semantics Anti-patterns for Inter-
acting Web Services. In proc of IEEE QSIC 2006.
1
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
Contents
Nomenclature v
1 Introduction 1
1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.1 Web Service Stack . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.2 The Relationships of BPEL and Others . . . . . . . . . . . . . . 5
1.1.2.1 BPEL and WS-CDL . . . . . . . . . . . . . . . . . . . . 5
1.1.2.2 BPEL and OWL-S . . . . . . . . . . . . . . . . . . . . . 5
1.1.2.3 BPEL and WSDL . . . . . . . . . . . . . . . . . . . . . 6
1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3 Aims and Objective s . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.5 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.6 Report Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2 Literature Review 10
2.1 Formal Semantics and Verification of BPEL based web services . . . . . 10
2.1.1 Petri Nets based approaches . . . . . . . . . . . . . . . . . . . . . 11
2.1.2 Process Algebras based approaches . . . . . . . . . . . . . . . . . 13
2.1.3 Automata based approaches . . . . . . . . . . . . . . . . . . . . . 16
2.1.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Testing of BPEL base d web s ervices . . . . . . . . . . . . . . . . . . . . 18
2.3 Analysis of Data De pendencies in Orchestration . . . . . . . . . . . . . . 19
2.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
i
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
CONTENTS
3 Web Service Automata 23
3.1 Static Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.2 Dynamic Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.3 Composition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.4 Buffering Schemes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.5 Compatibility and Anti-patterns . . . . . . . . . . . . . . . . . . . . . . 37
3.5.1 Compatibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.5.2 Anti-patterns . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4 Analysis of BPEL Features in Web Service Automata 44
4.1 BPEL Control Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.1 Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.2 Concurrency, Fault Propagation, and Interruption . . . . . . . . 46
4.1.3 Synchronization of Activities and Dead-Path-Elimination . . . . 48
4.1.4 Scoping, Compensation and Fault Handling . . . . . . . . . . . . 50
4.1.5 Multiple Threads of Message Event Handlers . . . . . . . . . . . 51
4.2 BPEL Data Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.2.1 Data flow annotation in WSA . . . . . . . . . . . . . . . . . . . . 54
4.2.2 Detailed Analysis of BPEL data handling . . . . . . . . . . . . . 56
4.2.2.1 BPEL internal data exchange model . . . . . . . . . . . 56
4.2.2.2 BPEL external data exchange m odel . . . . . . . . . . . 60
4.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
5 Verification and Test Case Generation of BPEL 64
5.1 Model Checking in Testing . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.2 Test Coverage Criteria in Temporal Logic . . . . . . . . . . . . . . . . . 65
5.3 Test Generation Framework . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.4 Symbolic Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
5.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6 Conclusions and Future Work 75
6.1 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
ii
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
CONTENTS
References 83
iii
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
List of Figures
1.1 Web Service Stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2 UML diagrams and web service specifications . . . . . . . . . . . . . . . 4
2.1 An example of Petri nets for BPEL activities . . . . . . . . . . . . . . . 11
3.1 Message overtaking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.2 Unspecified reception . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.3 An example of anti-pattern 1 . . . . . . . . . . . . . . . . . . . . . . . . 41
3.4 Non-local branching 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.5 An example of anti-patterns 2 and 3 . . . . . . . . . . . . . . . . . . . . 42
3.6 Non-local branching 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.1 An example of machine hierarchy . . . . . . . . . . . . . . . . . . . . . . 46
4.2 Propositional input events and common machine structure . . . . . . . . 47
4.3 linkWrapper machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.4 Scope and Compensation . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.5 EHS and MEH machines . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.6 Unreachable and deadlock activities . . . . . . . . . . . . . . . . . . . . 53
4.7 High level data flow models . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.8 The loanapproval’s partnerLinks . . . . . . . . . . . . . . . . . . . . . . 56
4.9 The BPEL variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.10 An example of BPEL internal data exchanges for variable x and y . . . 58
4.11 The internal data exchange m odel of the loanapproval pro ces s . . . . . . 59
4.12 The loanapproval’s invoke activity . . . . . . . . . . . . . . . . . . . . . 61
4.13 BPEL external data exchange model . . . . . . . . . . . . . . . . . . . . 62
4.14 BPEL internal and external data exchange model . . . . . . . . . . . . . 62
iv
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
LIST OF FIGURES
5.1 Test framework architecture . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.2 An example of WSA code . . . . . . . . . . . . . . . . . . . . . . . . . . 69
5.3 An example of state coverage . . . . . . . . . . . . . . . . . . . . . . . . 71
5.4 An example of predicate handling . . . . . . . . . . . . . . . . . . . . . . 73
v
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
Chapter 1
Introduction
In recent years, Service-Oriented Computing(SOC) has been actively researched. SOC
provides a systematic and extensible framework for application-to-application interac-
tion, built on top of existing web proto c ols and based on open XML standards. It
defines a standardized mechanism to describe, locate, and communicate with online
applications. In a SOC e nvironment, each application becomes an accessible web ser-
vice that is described using open standards. Due to the advantages of open standards,
the SOC paradigm provides a flexible, re-usable, and loosely coupled model for dis-
tributed computing. A SOC offers three main functions: communication protocols,
service descriptions, and service discovery.
In this work we lo ok at the service descriptions, with focus on the verification
and testing of the behavioural aspect of web services. BPEL is the de-facto industry
standard language to model the behaviour of web service compositions. BPEL is a
semi-formal flow-based language with complex features, which may thus include fault
behaviours. It becomes essential to verify a web service design before publishing it,
and to test whether the published service conforms to the design m odel. The manual
writing and verification of test cases for complex models is tedious, time-consuming
and error prone. Hence, it is vital to automate this process. This report provides the
theoretical background to a test-case generation and execution plug-in that has been
developed for the DBEStudio. The plug-inmay be downloaded from the Source-Forge
1
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.1 Background
DBE Project.
1.1 Background
SOC is the emerging paradigm for the realization of heterogeneous, distributed systems,
obtained from the dynamic combination of remote applications owned and operated by
distinct organizations. SOC characterizes a collection of autonomous and self-contained
we b services. The essence of SOC lies in independent web services which communicate
with each other exclusively through messages . No knowledge of the partner service
is shared other than the message formats and the sequences of the messages that are
expected. The agreed-on standards of service description, discovery, and communica-
tion explicitly allow that the partner service may be implemented with heterogeneous
technology, with diverse applications written in different programming languages and
running on different operating systems and hardware.
In the SOC architecture, there are three roles: service provider, service consumer,
and service registry. Service providers can publish their services in a service registry.
Service requesters or consume rs can use the services that are retrieved via the service
registry. A Service registry provides facilities for service providers and consumers to
find each other. A web service can play any or all of these roles.
1.1.1 Web Service Stack
To support the SOC architecture, web services must provide standards-based defini-
tions of interoperability communication protocols, mechanisms for service description,
discovery, and composition as well as quality of se rvice (QoS) protocols. T he web
service stack is shown in Figure 1.1.
The initial trio of web services specifications SOAP, WSDL, and UDDI provides
open XML-based mechanisms for service communication, se rvice desc ription, and ser-
vice discovery.
UDDI (Universal Description, Discovery and Integration) (UDD) provides a stan-
2
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.1 Background
Choreography (WSDL-CDL..)
Orchestration (BPEL, OWL-S..)
WS-
Security
WS-Reliable
Messaging
WS-Transaction
UDDI
WSDL, WS-Policy
XML Schema, SOAP
Business
Processes
Quality of
Service
Discovery
Description
Messaging
HTTP, MQ, SMTP Transport
SBVR
Business
Rules
Figure 1.1: Web Service Stack
dard way for publishing and discovering information about web service.
WSDL (Web service Definition Language) (CCMW01) defines a public interface
of a web service, by describing the functions that can be provided by a web service.
WSDL enables dynamic discovery and binding of compatible services which are
used in conjunction with registry services.
SOAP (Simple Object Access Protocol) (SOA03) is a platform and language
independent communication protocol that defines an XML-based format for web
services to exchange information over HTTP by using remote proc edure calls.
Web services describe their functionality using WSDL and they interact with each
other by exchanging SOAP message s serialized in XML and sent over a transport
protocol, usually HTTP. Moreover, UDDI is used to interconnect service providers and
service consumers. This basic SOC model covers discovery, description, messaging, and
transport layers of the we b service stack in Figure 1.1.
To move beyond this basic model, mechanisms for service composition and QoS
protocols are required. Several specifications have been proposed in these areas:
Business rule layer: SBVR (Semantics of Business Vocabulary and Business Rules
Specification) (OMG06) describes the business rules using the pre-defined busi-
ness vocabulary.
Business process layer: WS-CDL (Web Services Choreography Description Lan-
guage) (KBR04) provides a conversation protocol to describe the global interac-
3
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.1 Background
tions of web services. BPEL (Business Process Execution Language) (ACD
+
03)
and OWL-S (Ontology Web Language for Services) (OWL04) specify service
compositions.
Quality of service layer: WS-Security ensures end-to-end message integrity, con-
fidentiality, and authentication. WS-Reliable Mess aging allows messages to be
delivered reliably between distributed applications in the presence of software
component, system, or network failures. WS-Transaction provides a means to
compose transactional qualities of service.
Description layer: XML Schema describes the data formats used for constructing
the messages addressed to and received from web services. WS-Policy extends
WSDL to all the encoding and attachment of QoS information to services in the
form of reusable s ervice policies.
In order to give an intuitive view of the main web service standard languages, we use
UML diagrams to link SBVR, WS-CDL, BPEL, and WSDL. In Figure 1.2, SBVR has
a similar role as UML use case diagrams to capture the business requirement; WS-CDL
is similar to UML collaboration or sequence diagrams to model the global web service
interactions; BPEL has a similar role as UML statecharts to model local web service
interactions and the stateful behaviour of individual web services; finally, WSDL has
similarities with UML c lass diagrams to describe we b service interfaces.
Use Case Diagrams
Collaboration /Sequence Diagrams
Statecharts
Class Diagrams
UML Diagrams
SBVR
WS-CDL
BPEL
WSDL
Web Services
Figure 1.2: UML diagrams and web se rvice specifications
4
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.1 Background
1.1.2 The Relationships of BPEL and Others
Since our work is focused on BPEL, in order to clarify the BPEL p os ition in the web
service stack, we will discuss the relationships between BPEL and WS-CDL, BPEL
and OWL-S, as well as BPEL and WSDL .
1.1.2.1 BPEL and WS-CDL
Two main approaches are currently investigated for static service composition. The
first approach, referred to as web service orchestration (e.g. BPEL), combines available
services by adding a central coordinator that is responsible for invoking and combining
the web services. The second approach, referred to as web service choreographer (e.g.
WS-CDL), does not assume the exploitation of a central coordinator but rather it
defines the c onversation that should be undertaken by each participant. The aim is to
model the peer-to-p e er interactions am ong the collaborating services.
Briefly speaking, BPEL aims to model the interactions of web services with re-
spect to a central coordinator, while WS-CDL is in a layer above BPEL to provide a
conversation protocol for the global interaction of web services.
1.1.2.2 BPEL and OWL-S
Both BPEL and OWL-S are workflow languages for modeling business processes com-
posed of a set of service invocations. The structure defines the partial order of invo-
cation of the services and their interactions. BPEL, as an industrial standard, aims to
provide rich control flow structures to integrate existing web services in a flexible way.
BPEL supports exception handling and compensations, while OWL-S does not define
recovery protocols. Also, BPEL provides more mature execution engines. OWL-S, as
one of the standards in the Semantic Web community, aims at fully automating all
stages of the web services lifecycle. By using OWL-S, AI planning techniques can be
used to automate the service composition.
Therefore, BPEL supports static service composition, with a focus on representing
composition where information flow and the binding between services are known in
5
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.2 Motivation
advance. OWL-S supports dynamic service composition, with focus on modelling the
preconditions and post-conditions of the process so that the evolution of the domain
can be logically inferred. It relies on ontologies to formalize the domain concepts which
are shared among services. The research groups of Standford University and Carnegie
Melon University have led the work in adapting BPEL for semantic web such as OWL-S.
1.1.2.3 BPEL and WSDL
BPEL has close relationships with WSDL. Interactions with services are modelled as
partnerLinks. A partnerLink has a partnerLinkType, which defines which WSDL port-
Type is used in a relationship with some partner and which portType is used when a
partner interacts with the process itself. The BPEL process is exposed as a service
and therefore has its own WSDL interface. These two relationships are defined in the
partnerRole and myRole attributes of the partnerLinkType.
For a composite service mo delled by process workflow languages such as BPEL or
OWL-S. WSDL defines the data types of the service w hich are used directly in the
process. WSDL uses messages to define and carry data types. In a BPEL process, a
variable is defined to carry a data type, which is declared in WSDL.
1.2 Motivation
The recent years has seen a rapid growth in the development of web services tech-
nology. However, some issues such as the compos ability, compatibility, conformance
and substitutability, correctness, and coordination of service compositions are not yet
thoroughly investigated. For instance, conformance and correctness should be checked
to find errors as early as possible in the workflow design phase.
BPEL activity relationships can be categorized into control-flow and data-flow.
Since BPEL is a semi-formal flow language, various formal semantics have be en pro-
posed, so that BPEL models can be verified rigorously. However, most current formal
models only focus on m odelling BPEL control flow, and do not cover the BPEL data
6
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.3 Aims and Objectives
flow analysis.
There exists two kinds of interactions of BPEL: internal and external. T he external
interactions between BPEL models are by message pass ing. The internal interactions
between activities of a BPEL model are by data sharing. Most existing work ignores
the internal interactions of BPEL activities.
In the literature, there is les s effort in using behavioural web service models (e.g.
BPEL models) as the test models for deriving test case s. To our knowledge, none
of the prior research studies the verification and test case generation of both BPEL
control-flows and data-flows in a unified approach.
1.3 Aims and Objectives
The objectives of this work will be:
To design a formal model that can cover most features of the BPEL, and cover
BPEL internal and external interactions.
To demonstrate that it is essential to separate verification and testing of BPEL
control flow and data flow.
To show that it is suitable to apply model checking as the test generation engine
to generate test cases from BPEL models.
To demonstrate that the test it is feasible to apply model checking as the test
generation engine for BPEL based web services.
1.4 Methodology
Existing model checking tools can be reused for the purpose of verification and testing
of BPEL. Our formal model is intended to be used by such verification tools. With
model checking, a BPEL model can not only be a design model for verification, but
also be a test model for deriving test cases. The formal semantics proposed to date
7
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.5 Contributions
for BPEL can be categorized as process algebra based, Petri-net based, and automata
based. We follow the automata-based approach, in order to facilitate the use of model
checking tools. We propose a Web Service Automaton (WSA), an extension of Mealy
machines, which covers data, supports message passing communication, and adapts
the asynchronous interleaving semantics. We justify the suitability of WSA for BPEL
on three counts. First, its propositional input events capture most features of the
BPEL language, while most automata-based formal models for BPEL only cover the
core subset features of BPEL. Second, its message passing communication provides a
uniform semantics for both BPEL internal and external interactions. Third, our model
supports the separate analyses of BPEL control and data flows.
Based on WSA, we provide a model checking based test case generation framework
for BPEL. We support application of both SPIN and NuSMV model checkers as the
test generation engines, and we encode the conventional structural test coverage criteria
into LTL and CTL temporal logic. State coverage, transition coverage, and predicate
coverage are used for BPEL control flow testing, and all-du-path coverage is used for
BPEL data flow testing. Two levels of test cases can be generated to test whether the
implementation of web services conforms to the BPEL behaviour and WSDL interface
models. The generated test cases are executed on the JUnit test execution engine.
1.5 Contributions
Our theoretical contribution is to propose a formal model to formalize BPEL semantics.
This formalization enables us to reason about properties of BPEL processes such as their
incorrectness and compatibility. Our practical contribution is to provide an automatic
verification and test case generation framework for BPEL and WSDL. The key benefits
of our approach are:
1) The propositional input events of our formal model can capture most features of
BPEL language (including exception handling and compensation handling), and
also can reduce unnecessary machine state space.
8
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
1.6 Report Structure
2) The explicit data handling of our formal model enables separating control flow
testing and data flow testing of BPEL.
3) The message passing communication me chanism of our formal model provides a
uniform semantics for BPEL internal and external interactions.
4) The test framework can automatically generate BPEL based test cases and WSDL
based test cases.
5) Demonstration that model checking is an effective means to automatically gener-
ate test cases in the web service domain.
1.6 Report Structure
Chapter 1 introduces background information and key concepts of web services. Chap-
ter 2 gives a review of relevant literature. Chapter 3 presents our formal model, its
static and dynamic semantics, and discusses the model compatibility. Chapter 4 pro-
vides detailed analysis of BPEL features in our formal model. Chapter 5 outlines our
automatic verification and test case generation framework. Chapter 6 summarizes the
thesis with conclusions and potential future work.
9
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
Chapter 2
Literature Review
An extensive literature of related work on the formal semantics and verification of
process models. In order to maintain the focus of this rep ort, we concentrate on the
verification and tes ting of B PEL based web service models in this chapter. The aim of
this section is not to thoroughly compare the existing approaches, but to point out the
motivation of our proposed work by reviewing related work.
2.1 Formal Semantics and Verification of BPEL based
web services
To a service composer, it is desirable to be able to verify that the composition is well-
formed. For example, that it does not contain any deadlock or livelocks which would
cause the composition to not terminate under certain conditions. It is possible to verify
these properties using formal notations and existing verification tools. The verification
tools have the advantage that they allow one to simulate and verify the behaviour of
one’s model at design time, thus enabling the detection and correction of errors as early
as possible. As such, the model verification phase helps increas e the reliability of web
services. The works of (MM04; HS04) provide good reviews for the current verification
approaches.
10
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
2.1.1 Petri Nets based approaches
A Petri net (Pet62) N = (P, T, F ) consists of places P nodes, transitions T nodes,
and flow relation F as directed arcs to connect places with transitions. The current
state of a Petri net is represented by a set of black tokens distributed over the places.
The places from which an arc runs to (resp. from) a transition is called the input places
(resp. output places) of the transition, respectively. A transition is enabled if all of its
input places contain tokens. An enabled transition fires by removing the tokens from its
input places and adds a specified number of tokens into each of its output places. One
can map BPEL based web services to Petri nets by assigning activities to transitions
and process states to places. Fig 2.1 shows an example of petri nets modelling BPEL
activities (OvdAB
+
05).
Figure 2.1: An example of Petri nets for BPEL activities
Each BPEL activity is associated with a Petri net with an input place r
i
and
an output place f
i
. The place r
i
,s
i
,c
i
, and f
i
denotes states ready, started (run-
ning),completed, and finished, respectively. Transitions are of three types. The first
type, denoted as unlabelled bars, is auxiliary transition. The solid bars denotes a transi-
tion to m odel internal actions for checking pre-conditions or evaluating post-conditions
for activities; and the other bars are used to implement composite constructs. The
other types are denoted as labelled boxes. The second type is substitution transition,
which is abstract representation of subnets for the enclosed BPEL activities. The third
11
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
type is activity transition to model the events or actions of a BPEL activity. On the
left of the figure, the petri net models a BPEL basic activity X. If X is to receive a
message m, the transition labelled with X can be replaced by ?m. On the right of the
figure, the petri net models a BPEL flow activity, when the flow is started, subnets
A, B will be executed, and the flow completes after A, B are completed.
In a standard Petri net, tokens are indistinguishable. In a Colored Petri nets (CP-
net) (Jen97), every token has a value. CP-nets extend Petri nets with the primitives
for defining data types (color) and the manipulations of data values, thus a CP-net is
more concise than a Petri net. Transition eligibility depends then on the availability of
an appropriately coloured token in all the input places of this transition. Likewise, the
output of a transition is not just a token but a specifically coloured token.
Web service algebra is proposed in (HB03) to define a s et of web service composition
operators. The authors use Petri nets as the formal semantics for the proposed web
service algebra. The works of (OvdAB
+
05; Sta05) present Petri net semantics for
the control flow of BPEL, with consideration of BPEL advanced features such as fault
handling, event handling, and compensation handling. In (Sta05), the tool BPEL2PN
is developed to map BPEL co de to Petri nets, and model checker LoLA (Sch00) is
used to verify CTL temporal logic. The author of (LMSW06) extends (Sta05) to use
Petri net to capture the global interactions between BPEL processes. In (OvdAB
+
05),
the tool BPEL2PNML is developed to map BPEL to Petri ne ts, and a verification tool
WofBPEL is used as the analysis engine. The paper discusses how to verify the activity
reachability and some pre-defined BPEL constraints. As a summary, the above works
abstract from data. As shown in our motivation example, it is important to consider
BPEL data dependencies.
In (YTYL05), they claim to capture both BPEL control and data dependencies in
CP-nets, and CPN tools (CPN) can be used to verify the process. However, the paper
only shows how to map a core subset of BPEL to CP-nets. There is no discussion
of how to capture BPEL data dependencies, and no concern of modelling faults or
compensations. They summarize a set of properties of CP-nets to be checked and
12
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
their corresponding meaning in the verification of web se rvice com position, including
boundness, deadlock-freedom, liveness, fairness, home, and reachability.
In (YK04), they use CP-nets to model the process composition models, and apply
CPN tools as the verification engine. BPEL skeleton code can be generated from the
process composition model. In the CP-nets models, messages (events) and process
variables are represented by tokens. Abstract colour sets are declared for the mess ages
and variables such that each colour set is kept small to speed up the analysis. They also
an algorithm to automatically derive the conversation protocol, which is also CP-net
based, from the process composition models. The conversation protocol in their context
only models the interactions between the service consumer and the service provider,
and hides the internal process details such as provide data manipulation and interaction
with other service partners. Instead of verifying the BPEL proce ss , their work focus
on designing a correct CP-net based model and generate BPEL skeleton process.
Petri net provide the constructions for specifying synchronization of concurrent
processes. Petri net adopts interleaving semantics for concurrency, and synchronous
communication. As a distributed computing paradigm, web services communicate by
message passing, so it is more suitable to adopt asynchronous communication by mes-
sage passing for inter web service interactions. Also, in Petri-nets, every transition is
restricted to model a single event, which will heavily increase the model state space.
2.1.2 Process Algebras based approaches
Process algebraic service composition aims to introduce much simpler descriptions than
other approaches. The underlying semantic foundation is based on labelled transition
systems, i.e. automata. Many variants have been defined and the field come s with
a rich body of literature. The most well-known process algebras are CCS (Mil89),
CSP (Hoa85), and LOTOS (BB87), and Pi-calculus (MPW92).
Pi-calculus extends CCS with mobile-ability, in which the basic entity is a process
- it can be an empty process a choice between several I/O operations and their contin-
uations; a parallel composition; a recursive definition, or a recursive invocation. I/O
13
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
operations can be input (receive) or output (send). For example, x(y) denotes receiv-
ing tuple y on channel x; ¯x[y] denotes sending tuple y on channel x. Dotted notation
specifies an action sequence. Parallel process composition is denoted with A|B. Several
processes can execute in parallel and communicate using c ompatible channels. Describ-
ing services in s uch an abstract way lets us reason about the composition’s correctness.
One can treat relevant properties by assigning behavioural types to processes. There
are at least two possible ways to type processes:
In the first case, one can type only port subsets. We can proscribe the type or
shape of data that can be exchanged via two ports. This would create additional
message limitations. For a two processes that can exchange any kind of message ,
if we type the messages (ports), we could limit the exchange.
In the second case, one can type the entire process. When the entire process is
typed, the type notion becomes a homomorphic image of the process. In many
such systems, process and type are synonyms.
With process algebras semantics for web services, the general question is what
information to type. Typing too little can make it impossible to verify some properties.
On the other hand, typing too much creates a complexity that renders verification
unusable or impractical.
In (Fer04), a two-way mapping is defined between BPEL and LOTOS, and model
checking toolbox CADP (FGK
+
96) is used as the verification engine. The mapping
from LOTOS to BPEL does not preserve the structure of a process, due to the expressive
and flexible structure of LOTOS. The disabling operator is used to capture the BPEL
interruptions. In LOTOS, the processes communicate synchronously by rendezvous.
In (FUMK03), the process algebra FSP (Finite State Processe) (MK99) is used
for the BPEL semantics and the model checker LTSA (MK99) as the verification
engine. The web service composition specification is modelled in MSC (Message Se-
quence Chart), and the implementation is modelled in BPEL. Both MSC models and
BPEL proce sse s are translated into FSPs, such that the BPEL implementation can
14
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
be verified against the MSC specification by trace equivalence checking. The work
(FUMK04; FUMK06) extends the earlier work to verify the interacting BPEL pro-
cesses and checks their compatibility. A tool LTSA-WS was implemented as an Eclipse
plug-in. FSP is abstract from data, so their mapping does not cover BPEL data de-
pendencies. Also, FSP supports synchronous communication.
In (XLP06), they use Pi-calculus as the BPEL formal model and NuSMV model
checker as the verification engine. A tool OPAL is developed to automate the mapping
from BPEL to Pi-calculus, and from Pi-calculus the input language SMV of the NuSMV
model checker. It points out that there exist two approaches to model check Pi-calculus.
One is to analyze Pi-calculus processes based on proof system, and the other is to
transform Pi-calculus into automata. The authors follow the sec ond approach. They
model a shared variable x of BPEL as a shared storage register Reg(x), where the
stored value can be read from or written to Reg(x).
In (WPSW04), they propose a language named CDL to extend WSDL to m odel the
behavioural of individual web s ervices , and propose a composition language which can
support both centralized or distributed orchestration. The formal semantics of these
two languages are based on Pi-calculus. They point out that the use of shared variables
in BPEL makes it difficult to coordinate the execution in a distributed manner. Their
composition language has two core concepts: a task and a process. A task is equal to a
BPEL activity. For inter-task dependency, they explicitly consider control dependencies
and data dependencies. The review of web service data dependency modelling will be
covered in section . They point out that the current tools support for verifying of Pi-
calculus is inmature. Most do not support the complete language and require a complex
and error prone input syntax. A solution is to map Pi-calculus to the input languages
of mature model checkers such as SPIN. Since the input languages of most mature
model checkers are automaton-based, we b elieve an automaton-based formal model is
more suitable to map to those input languages. There are other works use Pi-calculus
as the formal semantics for the orchestration language (GLSC06; ML06; DMCS05).
In the above Process Algebra approaches, they consider both the core BPEL ac-
15
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
tivities and the advanced BPEL features with fault handling, compensation handling,
and event handling.
2.1.3 Automata based approaches
Automata or labelled transition systems are a well-known model underlying formal
specifications of systems. An automaton is a mathematical model for a finite state
machine FSM. An FSM is a machine that, given an input symbols, transfers through
a series of states according to a transition function. A Mealy machine is a FSM that
generates an output based on its current state and an input. The transitions will include
both an input and output signal. In contrast, a Moore machine is a FSM that only
depends on the machine’s current state, transitions having no input signal. For each
Mealy machine there is an equivalent Moore machine, and vice versa. Mealy machine is
commonly used, and there exist a variety of models extends Mealy machine with data,
hierarchy, or time .
In (WFN04), BPEL models are mapped into deterministic finite state automata
for the matchmaking of web service composition. The STSs(State Transition Systems)
are used in (PTBM05) to b e the BPEL formal semantics, and a tool is developed as
a part of the ASTRO toolset (AST). Both of these formal models are abstracted from
data.
In (FBS05), they propose guarded automata (GA) to be the formal models for
both BPEL and the conversation protocol. GA extends Mealy machine with data, and
eve ry transition is equipped with a guard in the form of an XPath expression. The
model checker SPIN is used as the verification engine. BPEL processes communicate
by sending asynchronous messages, and each process has a queue. A global watcher
kee ps track of all messages. The c onversation is introduced as a sequence of messages.
They propose a set of sufficient conditions so that asynchronous communication can be
replaced with synchronous communication. A tool WSAT is developed to map BPEL
to guarded automata, and map guarded automata to Promela (the input language
of SPIN). In their approach, each BPEL activity is mapped to a GA, so the BPEL
16
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.1 Formal Semantics and Verification of BPEL based web services
process as a whole is a composition of a set of GAs. The interleaving semantics of
concurrency is used. However, they omit the inter activity data dependencies. Also, in
their models, the GAs representing BPEL processe s communicate by message passing,
but it is not clear how the GAs representing the BPEL activities communicate. In
our formal model, we believe it is clearer from the theoretical view to provide a single
communication mechanism for both external and internal interactions, where machines
communicate by either message passing or by data sharing, but not both. In their
mapping from GA to Promela, the XPath expressions in the GA transition guards are
also translated into Promela, so that the data manipulation can be verified. We believe
this will decrease the speed of model checkers, and symbolic transition guards can reach
the same verification result. We will discuss it in section .
Similar as (FBS05), the author of (Nak05) transform BPEL into EFA (Extended
Finite State Automata). A tool is developed to automate the mappings from BPEL
to EFA, and from EFA to Promela. EFA extends Mealy machine with data, and it
adopts asynchronous interleaving semantics of concurrency. They also has no concern
of the interaction among BPEL activities due to data dependencies. It is not clear
which communication mechanism is used when modelling read and write data by BPEL
activities.
In the above automata based approaches, they only cover core subset of BPEL
activities and do not consider fault handling, compensation handling, or event handling.
2.1.4 Summary
For a large system of concurrently executing services, a crucial aspect of the correctness
of such system is their temporal behaviour.
Both Petri nets and process algebras are precise and well-studied formalisms that
allow automatic verification of certain properties of their behaviours. Likewise, they
provide a rich theory on bi-simulation analysis, one can establish whether two processes
have equivalent behaviours. Such analyses are useful to establish whether a service can
substitute another service in a composition or to verify the redundancy of a service.
17
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.2 Testing of BPEL based web services
Process algebra approaches have the advantage that the composition operators of pro-
cess algebras are convenient in capturing the semantics of BPEL structured activities,
and they support simulation and bi-simulation analysis, which are useful for model
substitution and refinement. However, for the purpose of verification and testing, the
automaton formalism is especially attractive due to the straight usage of mo del check-
ing tools. The model s ubstitution and refinement is not the focus of our test framework.
Therefore, we have investigated the usability of automata approaches.
The problem of the promising pi-calculus based approaches is that it offers typing
for order and format of messages. The limitation of Petri-net based approaches is the
single e vent restriction on every transition, w hich will easily cause large model state
space. Most Petri bet based and pro ce ss algebraic models can handle compensations
and exception handling, but this remains to be seen for the automata based models.
Our automata based formal model need to fill this gap.
In summary, in order to solve some of the current problems, it is essential to design
a formal m odel which fulfils the following requirements: 1) the formal model should
be able to fill the gap of current automata based approaches to capture not only the
basic BPEL features but also the advanced BPEL features to model fault handling,
eve nt handling, and compensation handling. 2) the formal model should be able to
capture both control dependencies and data dependencies between BPEL activities. 3)
the formal model should reduce state space for model checking. 4) the mapping from
the formal model to the input language of model checkers should contain abstraction
to speed up the model checking.
2.2 Testing of BPEL based web services
As we c an see from the previous section, there are intensive research on providing precise
semantics for BPEL and verification of correctness of BPEL models. However, there
is less effort in using BPEL as the test models for deriving test cases. A framework is
proposed in (BP05a) to augment WSDL with a UML2.0 PSM (Process State Machine)
18
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.3 Analysis of Data Dependencies in Orchestration
for modelling the web service interactions. After transforming PSM to a Symbolic
Transition System, existing ioco-conformance testing tools can be applied. In (HM05),
they use Graph Transformation Rules along with WSDL to generate test cases. WSDL-
S is proposed in (SP06) to be the service behaviour model, which e xtends WSDL by
adding a pre-condition and post-condition to each WSDL operation. The WSDL-S is
mapped to EFSM so that the existing test techniques for EFSM can be applied.
For the purpose of providing an automated test case generation and execution en-
vironment, our test framework should allow users to choose test c riteria in an easy
way. Test case generation techniques can be categorized as test purpose oriented and
coverage oriented. Test purpose oriented techniques allow testers to define interest-
ing scenarios as test purposes, but the testers need to have knowledge to encode test
purposes into temporal logic formulas for model checkers. Instead, coverage oriented
techniques release testers from writing temporal logic formula manually. So we target
at coverage oriented test generation. It is not new to apply model checking to achieve
test coverage (HCL
+
03; HGW04; RH01), but it is new to apply such a technique in
the domain of web services.
2.3 Analysis of Data Dependencies in Orchestration
Referring to the works discussed in section , many works abstract from data and di-
rected the attention to the control flow. When data is omitted, the transition guards
and variables were left out, so selecting one of two control pathes, solved by the eval-
uation of data, needs to be modelled by a nondeterministic choice. Even for those
works considering BPEL data, they do not consider modelling data dependencies in
an explicitly way. In this section, we review the works with consideration of modelling
data dependencies in the orches tration m odels such as BPEL models. The purpose of
analyzing data dependencies is to e nsure data is always defined before being used.
In (PA03), they propose a BioOPera Flow language to model the control depen-
dencies and data dependencies between tasks (BPEL activities) as visual flow graphs.
19
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.3 Analysis of Data Dependencies in Orchestration
In order to maintain the consistency, they provide a set of constraints when construct-
ing a data flow graph. For instance in a process data flow graph, data always flows
from output to input parameters of tasks. The input parameters of a process can only
be connected to input parameters of tasks, and output parameters of the process may
receive data only from output parameters of tasks. A constant data can be connected
to multiple input parameters, but an input parameters bound to a constant data can-
not have any other incoming data flow edge. A toolset is developed to support the
visualization. Even though their focus is not rigorous verification of design models,
they shows the importance of considering control dependencies and data dependencies
in separation.
In the composition language proposed by (
WPSW04), each task (equally to a
BPEL activity) has inputDependencies section to describe the control dependencies
and data dependencies from itself to other tasks. For instance, variable x is the output
data of task tk
1
and the input data of task tk
2
, tk
2
will declare a data dependency
in its input-Dependencies section to specify tk
1
is the source who sends x to it. The
task who receives a message from an external web service will se nd the message to
other ’downstream’ tasks w hich have dependencies on this message. Their com position
language is mapped to Pi-calculus. In Pi-calculus, a process denotes web service task,
channels represent takes data dependencies, and control dependencies are represented
implicitly using the operators of Pi-calculus directly. The composition service as a whole
is modelled as a parallel composition of all of these processes. Their data dependency
modelling makes the data definition and usage clear. With this in mind, our proposed
formal model should also be able to capture the data dependencies between BPEL
activities in an e xplicit way.
A grid workflow language is proposed in (FQH05), where each activity may have
data-in port and data-out port. The data exchange describes that the data flows
from data-out ports to data-in ports. They discuss the constraints added on the data
exchanges in conditional activities (e.g. BPEL switch activities and pick activities), in
sequential loop activities (e.g. BPEL while activities), and in parallel loop activities
20
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.3 Analysis of Data Dependencies in Orchestration
(e.g. BPEL flow activities).
The authors in (APS05) provide a mo del of data flow in addition to control flow
for OWL-S process models. They transform OWL-S to Promela so that SPIN model
checker can be used to verify the OWL-S process model. Their scope of the data flow
is limited to within a composite process. The processes in a composite process can
exchange data among themselves or with the parent process. Here an OWL-S process
has the same role as a BPEL activity. T he control flow features of OWL-S are a lot
simpler than BPEL. We will add similar level-based constraint on the data exchanges
within a BPEL process, and the rationale of adding this c onstraint will be covered in
section 4.
For external data exchanges between orchestration models, if there is a conversation
protocol available, the data dependencies between web services can be directly derived
from the conversation protocol; otherwise, one need to analyze the data exchanges
to get the data dependencies. The work of (BP05b) discusses how to analyze data
exchanges between YAWL workflow models, so that the resulted data dependencies
between web services can be used for service matching. In (DMCS05), they propose a
OWL-P language to model both the conversation protocol as well as the orchestration
models. When composing orchestration models, the designer needs to define a set
of composittion axioms to add constrains on the conversation protocol. A data-flow
axiom states the data exchange dependency among the orchestration models. In our
test framework, we do not assume a conversation protocol is available to guide the
communications between BPEL models, so data dependencies between BPEL models
need to be analyzed.
In (MPT06), they propose data nets to capture data exchange and data manip-
ulation within an orchestration model, as well as data exchange between composition
models. The control flow of a orchestration model is modelled by STS (State Transition
System) (PTBM05). STS with data is the synchnonized product of all the STSs and
data nets. A tool is needed to do the experimental evaluation. Since we assume our
formal model includes data, there is no need to add a seperate data model. Data flow
21
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
2.4 Summary
can be derived from our formal model based on existing data flow analysis techniques.
In sum up, it is necessary to model data exchange explicitly in our formal model,
to capture the data dependencies within a BPEL model and the data dependencies
between BPEL mo dels in a correct way.
2.4 Summary
In this section, we review the formal models for BPEL including Petri-nets, Process
Algebra, and automata; the verification approaches based on these formal models; the
testing approaches of deriving test cases from web service behavioural models; and the
approaches of analyzing data dependencies internal and external to an orchestration
model. We discuss the motivation to propose a formal model, and the required features
of the formal model. Thereafter, we present the reason to design and develop an auto-
mated test generation framework. Moreover, we point out the importance of analyzing
data aspect of BPEL models.
22
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
Chapter 3
Web Service Automata
WSA provides a formal description of the legal protocol for web service interaction,
and following some translation step it can be used as a reference model for test case
derivation, applying we established algorithms from formal test theory.
In WSA, each message is represented by a channel. Unique names for channels
corresponding to each message type are assumed.
3.1 Static Semantics
The static semantics of a web service automaton extends finite state machine with sig-
nature, data structure, and message storage schema. The dynamic semantics of a web
service automaton includes machine configurations and execution traces. The formal
definitions are given below.
Definition 1. We assume that we have available an enumerable infinite set V of
variables and sets AX,BX of assignment expressions and Boolean expressions respec-
tively, together with a set D of values. We also assume that we have a set of functions
Env where Env : V D assigns variables of V with values from D. Given an
expression exp, we need three functions:
def : AX V , where def(exp) V returns the assigned variable, i.e. the
23
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.1 Static Semantics
variable on the left hand side of the assignment.
cuses : AX (V ), where (V ) is the power set of V and cuses(exp) V
returns the variables on the right hand side of the assignment.
puses : BX (V ), where puses(exp) V returns the variables in the Boolean
expression.
If exp AX, we need a function apply
A
: AX × Env Env that satisfies:
If v 6= def(exp) then apply
A
(exp, (v)) = (v). This means only the assigned
variable may change.
If for all v cuses(exp) we have
1
(v) =
2
(v), then apply
A
(exp,
1
(v)) =
apply
A
(exp,
2
(v)).
If for all Env we have apply
A
(exp
1
, ) = apply
A
(exp
2
, ), then exp
1
= exp
2
.
If exp BX, we need a function apply
G
: BX × Env {true, f alse} that sat-
isfies: if for all v puses(exp) we have
1
(v) =
2
(v), then appl y
G
(exp,
1
(v)) =
apply
G
(exp,
2
(v)).
Each web service automaton M will be assoc iated with certain variables and ex-
pressions. These constitute its data structure. A formal definition of a machine’s data
structure is given in definition 2.
Definition 2. A Web Service Automaton (WSA) M is a finite state machine,
consisting of W SA
M
= (I
M
, S
M
, s
M
0
, S
M
f
, T
M
, δ
M
). As a convention, we omit the su-
perscript of M such that M = (I, S, s
0
, S
f
, T, δ), and the components of M inherit
subscripts, superscripts, or dashes.
1) I is the signature of M , denoted as a three tuple I = (E, L, O), where E, L, O are
pair-wise disjoint and represent a se t of input events, internal events, and output
eve nts, respectively. Let Msg = (L E O) to be the set of events, we refer
to the elements of L = L
in
L
out
as internal input events and internal output
eve nts, and to those of M sg = (E O) as external events.
24
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.1 Static Semantics
2) S is a set of states, s
0
S is the initial state, S
f
S is a set of final states.
3) T IN ×BX×((AX)OUT ) is a set of transitions, where IN = (EL
in
{})
and O U T = (O L
out
{}). For each t = (m, g, a) T (graphically denoted
as m[g]/a), m IN is a set of triggering events, g BX is the guard predicate,
and a ((AX) OUT ) is the action set composed of assignments and output
eve nts. indicates the omission of an event. We would represent a transition by
Ω[g]/ which simply determines a state change and nothing else. The elements
of transition t are denoted as t.m = m, t.g = g, t.a = a.
The events of the transition input event set t.m IN are linked by logi-
cal ope rator conjunction, disjunction, or negation, denoted as AND : e
1
e
2
, .., e
n
, OR : e
1
e
2
, .., e
n
, and NOT : ¬(e
i
), respectively.
The data structure of machine M is the form of (V
M
, AX
M
, BX
M
), which
can be retrieved from T . Since T IN × BX × ((AX) OUT ), we can
retrieve AX
M
= {exp AX|∃t T exp t.a}, BX
M
= {exp BX|∃t
T exp t.g}, and V
M
which is the disjoin union of
S
expAX
({def(exp)}
cuses(exp)) and
S
expBX
{puses(exp)}.
We define that a WSA is T -complete iff t T then s
t
s
0
, which means
eve ry transition will be triggered from some state.
4) δ S × T × S is the transition relation.
We use symbols !, ?, @ as a convention in diagrams to indicate whether an event
is input, output, or internal event, denoted as !e E, ?e O, @e L, respectively.
Conversely, going from the formal des cription to a diagram, !, ?, @ are introduced de-
pending on membership of E, O, L. For instance if M sends a message m to M
0
, then
in the composite automaton (definition 10), !m and ?m will b ec ome @!m and @?m to
indicate that output event !m and input event ?m become internal output and internal
input events, respectively.
25
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.2 Dynamic Semantics
Definition 3. A WSA is deterministic iff s, s
0
, s
00
S.t T , s
t
s
0
s
t
s
00
s
0
= s
00
holds.
Definition 4. We define a message x to be a pair of send and receive events (!x, ?x).
If machine M
1
sends message x to machine M
2
, then !x O
1
?x E
2
.
3.2 Dynamic Semantics
We have defined the static structure of a WSA. We now explain its dynamic semantics.
We assume, first of all, that a WSA is equipped with a means of storing incoming
messages. Instead of limiting the buffers to a particular type such as FIFO or multi-
set, we consider different buffering schemes (s ec tion 3.4). We as sume that each WSA is
associated with a finite buffer. The buffer β(E L
in
) stores the external and internal
input events. In one step of the WSA, either: 1) a message e is received from the
environment e E, and added to the buffer β(E L
in
); or 2) an enabled transition
fires, possible causing a state change and change to the values of some variables v V
M
.
In order to precisely define a step, we need to formalise the notion of a configuration
η which records the current state, the current values of the variables associated with
M and the current content of the buffer.
A transition t is enabled in a configuration η, when 1) its triggering event set t.m
is either empty or belonging to β(E L
in
), 2) t.m can be consumed according to the
machine’s buffering scheme, a nd 3) the transition guard t.g is evaluated to be true.
When a transition t is enabled, a set of actions t.a is executed, and the state machine
moves from the start state to the end state of t. Such transition is called enabled
transition.
A machine is associated with a set of events, and an event may have multiple event
occurrences. When considering a machine’s dynamic behaviour, we need to distin-
guish event occurrences from events. Similarly, a message sent between machines may
have multiple message instances, and message instances also need to be distinguished
26
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.2 Dynamic Semantics
from messages. We define a function λ : Ins C to map class instances Ins to classes
C. 1) When applying λ to event occurrences and events, λ(o) = e returns the event
e for an event occurrence o. For an enabled transition t, if ?x t.m then we say t
corresponds to the event occurrence o
i
with λ(o
i
) =?x. 2) When applying λ to message
instances and messages, for a message instance om = (!om, ?om), there exists message
m = (!m, ?m) such that λ(!om) =!m and λ(?om) =?m.
Definition 5. A configuration of a machine M is of the form η = (s, B, ), where
s S, B β(E L
in
) is the current buffer content, and function : V D assigns
the variable of V with a value from D. The set of configurations of M is denoted as
confs(M ) where η confs(M). Note that we ass ume the buffer is empty when M
is either in the initial state or in a final state (hypothesis 1), so η
0
= (s
0
, ,
0
) and
η
n
= (s
n
, ,
n
) are the initial and a final configuration, respectively.
Hypothesis 1. The buffer is empty when machine M is in a final state. If M is
in a final state, we s ay a lifecycle of the machine ends. If the buffer is not empty then
the remaining messages will be discarded because they cannot be c onsumed within this
lifecycle.
Definition 6. A step is a triple (η, x, η
0
) confs(M) × (T E L
in
) × confs(M ).
A step η 7→
x
η
0
changes machine M from configuration η to configuration η
0
in the
following forms:
1) If x E L
in
, representing the case when a message x is arriving and is added
to the buffer B, then (s, B, ) 7→
x
(s
0
, B
0
,
0
) iff s = s
0
, =
0
, B
0
= B + {x}.
2) If x = t T , representing the case when either the message is already in the
buffer t.m B or there is no triggering event associated with t, then (s, B, ) 7→
t
(s
0
, B
0
,
0
) iff t is an enabled transition, i.e. (s, t, s
0
) δ, B
0
= (B \ {t.m} + (t.a
L
in
), apply
G
(t.g, ) = true.
27
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
Definition 7. We define a set of configuration sequences of M as configs(M, η
0
).
A configuration sequence of M ,α = hη
0
, x
0
, .., η
n
)i configs(M, η
0
), is a sequence of
configurations linked by input events,internal input events, or enabled transitions from
the initial configuration to a final configuration, where η
i
= (s
i
, B
i
,
i
), x E L
in
T .
1) We define a set of transition sequences as trans(M ), where a transition se -
quence of M is a sequence of enabled transitions trans(α) = hx
0
, .., x
n1
i such
that trans(M ) = {trans(α)}, where x
i
T, α = hη
0
, x
0
, .., η
n
i configs(M, η
0
),
and trans(η
0
) = {}.
2) We define the set of traces as trances(M ). A trace of machine M is a non-
empty sequence of external event occurrences ho
1
, .., o
n
i, such that trace(M) =
{ho
1
, .., o
n
i}, where for all enabled transitions trans(M) , λ(o
i
) t.m E or
λ(o
i
) t.a O 6= holds.
Definition 8. Let SReach(M) = {s S|∃α traces(M).s
0
α
s} be the set of
states reachable from the initial state of M , and let T Reach(M) = {t T |∃s
SReach(M), s
0
S.s
t
s
0
} be the set of reachable transitions. So a machine M is
fully reachable iff SReach(M) = S T Reach(M ) = T .
3.3 Composition
In order for our notion of composition to be commutative and associative, we intro-
duce the unordered Cartesian product (definition 9). The commutative property is
easy to obtain based on the unordered Cartesian product, but the associative property
requires further constraints on the individual WSAs. We define a general composite
automaton with an interleaving s em antics (definition 10). Such composite automaton
is not guarantee to be a WSA (definition 11). We then elicit a set of constraints on
the individual WSAs as the necessary, sufficient, or necessary and sufficient conditions
for a composite automaton to be a WSA or to be a deterministic WSA. For strongly
composable WSAs (definition 12), we prove that the buffer content of the composite
28
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
automaton is a unique pair, the configurations as well as configuration sequences of
individual WSAs can be projec ted from the composite automaton, and we also prove
that the composition operator is associative.
Definition 9. If (X
i
)
iI
is an indexed family of sets, we define
Q
iI
X
i
to be the
set of all functions ω : I
S
iI
X
i
satisfying ω(i) X
i
for each i I. We refer
to
Q
iI
X
i
as the unordered Cartesian product of a set of X
i
. Note that
Q
is a
commutative and associative binary operator.
Definition 10. If M
1
, M
2
are WSAs, then we define their Composite Automa-
ton
ˆ
M = M
1
k M
2
to be the structure
ˆ
M = (
ˆ
I,
ˆ
S, ˆs
0
,
ˆ
S
f
,
ˆ
T ,
ˆ
δ), where
1)
ˆ
I = (
ˆ
E,
ˆ
L,
ˆ
O), we define com
12
to be the common messages of M
1
, M
2
by com
12
=
(E
1
O
2
) (E
2
O
1
). Now we can define
ˆ
I by
ˆ
E = (E
1
E
2
) \ com
12
,
ˆ
L =
E
1
E
2
com
12
, and
ˆ
O = (O
1
O
2
) \ com
12
.
2)
ˆ
S = S
1
Q
S
2
.
3) ˆs
0
= {s
1
0
}
Q
{s
2
0
}.
4)
ˆ
S
f
= {S
1
f
}
Q
{S
2
f
}. A state of M
1
k M
2
, .., k M
n
is final if, for all machines, the
local state s
i
of M
i
is final.
5)
ˆ
T = T
1
T
2
. Note we assume that v V
i
is a local variable of machine M
i
,
where V
i
= {v V |∃exp AX
i
BX
i
}. This means that there are no shared
variable between t T
i
and t T
j
where i 6= j.
6)
ˆ
δ
ˆ
S ×
ˆ
T ×
ˆ
S. If t T
1
then (s
1
i
, s
2
i
)
t
(s
1
j
, s
2
j
) s
2
i
= s
2
j
s
1
i
t
s
1
j
,
similarly if t T
2
then (s
1
i
, s
2
i
)
t
(s
1
j
, s
2
j
) s
1
i
= s
1
j
s
2
i
t
s
2
j
. If follows
from the asynchronous interleaving semantics that a transition of the composite
automaton is either from M or M
0
but not from both machines.
Definition 11. M
1
, M
2
are composable iff M sg
1
M sg
2
= com
12
(E
1
E
2
) (L
1
L
2
) (O
1
O
2
).
29
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
Definition 12. M
1
, M
2
are strongly composable iff a) Msg
1
Msg
2
= com
12
,
and b) T
1
T
2
= .
Theorem 1.
ˆ
M = M
1
k M
2
are WSAs iff Msg
1
Msg
2
= com
12
(E
1
E
2
)
(L
1
L
2
) (O
1
O
2
) (1).
Proof. Expanding Msg
1
M sg
2
, we get Msg
1
M sg
2
= com
12
(E
1
L
2
) (L
1
E
2
) (O
1
L
2
) (O
2
L
1
) (E
1
E
2
) (L
1
L
2
) (O
1
O
2
) (2). Suppose that
ˆ
M
is a WSA, by lemma 1
ˆ
E = (E
1
L
2
)(E
2
L
1
) \ com
12
= , and based on set theory
A \ B = A B, we have (E
1
L
2
) (E
2
L
1
) com
12
. Similarly, we can get
(O
1
L
2
) (O
2
L
1
) com
12
. This results (1).
Next, we need to prove if (1) holds then
ˆ
M is a WSA. If (1) holds, from (2) we c an
deduce (E
1
L
2
)(E
2
L
1
)(O
1
L
2
)(O
2
L
1
) com
12
(E
1
E
2
)(L
1
L
2
)(O
1
O
2
)
(3) . If m (E
1
L
2
) (E2
L
1
) then m / com
12
where com
12
= (E
1
O
2
) (E
2
O
1
),
because of the pair-wise disjoint O
i
L
i
= . So from (3) we can derive (E
1
L
2
)
(E
2
L
1
) (E
1
E
2
) (L
1
L
2
) (O
1
O
2
). By (1) of lemma 1, we have E L
(E
1
E
2
) (L
1
L
2
) (O
1
O
2
) \ com
12
.Based on the pair-wise disjoint of E
i
, L
i
, O
i
, if
m
ˆ
E
ˆ
L = (E
1
L
2
)(E
2
L
1
)\com
12
then m / (E
1
E
2
)(L
1
L
2
)(O
1
O
2
)\com
12
.
So we have
ˆ
E
ˆ
L ((E
1
E
2
) (L
1
L
2
) (O
1
O
2
)) = . Based on set theory
A B = A B A = , we have
ˆ
E
ˆ
L = . Similarly,
ˆ
O
ˆ
L = holds.
Thereafter, by (3) of lem ma 1, we have
ˆ
O
ˆ
L = . This indicates that the internal
messages of a machine are pair-wise disjoint with the external messages of the partner
machine, i.e. E
i
L
j
= and O
i
L
j
= where i 6= j.
Finally, we need to show that
ˆ
M = M
1
k M
2
is T-complete. For a transition t
ˆ
T ,
without loss of generality, we may suppose that t
ˆ
T , then since M
1
is T-complete,
there exists s
1
, s
0
1
, s such that s
1
tT
1
s
0
1
, which results (s
1
, s
2
)
t
ˆ
T
(s
0
1
, s
2
). Therefore,
ˆ
M is T-complete.
Corollary 1. Suppose that M
1
, M
2
are WSAs and
ˆ
M = M
1
k M
2
, if (E
1
E
2
) =
30
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
(L
1
L
2
) = (O
1
O
2
) (1), then
ˆ
M is a WSA.
Proof. From the proof of theorem 1 we have E L (E
1
E
2
) (L
1
L
2
) (O
1
O
2
) \ com
12
, if(1) holds then
ˆ
E
ˆ
L = . Similarly,
ˆ
O
ˆ
L = holds, and by lemma 1
ˆ
E
ˆ
O = holds.
Lemma 2. If
ˆ
M = M
1
k M
2
is deterministic, then M
1
and M
2
are deterministic.
Proof. We use
i
(resp. ˆ) to denote a transition of M
i
(resp.
ˆ
M. For t
ˆ
T , suppse
t T
1
we have s
1
1
s
0
1
s
1
1
s
00
1
, then (s
1
, s
2
) ˆ(s
0
1
, s
2
) (s
1
, s
2
) ˆ(s
00
1
, s
2
). If
ˆ
M
is deterministic, we must have s
0
1
= s
00
1
. Hence M
1
is deterministic; likewise M
2
is
deterministic.
Lemma 3. Suppose M
1
, M
2
are WSAs and
ˆ
M = M
1
k M
2
, if (1)M
1
, M
2
are de-
terministic and (2) T
1
T
2
= , then
ˆ
M is deterministic.
Proof. For t
ˆ
T ,(s
1
, s
2
) ˆ(s
0
1
, s
0
2
) (s
1
, s
2
) ˆ(s
00
1
, s
00
2
). Suppose that T
1
T
2
= (2),
in the case of t T
1
, we must have s
1
1
s
0
1
s
1
1
s
00
1
and s
2
= s
0
2
= s
00
2
, but then
s
0
1 = s
00
1 by deterministic of M
1
(1), so (s
0
1
, s
0
2
) = (s
00
1
, s
00
2
.The case t T
2
is similar. We
have proved that if M
1
, M
2
are deterministic and T
1
T
2
= , then
ˆ
M is deterministic.
The case T
1
T
2
6= is slightly trickier and we merely include it for completeness .
We define a transition t to be self-loop in machine M , written as t self(M), iff for
all s, s
0
S
M
, if s
t
s
0
then s = s;.
Proposition 1. Suppose M
1
, M
2
are WSAs,
ˆ
M = M
1
k M
2
is deterministic iff (1)
M
1
, M
2
are deterministic, (2) T
1
T
2
self(M
1
) self (M
2
).
Proof. Suppose (2) holds and (s
1
, s
2
) ˆ(s
0
1
, s
0
2
) (s
1
, s
2
) ˆ(s
00
1
, s
00
2
). If t T
1
\ T
2
or
t T
2
\ T
1
, then (s
0
1
, s
0
2
) = (s
00
1
, s
00
2
) by argument perceived of lemma 3. So we only need
to consider the case in which t T
1
T
2
, by (2) we get t self(M
1
) self(M
2
). Hence
(s1, s2) = (s
0
1
, s
0
2
) = (s
00
1
, s
00
2
),
ˆ
M is deterministic.
31
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
Next we consider the converse. Suppose that
ˆ
M is deterministic and t T
1
T
2
,
by T-completeness there exists s1, s
0
1
, s2, s
0
2
such that s
i
i
s
0
i where i = 1, 2, we
have (s
1
, s
2
) ˆ(s
0
1
, s
2
) (s
1
, s
2
) ˆ(s
1
, s
0
2
). Since
ˆ
M is deterministic, we have (s
0
1
, s
2
) =
(s
1
, s
0
2
). Because s
1
, s
0
1
are arbitrary, we can conclude that t self(M
1
). We can get
t self(M
2
) similarly. Hence, we prove that t self(M
1
) self (M
2
).
Theorem 2. Suppose M
1
, M
2
are WSAs,
ˆ
M = M
1
k M
2
is a deterministic WSA
iff
(1) M
1
and M
2
are deterministic;
(2) Msg
1
Msg
2
= com
12
(E
1
E
2
) (L
1
L
2
) (O
1
O
2
);
(3) t self(M
1
) self (M
2
).
Proof. If
ˆ
M = M
1
k M
2
is a deterministic WSA, then (1) is proved by lemma 2, (1)
is proved by theorem 1, and (3) is proved by prop osition 1. Conversely, the condition
(2) proves that
ˆ
M is a WSA following theorem 1; and the condition (1) and (3) proves
that
ˆ
M is deterministic following proposition 1.
Proposition 2. If M
1
, M
2
are strongly composable, then
(1) (E
1
E
2
) (L
1
L
2
) (O
1
O
2
) = ;
(2) M
1
, M
2
are composable;
(3) If M
1
, M
2
are deterministic then
ˆ
M = M
1
k M
2
is also deterministic.
Proof. From definition 12, if M
1
, M
2
are strongly composable then Msg
1
Msg
2
=
com
12
. From theorem 1 we have Msg
1
Msg
2
= com
12
(E
1
E
2
)(L
1
L
2
)(O
1
O
2
)
and com
12
((E
1
E
2
)(L
1
L
2
)(O
1
O
2
)) 6= because of pair-wise disjoint property
of E
i
, L
i
, O
i
. Hence we can prove that (1) holds. (2) holds following corollary 1. By
definition 12 and lemma 3, (3) can be proved.
32
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
Lemma 4. Suppose M
1
, M
2
are strongly composable, let
ˆ
M = M
1
k M
2
and B
β(
ˆ
E
ˆ
L), then there exists a unique pair B
1
β(E
1
L
1
) and B
2
β(E
2
L
2
) such
that B
1
B
2
= B and B
1
B
2
= , i.e.B = B
1
+ B
2
.
Proof. Let B
i
(m) =
B
i
(m) m E
i
L
i
0 otherwise
, we shall show that (E
1
L
1
)(E
2
L
2
)
(1), from this it follows B
1
B
2
= so that a message m
1
implies m / B
2
. For (1),
we have com
12
((E
1
E
2
) (L
1
L
2
) (O
1
O
2
)) = . Based on the pair-wise
disjoint prop e rty of E
i
, L
i
, O
i
, the proof of theorem 1 shows that E
i
L
j
= and
O
i
L
j
= where i 6= j. From proposition 2, if M
1
, M
2
are strongly composable then
(E
1
E
2
) (L
1
L
2
) (O
1
O
2
) = , so we can prove that (1) holds as claimed.
Lemma 5. Suppose M
1
, M
2
are s trongly composable, let
ˆ
M = M
1
k M
2
and η
Conf(
ˆ
M), then project
i
(η) Conf(M
i
) where project
i
(ˆs,
ˆ
B, ˆ) = (s
i
, project
i
(
ˆ
B,
ˆ
|V
i
), ,
i.e. project
i
(η) = η
i
.
Proof. By lemma 4 we have project
i
(
ˆ
B) β(E
i
L
i
), it follows that the configura-
tion of individual automaton η
i
can be projected from the configuration of composite
automaton η Conf(
ˆ
M) by project
i
(η).
Lemma 6. Suppose that M
1
and M
2
are strongly composable, let
ˆ
M = M
1
k M
2
,
then α configs(
ˆ
M project
i
(α) conf igs(M
i
)) (1).
Proof. Since both trans(
ˆ
M) and traces(
ˆ
M) can be retrieved from configs(
ˆ
M), it is
sufficient to prove (1) holds. Based on definition 8, we need η 7→
x
η
0
to represent a step
between configurations.
First, when x
ˆ
E, we have η 7→
x
η
0
iff 1) In the case of x E
1
\
ˆ
L,project
1
(η) 7→
x
project
1
(η
0
) and project
2
(η) = project
2
(η
0
). By lemma 4 it follows x
ˆ
E η
1
7→
x
η
0
1
η
2
= η
2
. From definition 8 it follows that the conditions s
1
= s
0
1
,B
0
1
= B
1
+ x, and
1
=
0
1
holds for η
1
7→
x
η
0
1
. 2) In the case of x E
2
\
ˆ
L,project
2
(η) 7→
x
project
2
(η
0
)
and project
1
(η) = project
1
(η
0
). Similar to 1), we can get x
ˆ
E η
2
7→
x
η
0
2
η
1
= η
1
,
and the conditions s
2
= s
0
2
,B
0
2
= B
2
+ x, and
2
=
0
2
holds for η
2
7→
x
η
0
2
.
33
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.3 Composition
Second, when t
ˆ
T , we have η 7→
x
η
0
iff 1) In the case of x T
1
, project
1
(η) 7→
x
project
1
(η
0
) and project
2
(η) 7→
x.aE
2
project
2
(η
0
). By lemma 5, it follows x T
1
η
1
7→
x
η
0
1
and η
2
7→
x.aE
2
η
0
2
. 2) Similarly, in the case of x T
2
, project
2
(η) 7→
x
project
2
(η
0
) and project
1
(η) 7→
x.aE
1
project
1
(η
0
). By lemma 5, it follows x T
2
η
2
7→
x
η
0
2
and η
1
7→
x.aE
1
η
0
1
.
As a result, for projection on transition and messages, we have project
i
(x
0
, .., x
n1
) =
project
i
(x0), .., pr oject
i
(x
n1
). If x
i
T
1
E
1
\
ˆ
L then project
1
(xi) = x
i
. If x
i
T
2
then project
1
(x
i
) = t.a E
1
.
Lemma 7. The composition operator is communtative. Suppose M
1
, M
2
are WSAs,
M
1
k M
2
= M
2
k M
2
.
Proof. Given M
A
= M
1
k M
2
= (I
A
, S
A
, s
A
0
, S
A
f
, T
A
, δ
A
) and M
B
= M
2
k M
1
=
(I
B
, S
B
, s
B
0
, S
B
f
, T
B
, δ
A
), following the definition of web service automaton, the e le-
ments of M
1
are symmetrical with the elements of M
2
. For instance, E
A
= (E
1
E
2
) \
com
12
= E
B
. Following the commutative nature of the set operators
Q
, we can
prove I
A
= I
B
, s
A
0
= s
B
0
, s
A
f
= s
B
f
, T
A
= T
B
and δ
A
= δ
B
. Hence M
1
k M
2
= M
2
k M
2
is proved as claimed.
Lemma 8. The composition operator is associative. Suppose M
1
, M
2
, M
3
are WSAs,
(M
1
k M
2
) k M
3
= M
1
k (M
2
k M
3
).
Proof. Suppose M
A
= (M
1
k M
2
) k M
3
= (I
A
, S
A
, s
A
0
, S
A
f
, T
A
, δ
A
) and M
B
= M
1
k
(M
2
k M
3
) = (I
B
, S
B
, s
B
0
, S
B
f
, T
B
, δ
B
), following the commutative nature of the set
operators
Q
, we can prove s
A
0
= s
B
0
, s
A
f
= s
B
f
, T
A
= T
B
and δ
A
= δ
B
. We can
derive I
A
= I
B
from E
A
= E
B
,L
A
= L
B
, and O
A
= O
B
. In the following, we let
E = E
A
E
B
E
C
, L = L
A
L
B
L
C
, O = O
A
O
B
O
C
, and X = X
12
X
13
X
23
where X
12
= com
12
,X
13
= com
13
, and X
23
= com
23
.
First, we need to prove E
A
= E
B
.
Let E
a
= E
1k2
E
3
and X
a
= (E
1k2
O
3
)(O
1k2
E
3
), where E
1k2
= (E
1
E
2
)
¯
X
12
and O
1k2
= (O
1
O
2
)
¯
X
12
. We have E
A
= E
a
¯
X
a
(1). From (1), we can
34
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.4 Buffering Schemes
derive E
a
= E(
¯
X
12
E
3
) (2), X
a
=
¯
X
12
(X
13
X
23
) and
¯
X
a
= X
12
(
¯
X
13
¯
X
23
)
(3). From (2)(3), E
A
= E ((E
3
X
12
)
¯
X (E
3
(
¯
X X
12
)) (4) can be derive d.
By proposition 2, E
i
, E
j
are pair-wise disjoint, we have E
3
X
12
(5). From (4)(5)
it results E
A
= E (
¯
X (E
3
¯
X)) = E
¯
X.
Similarly, let E
b
= E
2k3
E
1
and X
b
= (E
2k3
O
1
) (O
2k3
E
1
), where E
2k3
=
(E
2
E
3
)
¯
X
23
and O
2k3
= (O
2
O
3
)
¯
X
23
. We have E
B
= E
b
¯
X
b
(6).
From (6), we can derive E
b
= E (
¯
X
23
E
1
) (7), X
b
=
¯
X
23
(X
12
X
13
) and
¯
X
b
= X
23
(
¯
X
12
¯
X
13
) (8). From (7)(8), E
B
= E((E
1
X
23
)
¯
X(E
1
(
¯
XX
23
))
can be derived. Since E
i
, E
j
are pairwise disjoint, we have E
1
X
23
= , such
that E
B
= E (
¯
X (E
1
¯
X)) = E
¯
X. So E
A
= E
B
is proved.
Second, because O is symmetrical to E, we have O
A
= O
B
= (O
¯
X) as claimed.
Third, we need to prove L
A
= L
B
. By L
A
= (L
1k2
L
3
)(E
1k2
O
3
)(O
1k2
E
3
) and
L
1k2
= L
1
L
2
X
1k2
, we have L
A
= LX
1k2
X
a
where X
a
= (E
1k2
O
3
)(O
1k2
E
3
)
(9). By (3)(9), L
A
= L X
1k2
X
1k3
X
2k3
= L X can be derived.
Similarly, by L
B
= (L
2k3
L
1
)(E
2k3
O
1
)(O
2k3
E
1
) and L
2k3
= L
2
L
3
X
2k3
,
we have L
B
= L X
2k3
X
b
(10), where Xb = (E
2k3
1
) (O
2k3
E
1
). By (8)(10),
L
A
= L X
1k3
X
2k3
= L X can be derived. Therefore, L
A
= L
B
is proved as
claimed.
3.4 Buffering Schemes
Since there is more than one reasonable buffering mechanism, the buffering scheme of
WSA should be flexible and configurable. Inspired by Alur (AHP96), we identify the
commonly used buffering s chemes:
1) FIFO buffering scheme: A machine has one FIFO buffer. The CFSM (BZ83)
and the guarded automata (FBS05) apply this scheme. No message overtaking
is allowed. A message can be consumed only when it is at the head of the FIFO
buffer.
35
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.4 Buffering Schemes
2) Multi-set (definition 13) buffering schemes: a) Multi-set buffer with FIFO sub-
buffers: A machine has one multi-set buffer that consists of FIFO sub-buffers,
where each FIFO sub-buffer corresponds to a message type. A message can be
consumed when it is at the head of each FIFO sub-buffer. b) Multi-set buffer
without sub-buffers: A machine has one multi-set buffer. A message can be
consumed as long as it is in the buffer. For those messages of the same type,
the machine will randomly consume a message in the buffer. c) Multi-set buffer
with multi-set sub-buffers: A machine has one multi-set buffer that consists of
multi-set sub-buffers, where each multi-set sub-buffer corresponds to a message
type. The machine consumes messages in the same way as of b).
Definition 13. A finite multi-set is formally defined as a pair (X, n), where X
is some set and n : X N is a function from X to the set N of natural numbers.
A multi-set differs from a set in that each element has a multiplicity. For instance,
{a, b, b, c, b, a} is a multiset, and the multiplicities are n(a) = 2, n(b) = 3, n(c) = 1,
respectively. The usual set operations such as union, intersection, and sum can be
generalized for multisets.
Note that without loss of generality, we assume the communication channels are lossless,
so that every message is always received after it is sent. Message overtaking may occur
during communication, Figure 3.1 shows two types of message ove rtaking in MSCs.
M1 M2
!ox
!oy
?ox
?oy
type 1
M1 M2
!ox1
!ox2
?ox1
?ox2
type 1
Figure 3.1: Message overtaking
For type 1, suppose messages x = (!x, ?x) and y = (!y, ?y), there exist message
instances ox = (!ox, ?ox) and oy = (!oy, ?oy) where λ(ox) = x and λ(oy) = y, re-
spectively. Message overtaking happens when the order of receive event occurrences
36
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.5 Compatibility and Anti-patterns
?ox, ?oy is diffe rent from the order of send event occurrences !ox, !oy. For type 2,
suppose message x = (!x, ?x), there exist message instances ox
1
= (!ox
1
, ?ox
1
) and
ox
2
= (!ox
2
, ?ox
2
) where λ(ox
1
) = λ(ox
2
) = x. Message overtaking happens when the
order of receive event occurrences ?ox
1
, ?ox
2
is different from the order of send event
occurrences !ox1, !ox2.
We assume that WSA with both FIFO and multi-set buffering schemes only allow
type 1) but not type 2) of message overtaking.
3.5 Compatibility and Anti-patterns
In this section, we define syntax and semantic compatibility. Since syntax compat-
ibility is easy to check from machine interfaces, we focus on checking the semantic
compatibility by checking the individual machines against anti-patterns.
3.5.1 Compatibility
After selecting a set of candidate WSAs, we need to check whether the WSAs can inter-
act properly as expected. Syntactic compatibility involves checking machine interfaces
for the matching external events. Semantic compatibility means checking the machine
behaviours for the absence of pathologies.
Definition 14. Two WSAs M
1
, M
2
are syntactic all y compatible if M
1
sends a
message x to M
2
, then there e xists x = (!x, ?x) such that !x O
1
and ?x E
2
.
Definition 15. Two WSAs M
1
, M
2
are semantically compatible if a) they are
strongly composable, and b) trans(M
1
k M
2
) 6= .
Now we discuss when the condition trans(M
1
k M
2
) 6= holds. This condition holds
iff for any ˆη = ((s
1
0
, s
2
0
), B, (
1
0
,
2
0
)) there is no transition t
ˆ
T such that ˆη 7→
t
ˆ
η
0
,
where (
1
0
,
2
0
) denotes the initial values of variables. First, suppose the initial con-
37
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.5 Compatibility and Anti-patterns
figuration is ˆη
0
= ((s
1
0
, s
2
0
), B, (
1
0
,
2
0
)), if B β(
ˆ
E) then there exists α such that
ˆη
0
7→
α
ˆη
B
= ((s
1
0
, s
2
0
), B + α, (
1
0
,
2
0
)), where α consists solely of external input events,
i.e. α
ˆ
E. Second, from definition 10, it shows (s
1
i
, s
2
i
)
t
(s
1
j
, s
2
j
) iff a) if t T
1
then
s
2
i
= s
2
j
s
1
i
t
s
1
j
, or b) if t T
2
then s
1
i
= s
1
j
s
2
i
t
s
2
j
. ˆη
B
7→
tT
1
η
1
B
7→
tT
1
or η
2
B
7→
tT
2
. Here η
i
B
= (s
i
0
, proj
i
(B),
i
0
), and proj is the projection operator.
Without loss of generality suppose ˆη 7→
tT
2
ˆ
η
0
, we have s
1
0
tT
1
s
1
1
, t.m B, and
apply
G
(t.g,
1
) = true. Conversely, we have ¬( ˆη
B
7→
tT
1
) iff for all B either ¬(s
1
0
tT
1
),
t.m /
ˆ
E, or appl y
G
(t.g,
1
) 6= true.
As a result, condition trans(M
1
k M
2
) 6= holds iff for B β(
ˆ
E), there does
not exist t
ˆ
T such that ˆη
B
7→
t
, which indicates that no transition is possible after
receiving as many as external inputs.
3.5.2 Anti-patterns
According to definition 15, the condition trans(M
1
k M
2
) 6= can be checked only
after constructing the composite WSA. This indicates that a thorough semantic com-
patibility checking has to be done by exploring the whole state space of the composite
automaton. Howe ver we can speed up the model checking, if some obviously incom-
patible behaviours can b e identified by only checking individual WSAs. We propose
anti-patterns for such obviously incompatible behaviours. As a complementary ap-
proach to post-checking, we provide warnings so that the problematic WSA can b e
either re-selected or modified in the earliest s tages . Furthermore, since a WSA’s local
ordering (definition 18) only needs to be computed once, the loc al ordering can be
re-used for pre-checking the compatibility with other machines. After pre-checking,
post-checking can be applied to thoroughly check the composite automaton for safety
and liveness properties.
Referring to the event occurrences and message instances discussed in section 3.2,
the anti-patterns discuss the temporal relations over event occurrences in traces of
individual machines. We follow the standard definitions of strict partial order and
mutually exclusive relation in set theory (e.g. (Wik07)).
38
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.5 Compatibility and Anti-patterns
Definition 16. In a machine M, suppose e, e
0
M sg
M
, the strict partial order over
eve nt occurrences o
1
< o
2
where λ(o
1
) = e, λ(o
2
) = e
0
indicates that o
1
happens be-
fore o
2
in a configuration sequence of M.
Corollary 1. Suppose there is a message m from machine M
1
to M
2
, if we have
a message instance om = (!om, ?om) where λ(!om) =!m and λ(?om) =?m, then the
strict partial order over an event occurrence pair !om <?om enforces that a mes sage
instance must be received after it is sent.
Definition 17. In machine M, suppose e, e
0
Msg
M
, the mutually exclusive relation
on event occurrences o
1
]o
2
where λ(o
1
) = e, λ(o
2
) = e
0
indicates that o
1
is branch-
conflict with o
2
in a configuration sequence of M . Intuitively, two branch-conflict
eve nt occurrences cannot happen in the same trace.
Definition 18. The local ordering on machine M
i
is a structure l
i
= (C
i
, <
i
, ]
i
),
where C
i
is the event occurrence set of E
i
O
i
, <
i
and ]
i
are the strict partial order
and the mutual exclusion relations on C
i
, respectively.
Definition 19. For machines {M
1
, .., M
n
}, we define message orderings to be the
structure <
X
=
S
λ(!om)(?om)X
(!om <?om), where om = (!om, ?om), X
S
1i,jn
com
ij
is the set of message s sent between machines {M
1
, .., M
n
}, and < is the strict partial
order on event occurrence pairs.
Definition 20. The causal ordering for a set of machines {M
1
, .., M
n
} is the struc-
ture
C
= (
S
1in
l
i
) <
X
, which describes the transitive closure of the set of local
orderings and message orderings.
Definition 21. A machine M is said to be blocking iff there exists a state s / S
f
and
a trace α traces(M) such that s
0
α
s and ¬(s
t
) for t T . Referring to definition
39
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.5 Compatibility and Anti-patterns
8, let S
d
be the set of all blocking states,S
d
= {s SReach(M) \ S
f
: t T.¬(s
t
)},
so M is blocking iff S
d
6= .
In state machine diagrams, an initial state is pointed by an arrow started with a filled
black circle, and a final state is shaded. For the anti-patterns, we suppose for two
messages x = (!x, ?x) and y = (!y, ?y) sent between machines M
1
and M
2
, there exist
message instances ox = (!ox, ?ox) and oy = (!oy, ?oy) of x and y, respectively, such
that λ(!ox) =!x and λ(!oy) =!y. Message Sequence Charts(MSCs) are used to show
the anti-pattern scenarios. In the examples, we introduce index k to identify a message
instance of a message, denoted as oe[k] = (!oe[k], ?oe[k]). The index k can be omitted
when there is only one message instance.
Anti-Pattern 1. Suppose !x O
1
, ?x E
2
and !y O
2
, ?y E
1
, M
1
k M
2
has
unspecified reception if ?oy <
1
!ox and ?ox <
2
!oy (1).
M1 M2
!ox
?oy
?ox
!oy
!ox
?ox
?oy
!oy
!oy
?oy
?ox
!ox
Figure 3.2: Unspecified reception
Figure 3.2 shows the corresponding MSC on the left and the causal ordering on the
right. Machine M
1
sends message instance ox to machine M
2
, and M
2
sends message
instance oy to M
1
. M
1
cannot send ox until it receives oy, while M
2
cannot send
oy until it receives ox (1). Based on message ordering and (1), the causal ordering
c
consists of !ox <?ox <!oy <?oy and !oy <?oy <!ox <?ox. This conflict indicates
that M
1
, M
2
wait for message instances from each other but never get them. Hence ,
M
1
k M
2
has an unspecified reception, where the blocking state sets of both machines
are not empty.
40
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.5 Compatibility and Anti-patterns
C1
C4
C2
[g2]
?e2[g1]
/!e1
MC
B1
B3
B4
B2
?e1[g1]
MB
?e1[g2]
/!e2
/!e2
?e1
?e1
?e3
Figure 3.3: An example of anti-pattern 1
Figure 3.3 illustrates an example. traces(M
B
) is composed of h?oe
1
[1], ?oe
1
[2], !oe
2
i
and h?oe
1
[1], !oe
2
, ?oe
1
[2]i. tr aces(M
C
) is composed of h!oe
1
[1], ?oe
2
, !oe
1
[2]i, h!oe
1
[1], ?oe
2
, ?oe
3
i,
h!oe
1
[1]i, and h?oe
3
i. The partial order ?oe
1
[2] <
B
!oe
2
and ?oe
2
<
C
!oe
1
[2] can be ob-
tained from one of the traces of M
B
and the trace of M
C
, so according to anti-patten1,
M
B
k M
C
will deadlock when ?oe
1
[2] happens before !oe
2
in M
B
and ?oe
2
happens
before ?oe
1
[2] in M
C
. The blocking states are S
B
d
= {B
2
} and S
C
d
= {C
2
}.
Anti-Pattern 2. Suppose !x O
1
, ?x E
2
and !y O
1
, ?y E
2
, M
1
k M
2
has
non-local branching choice if !ox]
1
!oy (2).
M1 M2
?oy
!ox ?ox
!oy
!ox
?ox
!oy
?oy
case 1
case 2
!ox
?ox
!oy
?oy
#
#
#
Figure 3.4: Non-local branching 1
Figure 3.4 shows the MSC and casual ordering. M
1
sends message instances ox, oy
to M
2
. In M
1
, a send event occurrence of ox is in branch-conflict with a send occurrence
of oy (2). Two cases may exist in M
2
:
1) If ?ox <
2
?oy, M
2
waits for both message instances ox and oy from M
1
, but
M
1
cannot send these message instances in the same run due to (2). We have
c
:!ox]!oy!ox <?ox!oy <?oy?ox <?oy. By !ox]
1
!oy and message ordering, we
have ox ¬(!oy) ¬(?oy) and oy ¬(!ox) ¬(?ox), so ?ox <
2
?oy does not
41
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.5 Compatibility and Anti-patterns
hold.
2) If ?ox]
2
?oy, we have casual ordering
c
:!ox]!oy!ox <?ox!oy <?oy?ox]?oy. If
!ox (resp. !oy) happens in M
1
and ?oy (resp. ?ox) happens in M
2
, then M
2
will
wait for message instance oy (resp. ox) forever due to (2). The blocking state set
of M
2
is not empty.
Figure 3.5 shows an example, we have !om
2
]
A
!om
3
. In case 1), we have ?om
2
<
B
?om
3
, so M
A
k M
B
has non-local branching choice with S
B
d
= {B
4
} or S
B
d
= {B
5
}. In
case 2), we have ?om
2
]
B
?om
3
, so M
A
k M
B
has non-local choice with S
B
d
= {B
2
} or
S
B
d
= {B
4
}.
A1
A3
A2
A5
A4
MA
B3
B2
MB
B4
B7
?m2
?m3
B5
B1
B6
?m4?m1
[g1]/!m1
[g2]/!m2
[g1]/!m3
[g2]/!m4
[g3]/count:=1
?m3
/!m5
Figure 3.5: An example of anti-patterns 2 and 3
Anti-Pattern 3. Suppose !x O
1
, ?x E
2
and !y O
2
, ?y E
1
, M
1
k M
2
has
non-local branching choice if !ox]
1
?oy and ?ox]
2
!oy (3).
M1 M2
!oy
!ox
?ox
?oy
?ox
?oy
!oy
#
#
!ox
Figure 3.6: Non-local branching 2
Figure 3.6 shows the MSC and casual ordering. M
1
sends message instance ox to
M
2
, and M
2
sends message instance oy to M
1
. The causal ordering is
c
:!ox <?ox,
!oy <?oy, !ox]?oy, and ?ox]!oy. If ?oy happens in M
1
and ?ox happens in M
2
, machine
42
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
3.6 Summary
M
1
(resp. M
2
) will wait for message instance oy (resp. ox) forever due to (3). The
blocking state s ets of both machines are not empty.
In Figure 3.5, !om
3
]
A
?om
4
and ?om
3
]
B
!om
4
hold. When ?om
4
happens in M
A
and
?om
3
happens in M
B
, M
A
k M
B
has non-local choice and each machine has blocking
states S
A
d
= {A
4
} and S
B
d
= {B
2
}. Similarly, !om
2
]
A
?om
1
and ?om
2
]
A
!om
1
will cause
non-local choice. In this example, om
2
]
A
om
3
will also cause non-local choice with the
type of anti-pattern2.
The above anti-patterns can be encoded into temporal logics, so that model checking
tools (e.g. (Hol03; CCGR99)) can be used to automate the pre-checking.
3.6 Summary
The formal static semantics and dynamic semantics of Web Service Automaton are
given in this section. The web service automaton is more general than the existing
automata-based semantics because we include multiple-event transitions, data, and
internal events. We use message-passing as the uniform mechanism for machine com-
munications. Aslo, anti-patterns are identified for web service interactions. The anti-
pattern pre-checking has the advantage that it needs less computation effort to identify
incompatible behaviours, and the corresponding properties can be reused.
43
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
Chapter 4
Analysis of BPEL Features in
Web Service Automata
BPEL consists of two categories of activities: basic and structured activities. Basic
activities are atomic actions. Structured activities impose control flow dependency
constrains on the executions of either the basic or structured activities within them.
A structured activity can contain arbitrary depth of sub-activities. Like many pro-
gramming languages, BPEL has control structures including pick, switch, while, scope,
eventHandlers, faultHandlers constructs to express control dependencies between activ-
ities. Also, BPEL has sequence, flow constructs to support sequential and concurrent
relationship between activities, and compensationHandler construct to reverse the com-
pleted activities. For data handling, BPEL uses ’blackboard approach’, where a set of
variables is shared by all activities.
In this section, we analyse BPEL main features and describe how to capture these
features in WSA. The detailed mapping from BPEL to WSA will be covered in (Zhe07).
Each BPEL activity is associated with a machine. We use machine as shorthand for
a web service automaton, and call the machine associated with BPEL x activity as x
machine. In state machine diagrams, an initial state is pointed by an arrow started
with a filled black circle, and a final state is shaded.
44
DBE Project (Contract n°507953)
D10.2 DBE Test Automation Framework
4.1 BPEL Control Flow
BPEL consists of basic and structured activities. Basic activities are atomic ac-
tions. Structured activities impose control dependencies on the executions of either
the basic or structured activities within them . A structured activity can contain an
arbitrary depth of sub-activities. BPEL has structured activities including the pick,
switch, while, sequence, flow, scope, eventHandlers, faultHandlers, and a compensation-
Handler structured activity to reverse completed activities. BPEL handles data using
a blackboard approach, where a set of variables is shared by the enclosed activities.
In this sec tion, we analyse the main features of BPEL and describe how to capture
these features in WSA. We use a loan approval process example (? ) to illustrate
the data flow mo del and the control flow hierarchy. We use m achine as shorthand for
a web service automaton, and call the machine associated with BPEL x activity as x
machine. In state machine diagrams, an initial state is pointed by an arrow starting
with a filled black circle, and a final state is shaded.
4.1 BPEL Control Flow
4.1.1 Hierarchy
A WSA has no hierarchy. We simulate the hierarchical relationships of BPEL activities
by adding start message and done message as common administration messages between
machines. A machine can play the role of parent or child. For a machine M, its parent