Presenter

Iyad Alshabani

Abstract

In this presentation I will talk about the using of a symbolic transition system (STS) for the test and verification of WS-BPEL orchestration.
The approch is to translate orchestration spcifications into a formal model (in STS), then a symbolic execution tree(SET) is computed from the this STS. It supports the retrieval of the STS execution semantics, while avoiding the usual state-explosion problem in presence of unbounded data types, as used in full-fledged BPEL. Given a coverage criterion, a set of execution paths is generated from the SET which are finally run by a test oracle against the orchestration implementation. Formal model, developement results,  challanges and demonstations about the implementation of BPEL->STS and STS->BPEL transoformations will be presented.