Fill in your chosen form

Sign the form using our drawing tool

Send to someone else to fill in and sign.

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

DATE

AUTHOR, ORGANISATION

1.0

09/02/2007

YONGYAN ZHENG

2.0

20/09/2006

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 Veriﬁcation 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 Buﬀering 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 ﬂow 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 Veriﬁcation 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

List of Figures

1.1 Web Service Stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

1.2 UML diagrams and web service speciﬁcations . . . . . . . . . . . . . . . 4

2.1 An example of Petri nets for BPEL activities . . . . . . . . . . . . . . . 11

3.1 Message overtaking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

3.2 Unspeciﬁed 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 ﬂow 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

deﬁnes 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 ﬂexible, re-usable, and loosely coupled model for dis-

tributed computing. A SOC oﬀers three main functions: communication protocols,

service descriptions, and service discovery.

In this work we lo ok at the service descriptions, with focus on the veriﬁcation

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 ﬂow-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 veriﬁcation 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 diﬀerent programming languages and

running on diﬀerent 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

ﬁnd 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 deﬁni-

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 speciﬁcations 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 Deﬁnition Language) (CCMW01) deﬁnes 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 deﬁnes 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 speciﬁcations have been proposed in these areas:

• Business rule layer: SBVR (Semantics of Business Vocabulary and Business Rules

Speciﬁcation) (OMG06) describes the business rules using the pre-deﬁned 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-

ﬁdentiality, 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; ﬁnally, 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 speciﬁcations

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

ﬁrst 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

deﬁnes 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.

Brieﬂy 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 workﬂow languages for modeling business processes com-

posed of a set of service invocations. The structure deﬁnes the partial order of invo-

cation of the services and their interactions. BPEL, as an industrial standard, aims to

provide rich control ﬂow structures to integrate existing web services in a ﬂexible way.

BPEL supports exception handling and compensations, while OWL-S does not deﬁne

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 ﬂow 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 deﬁnes 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 deﬁned in the

partnerRole and myRole attributes of the partnerLinkType.

For a composite service mo delled by process workﬂow languages such as BPEL or

OWL-S. WSDL deﬁnes the data types of the service w hich are used directly in the

process. WSDL uses messages to deﬁne and carry data types. In a BPEL process, a

variable is deﬁned 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 ﬁnd errors as early as possible in the workﬂow design phase.

BPEL activity relationships can be categorized into control-ﬂow and data-ﬂow.

Since BPEL is a semi-formal ﬂow language, various formal semantics have be en pro-

posed, so that BPEL models can be veriﬁed rigorously. However, most current formal

models only focus on m odelling BPEL control ﬂow, and do not cover the BPEL data

6

DBE Project (Contract n°507953)

D10.2 DBE Test Automation Framework

1.3 Aims and Objectives

ﬂow 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 eﬀort 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 veriﬁcation and test case generation of both BPEL

control-ﬂows and data-ﬂows in a uniﬁed 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 veriﬁcation and testing of BPEL

control ﬂow and data ﬂow.

• 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 veriﬁcation and testing

of BPEL. Our formal model is intended to be used by such veriﬁcation tools. With

model checking, a BPEL model can not only be a design model for veriﬁcation, 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 ﬂows.

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 ﬂow testing, and all-du-path coverage is used for

BPEL data ﬂow 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

veriﬁcation and test case generation framework for BPEL and WSDL. The key beneﬁts

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 ﬂow

testing and data ﬂow 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 eﬀective 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 veriﬁcation 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 veriﬁcation of

process models. In order to maintain the focus of this rep ort, we concentrate on the

veriﬁcation 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 Veriﬁcation 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 veriﬁcation tools. The veriﬁcation

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 veriﬁcation phase helps increas e the reliability of web

services. The works of (MM04; HS04) provide good reviews for the current veriﬁcation

approaches.

10

DBE Project (Contract n°507953)

D10.2 DBE Test Automation Framework

2.1 Formal Semantics and Veriﬁcation 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 ﬂow 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 ﬁres by removing the tokens from its

input places and adds a speciﬁed 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 ﬁnished, respectively. Transitions are of three types. The ﬁrst

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 Veriﬁcation of BPEL based web services

type is activity transition to model the events or actions of a BPEL activity. On the

left of the ﬁgure, 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

ﬁgure, the petri net models a BPEL ﬂow activity, when the ﬂow is started, subnets

A, B will be executed, and the ﬂow 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 deﬁning 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 speciﬁcally coloured token.

Web service algebra is proposed in (HB03) to deﬁne 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 ﬂow 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 veriﬁcation tool

WofBPEL is used as the analysis engine. The paper discusses how to verify the activity

