Skip to main content

Research Repository

Advanced Search

A model checking based approach to automatic test suite generation for testing web services and BPEL.

Zhao, Huiqun; Sun, Jing; Liu, Xiaodong


Huiqun Zhao

Jing Sun


With the rapid increase of Web Service applications, the reliability of web service and service composition has drawn particular attention from researchers and industries. Many methods for testing and verifying the reliability have been discussed, however, the existing methods are weak in test automation and therefore difficult in tackling the dynamic features of modern SOA based application. The traditional method of model checking and the technique of test suite generation have a large potential for the reliability verification of web services and service composition. In this paper, an approach to integrating the test suite generation technique with model checking is presented. The approach takes advantage of model checking to verify BPEL script at the logical level, and to generate test suite automatically based on the model description, and finally to select test cases with respect to the counterexamples of model checking output. The approach contributes a set of algorithms and its implementation to support a translation from BPEL to LOTOS, and LTS(Labeled Transition Systems, LTS in short) to TTCN(Test and Testing Control Notation, TTCN in short) behavior Tree. Finally, a case study is presented to demonstrate and verify the proposed approach.

Start Date Dec 6, 2012
End Date Dec 8, 2012
Publication Date 2012
Deposit Date Nov 5, 2013
Peer Reviewed Peer Reviewed
Pages 61-69
Book Title Proceedings of IEEE Asia-Pacific Services Computing Conference
ISBN 978-1-4673-4825-6
Keywords Automatic Test; BPEL Model Checking; LOTOS; Test Case Generation; Web Service Testing; TTCN-3;
Public URL
Publisher URL