Web services are gaining industry-wide acceptance and usage by fostering the developmentof distributed applications out of the composition of simpler entities calledservices. In complement to verification, testing allows one to check for the correctnessof a binary (no source code) service implementation with reference to a specification.In this thesis, we propose black box conformance testing approach for centralizedservice compositions (orchestrations). With reference to the state of the art, wedevelop a symbolic approach in order to avoid state space explosion issues due to theXML data being largely used in Web services. This approach is based on symbolicmodels (STS), symbolic execution, and the use of a satisfiability modulo theory(SMT) solver. Further, we propose a comprehensive end-to-end approach that goesfrom specification using a standard orchestration language (ABPEL), and the possibledescription of test purposes, to the online realization and execution of symbolic testcases against an implementation. A crucial point is a model transformation fromABPEL to STS that we have defined and that takes into account the peculiarities ofABPEL semantics. The automation of our approach is supported by a tool-chainthat we have developed.