reachability and some pre-deﬁned 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 Veriﬁcation of BPEL based web services

their corresponding meaning in the veriﬁcation 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 veriﬁcation 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 deﬁned and the ﬁeld 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 deﬁnition, or a recursive invocation. I/O

13

DBE Project (Contract n°507953)

D10.2 DBE Test Automation Framework

2.1 Formal Semantics and Veriﬁcation 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

speciﬁes 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 ﬁrst 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 veriﬁcation

unusable or impractical.

In (Fer04), a two-way mapping is deﬁned between BPEL and LOTOS, and model

checking toolbox CADP (FGK

+

96) is used as the veriﬁcation engine. The mapping

from LOTOS to BPEL does not preserve the structure of a process, due to the expressive

and ﬂexible 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 veriﬁcation

engine. The web service composition speciﬁcation 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 Veriﬁcation of BPEL based web services

be veriﬁed against the MSC speciﬁcation 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 veriﬁcation 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 diﬃcult 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 Veriﬁcation 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

speciﬁcations of systems. An automaton is a mathematical model for a ﬁnite 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 ﬁnite 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 veriﬁcation 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 suﬃcient 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 Veriﬁcation 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 veriﬁed. We believe

this will decrease the speed of model checkers, and symbolic transition guards can reach

the same veriﬁcation 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 veriﬁcation 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 reﬁnement. However, for the purpose of veriﬁcation and testing, the

automaton formalism is especially attractive due to the straight usage of mo del check-

ing tools. The model s ubstitution and reﬁnement 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 oﬀers 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 ﬁll this gap.

In summary, in order to solve some of the current problems, it is essential to design

a formal m odel which fulﬁls the following requirements: 1) the formal model should

be able to ﬁll 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 veriﬁcation of correctness of BPEL models. However, there

is less eﬀort 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 deﬁne 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 ﬂow. 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 deﬁned 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 ﬂow 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 ﬂow graph. For instance in a process data ﬂow graph, data always ﬂows

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 ﬂow edge. A toolset is developed to support the

visualization. Even though their focus is not rigorous veriﬁcation 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 deﬁnition 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 workﬂow language is proposed in (FQH05), where each activity may have

data-in port and data-out port. The data exchange describes that the data ﬂows

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 ﬂow activities).

The authors in (APS05) provide a mo del of data ﬂow in addition to control ﬂow

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 ﬂow

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 ﬂow 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 workﬂow 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 deﬁne a set

of composittion axioms to add constrains on the conversation protocol. A data-ﬂow

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 ﬂow 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 ﬂow

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 ﬂow 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 veriﬁcation 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 ﬁnite state machine with sig-

nature, data structure, and message storage schema. The dynamic semantics of a web

service automaton includes machine conﬁgurations and execution traces. The formal

deﬁnitions are given below.

Deﬁnition 1. We assume that we have available an enumerable inﬁnite 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 satisﬁes:

• 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-

isﬁes: 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 deﬁnition of a machine’s data

structure is given in deﬁnition 2.

Deﬁnition 2. A Web Service Automaton (WSA) M is a ﬁnite 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 ﬁnal states.

3) T ⊆ IN ×BX×(℘(AX)∪OUT ) is a set of transitions, where IN = (E∪L

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

exp∈AX

({def(exp)} ∪

cuses(exp)) and

S

exp∈BX

{puses(exp)}.

• We deﬁne that a WSA is T -complete iﬀ 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 (deﬁnition 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

Deﬁnition 3. A WSA is deterministic iﬀ ∀s, s

0

, s

00

∈ S.∀t ∈ T , s

t

→ s

0

∧ s

t

→

s

00

⇒ s

0

= s

00

holds.

Deﬁnition 4. We deﬁne 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 deﬁned the static structure of a WSA. We now explain its dynamic semantics.

We assume, ﬁrst of all, that a WSA is equipped with a means of storing incoming

messages. Instead of limiting the buﬀers to a particular type such as FIFO or multi-

set, we consider diﬀerent buﬀering schemes (s ec tion 3.4). We as sume that each WSA is

associated with a ﬁnite buﬀer. The buﬀer β(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 buﬀer β(E ∪ L

in

); or 2) an enabled transition

ﬁres, possible causing a state change and change to the values of some variables v ∈ V

M

.

In order to precisely deﬁne a step, we need to formalise the notion of a conﬁguration

η which records the current state, the current values of the variables associated with

M and the current content of the buﬀer.

A transition t is enabled in a conﬁguration η, 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 buﬀering 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 deﬁne 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.

Deﬁnition 5. A conﬁguration of a machine M is of the form η = (s, B, ), where

s ∈ S, B ⊆ β(E ∪ L

in

) is the current buﬀer content, and function : V → D assigns

the variable of V with a value from D. The set of conﬁgurations of M is denoted as

confs(M ) where η ∈ confs(M). Note that we ass ume the buﬀer is empty when M

is either in the initial state or in a ﬁnal state (hypothesis 1), so η

0

= (s

0

, ∅,

0

) and

η

n

= (s

n

, ∅,

n

) are the initial and a ﬁnal conﬁguration, respectively.

Hypothesis 1. The buﬀer is empty when machine M is in a ﬁnal state. If M is

in a ﬁnal state, we s ay a lifecycle of the machine ends. If the buﬀer is not empty then

the remaining messages will be discarded because they cannot be c onsumed within this

lifecycle.

Deﬁnition 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 conﬁguration η to conﬁguration η

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 buﬀer B, then (s, B, ) 7→

x

(s

0

, B

0

,

0

) iﬀ s = s

0

, =

0

, B

0

= B + {x}.

2) If x = t ∈ T , representing the case when either the message is already in the

buﬀer t.m ∈ B or there is no triggering event associated with t, then (s, B, ) 7→

t

(s

0

, B

0

,

0

) iﬀ 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

Deﬁnition 7. We deﬁne a set of conﬁguration sequences of M as configs(M, η

0

).

A conﬁguration sequence of M ,α = hη

0

, x

0

, .., η

n

)i ∈ configs(M, η

0

), is a sequence of

