Generating Test Cases Specifications for BPEL Compositions of Web Services Using SPIN
José García-Fanjul, Javier Tuya, Claudio de la Riva · Consultation of the Doctoral Thesis Database (TESEO) (Ministerio de Educación, Cultura y Deporte) · 2006
Generating test cases for compositions of web services is complex, due to their distributed nature and asynchronous behaviour.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.