University of Oulu
From the inception of the Web, a growing number of companies have tried to use it as a new commercial channel. Generating test cases for compositions of web services is complex, due to their distributed nature and asynchronous behavior. In this paper, a formal verification tool - the SPIN model checker - is used to generate test suite specifications for compositions specified in BPEL. A transition coverage criterion is employed to define a systematic procedure to select the test cases. The approach is applied to the \"Loan approval\" sample composition.