conﬁgurations linked by input events,internal input events, or enabled transitions from

the initial conﬁguration to a ﬁnal conﬁguration, where η

i

= (s

i

, B

i

,

i

), x ∈ E ∪L

in

∪ T .

1) We deﬁne 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

n−1

i such

that trans(M ) = {trans(α)}, where x

i

∈ T, α = hη

0

, x

0

, .., η

n

i ∈ configs(M, η

0

),

and trans(η

0

) = {Ω}.

2) We deﬁne 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.

Deﬁnition 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 iﬀ 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 (deﬁnition 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 deﬁne a general composite

automaton with an interleaving s em antics (deﬁnition 10). Such composite automaton

is not guarantee to be a WSA (deﬁnition 11). We then elicit a set of constraints on

the individual WSAs as the necessary, suﬃcient, or necessary and suﬃcient conditions

for a composite automaton to be a WSA or to be a deterministic WSA. For strongly

composable WSAs (deﬁnition 12), we prove that the buﬀer 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 conﬁgurations as well as conﬁguration sequences of

individual WSAs can be projec ted from the composite automaton, and we also prove

that the composition operator is associative.

Deﬁnition 9. If (X

i

)

i∈I

is an indexed family of sets, we deﬁne

Q

i∈I

X

i

to be the

set of all functions ω : I →

S

i∈I

X

i

satisfying ω(i) ∈ X

i

for each i ∈ I. We refer

to

Q

i∈I

X

i

as the unordered Cartesian product of a set of X

i

. Note that

Q

is a

commutative and associative binary operator.

Deﬁnition 10. If M

1

, M

2

are WSAs, then we deﬁne 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 deﬁne 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 deﬁne

ˆ

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 ﬁnal if, for all machines, the

local state s

i

of M

i

is ﬁnal.

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.

Deﬁnition 11. M

1

, M

2

are composable iﬀ 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

Deﬁnition 12. M

1

, M

2

are strongly composable iﬀ a) Msg

1

∩ Msg

2

= com

12

,

and b) T

1

∩ T

2

= ∅.

Theorem 1.

ˆ

M = M

1

k M

2

are WSAs iﬀ 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

t∈T

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 deﬁne a transition t to be self-loop in machine M , written as t ∈ self(M), iﬀ 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 iﬀ (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

iﬀ

(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 deﬁnition 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

deﬁnition 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 conﬁgura-

tion of individual automaton η

i

can be projected from the conﬁguration 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

suﬃcient to prove (1) holds. Based on deﬁnition 8, we need η 7→

x

η

0

to represent a step

between conﬁgurations.

First, when x ∈

ˆ

E, we have η 7→

x

η

0

iﬀ 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 deﬁnition 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

iﬀ 1) In the case of x ∈ T

1

, project

1

(η) 7→

x

project

1

(η

0

) and project

2

(η) 7→

x.a∩E

2

project

2

(η

0

). By lemma 5, it follows x ∈ T

1

⇒

η

1

7→

x

η

0

1

and η

2

7→

x.a∩E

2

η

0

2

. 2) Similarly, in the case of x ∈ T

2

, project

2

(η) 7→

x

project

2

(η

0

) and project

1

(η) 7→

