Verifiable Web services with hierarchical interfaces

We propose an hierarchical state machine (HSM) model for specifying behavioral interfaces of peers participating in a composite Web service. We integrate the HSM model to a design pattern which is supported by a modular verification technique that can 1) statically analyze the properties about global interactions of a composite Web service and 2) check the conformance of the Java implementations of the participant peers to their interfaces. We extend the synchronizability analysis to HSMs to efficiently identify composite Web services whose global interactions can be analyzed with respect to unbounded queues using finite state model checkers. We also discuss automated translation of behavioral interfaces specified as HSMs to BPEL specifications to be published and used by other services.