Web Services Choreography Description Language (abbreviated as WS-CDL) which is reusable and capable of describing transactional requirements regulates the partici-pants' external behaviors from the global viewpoint. Verification and testing of WS-CDL programs before deployment can drastically reduce the deployment risk and project cost. Since WS-CDL is a description language whose program is not executable, and there is no language compiler or simulator available, it is very hard to test and verify WS-CDL programs.In this thesis, we propose a unified approach to validate the static constraints of XM-L languages. This approach which resembles the model checking method is language-agonistic and version scalable. The logic used for describing static constraints is called Constraint Logic which is based on the First Order Logic. We also propose a formal model for capturing XML documents. Furthermore, an algorithm optimized with model pruning technique is also designed for validating XML documents against static con-straint formulas.Based on a home-grown WS-CDL program simulator, we propose an automatic test-ing approach for WS-CDL documents. This approach employs test cases generated from symbolic execution to automatically test WS-CDL documents regarding path coverage criteria. It supports features such as exception handling and finalization which are ig-nored in other researches. Furthermore, we introduce two ways of handling assertions which are used for expressing the desired behavioral results for WS-CDL programs.We implement the aforementioned approaches in a modular based open source E-clipse Plugin called CDLChecker. CDLChecker is an Integrated Development Environ-ment for WS-CDL with features such as editing, simulation, validation and automatic testing. Finally, we evaluate the proposed approaches on CDLChecker with several ex-periments. The experimental results reveal that the proposed approaches work effectively for WS-CDL. |