Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger
We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform.
Proceedings of the International Conference on Web Services (ICWS), IEEE Computer Society Press, 2007, pp. 831-838.
Download inofficial, sometimes updated
© 2007 IEEE.