Abstract

BPEL (Business Process Execution Language)as a de-facto standard for web service orchestration hasdrawn particularly attention from researchers and industries.BPEL is a semi-formal flow language with complexfeatures such as concurrency and hierarchy. To test a modelthoroughly, we need to cover different execution scenarios.As is well known, it is tedious, time-consuming, and errorprone to design test cases manually, especially for complexmodelling languages. Hence, it is desirable to apply existingmodel-based-testing techniques in the domain of web services.We proposed WSA (Web Service Automata) to be theoperational semantics for BPEL. Based on WSA, we proposea model checking based test case generation framework forBPEL. The SPIN and NuSMV model checkers are used asthe test generation engine, and the conventional structuraltest coverage criteria are encoded into LTL and CTLtemporal logic. State coverage and transition coverage areused for BPEL control flow testing, and all-du-path coverageis used for BPEL data flow testing. Two levels of test casescan be generated to test whether the implementation ofweb services conforms to the BPEL behaviour and WSDLinterface models. The generated test cases are executed onthe JUnit test execution engine.