Abstract
Web service conformance testing checks the correctness of a black box service implementation, and it is the basis of other testings. An efficient formal method for conformance testing is the Chinese Postman traversal algorithm [2] that can find minimum-cost test sequences.However, the applicability of this algorithm is in question if data dependences are present in the protocol specification. Also, it suffers from the limited observability problem which is not uncommon in web services. Despite its optimality, the traversal algorithm does not take advantages of the special patterns in web service interfaces observed by developers. To address these issues, we propose an abstract GFSM (Guarded Finite-State Machine) model that unifies and augments the commonly used Moore and Mealy machines with dataflows. Using this abstract model, we formalize the conditions under which the tours with complete data and control coverage are guaranteed, and address the limited observability problem using the equivalence of Moore and Mealy machines. Furthermore, we propose a Recursive Descent traversal algorithm that explores the inverse operation pattern of web services to facilitate incremental development of web services.