ISSN : 1796-217X
Volume : 2    Issue : 3    Date : September 2007

An Automatic Test Case Generation Framework for Web Services
Yongyan Zheng, Jiong Zhou, and Paul Krause
Page(s): 64-77
Full Text:
PDF (509 KB)

BPEL (Business Process Execution Language) as a de-facto standard for web service
orchestration has drawn particularly attention from researchers and industries. BPEL is a
semi-formal flow language with complex features such as concurrency and hierarchy. To test a
model thoroughly, we need to cover different execution scenarios. As is well known, it is tedious,
time consuming, and error prone to design test cases manually, especially for complex modelling
languages. Hence, it is desirable to apply existing model-based-testing techniques in the domain of
web services. We proposed WSA (Web Service Automata) to be the operational semantics for
BPEL. Based on WSA, we propose a model checking based test case generation framework for
BPEL. The SPIN and NuSMV model checkers are used as the test generation engine, and the
conventional structural test coverage criteria are encoded into LTL and CTL temporal logic. State
coverage and transition coverage are used for BPEL control flow testing, and all-du-path coverage is
used for BPEL data flow testing. Two levels of test cases can be generated to test whether the
implementation of web services conforms to the BPEL behaviour and WSDL interface models. The
generated test cases are executed on the JUnit test execution engine.

Index Terms
web services, finite state machine, model checking, test coverage, test case generatio