x.a∩E

1

project

1

(η

0

). By lemma 5, it follows x ∈ T

2

⇒

η

2

7→

x

η

0

2

and η

1

7→

x.a∩E

1

η

0

1

.

As a result, for projection on transition and messages, we have project

i

(x

0

, .., x

n−1

) =

project

i

(x0), .., pr oject

i

(x

n−1

). 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 deﬁnition 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 Buﬀering 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

∩(

¯

X∪X

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

= L∪X

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 Buﬀering Schemes

Since there is more than one reasonable buﬀering mechanism, the buﬀering scheme of

WSA should be ﬂexible and conﬁgurable. Inspired by Alur (AHP96), we identify the

commonly used buﬀering s chemes:

1) FIFO buﬀering scheme: A machine has one FIFO buﬀer. 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

buﬀer.

35

DBE Project (Contract n°507953)

D10.2 DBE Test Automation Framework

3.4 Buﬀering Schemes

2) Multi-set (deﬁnition 13) buﬀering schemes: a) Multi-set buﬀer with FIFO sub-

buﬀers: A machine has one multi-set buﬀer that consists of FIFO sub-buﬀers,

where each FIFO sub-buﬀer corresponds to a message type. A message can be

consumed when it is at the head of each FIFO sub-buﬀer. b) Multi-set buﬀer

without sub-buﬀers: A machine has one multi-set buﬀer. A message can be

consumed as long as it is in the buﬀer. For those messages of the same type,

the machine will randomly consume a message in the buﬀer. c) Multi-set buﬀer

with multi-set sub-buﬀers: A machine has one multi-set buﬀer that consists of

multi-set sub-buﬀers, where each multi-set sub-buﬀer corresponds to a message

type. The machine consumes messages in the same way as of b).

Deﬁnition 13. A ﬁnite multi-set is formally deﬁned 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 diﬀers 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 diﬀe 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 diﬀerent from the order of send event

occurrences !ox1, !ox2.

We assume that WSA with both FIFO and multi-set buﬀering schemes only allow

type 1) but not type 2) of message overtaking.

3.5 Compatibility and Anti-patterns

In this section, we deﬁne 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.

Deﬁnition 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

.

Deﬁnition 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

iﬀ 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

ﬁguration 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 deﬁnition 10, it shows (s

1

i

, s

2

i

)

t

→ (s

1

j

, s

2

j

) iﬀ 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→

t∈T

1

⇔ η

1

B

7→

t∈T

1

or η

2

B

7→

t∈T

2

. Here η

i

B

= (s

i

0

, proj

i

(B),

i

0

), and proj is the projection operator.

Without loss of generality suppose ˆη 7→

t∈T

2

ˆ

η

0

, we have s

1

0

t∈T

1

→ s

1

1

, t.m ∈ B, and

apply

G

(t.g,

1

) = true. Conversely, we have ¬( ˆη

B

7→

t∈T

1

) iﬀ for all B either ¬(s

1

0

t∈T

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 iﬀ 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 deﬁnition 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 identiﬁed 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 modiﬁed in the earliest s tages . Furthermore, since a WSA’s local

ordering (deﬁnition 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 deﬁnitions 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

Deﬁnition 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 conﬁguration 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.

Deﬁnition 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-

conﬂict with o

2

in a conﬁguration sequence of M . Intuitively, two branch-conﬂict

eve nt occurrences cannot happen in the same trace.

Deﬁnition 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.

Deﬁnition 19. For machines {M

1

, .., M

n

}, we deﬁne message orderings to be the

structure <

X

=

S

λ(!om),λ(?om)∈X

(!om <?om), where om = (!om, ?om), X ⊆

S

1≤i,j≤n

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.

Deﬁnition 20. The causal ordering for a set of machines {M

1

, .., M

n

} is the struc-

ture ≺

C

= (

S

1≤i≤n

l

i

)∪ <

X

, which describes the transitive closure of the set of local

orderings and message orderings.

Deﬁnition 21. A machine M is said to be blocking iﬀ 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 deﬁnition

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 iﬀ S

d

6= ∅.

In state machine diagrams, an initial state is pointed by an arrow started with a ﬁlled

black circle, and a ﬁnal 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

unspeciﬁed 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: Unspeciﬁed 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 conﬂict 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 unspeciﬁed 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-conﬂict 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 identiﬁed for web service interactions. The anti-

pattern pre-checking has the advantage that it needs less computation eﬀort 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 ﬂow 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, ﬂow 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 ﬁlled black circle, and a ﬁnal 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, ﬂow, 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 ﬂow mo del and the control ﬂow 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 ﬁlled black circle, and a ﬁnal 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