Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services
This paper focuses on the realizability problem of a framework for modeling and specifying the global behavior of reactive electronic services (e-services). In this framework, Web accessible programs (peers) communicate by asynchronous message passing, and a virtual global watcher listens silently to the network. The global behavior is characterized by a conversation, which is the infinite sequence of messages observed by the watcher. We show that given a Büchi automaton specifying the desired set of conversations, called a conversation protocol, it is possible to implement it using a set of finite state peers if three realizability conditions are satisfied. In particular, the synthesized peers will conform to the protocol by generating only those conversations specified by the protocol. Our results enable a top-down verification strategy where: (1) A conversation protocol is specified by a realizable Büchi automaton, (2) The properties of the protocol are verified on the Büchi automaton specification, (3) The peer implementations are synthesized from the protocol via projection.
KeywordsGlobal Behavior Business Process Execution Language FIFO Queue Input Queue Illegal State
Unable to display preview. Download preview PDF.
- L.D. Alfaro and T.A. Henzinger. Interface automata. In Proc. of 9th ACM Symp. on Foundations of Software Engineering, pages 109–120, 2001.Google Scholar
- R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification of MSC graphs. In Proc. 28th Int. Colloq. on Automata, Languages, and Programming, 2001.Google Scholar
- Business process execution language for web services (BPEL4WS), version 1.1. available at http://www.ibm.com/developerworks/library/ws-bpel.
- Business process modeling language (BPML). http://www.bpmi.org.
- T. Bultan, X. Fu, R. Hull, and J. Su. Conversation specification: A new approach to design and analysis of e-service composition. In Proc. of 12th Intl. World Wide Web Conf., May 2003.Google Scholar
- M. Chiodo, P. Giusto, A. Jurecska, L. Lavagno, H. Hsieh, and A. Sangiovanni-Vincentelli. A formal specification model for hardware/software codesign. In Proc. of the Intl. Workshop on Hardware-Software Codesign, October 1993.Google Scholar
- E. M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.Google Scholar
- E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science: Volume B: Formal Models and Semantics, pages 995–1072. Elsevier, 1990.Google Scholar
- S. J. Garland and N. Lynch. Using I/O automata for developing distributed systems. In Foundations of Component-Based Systems. Cambridge Univ. Press, 2000.Google Scholar
- P. Graunke, R.B. Findler, S. Krishnamurthi, and M. Felleisen. Modeling web interactions. In Proc. of 12th European Symp. on Programming, LNCS 2618, 2003.Google Scholar
- J.E. Hanson, P. Nandi, and S. Kumaran. Conversation support for business process integration. In Proc. of 6th IEEE Int. Enterprise Distributed Object Computing Conference, 2002.Google Scholar
- R. Hull, M. Benedikt, C. Christophides, and J. Su. E-services: A look behind the curtain. In Proc. of 22nd ACM Symp. on Principles of Database Systems, 2003.Google Scholar
- IBM. Conversation support project. http://www.research.ibm.com/convsupport/
- G. Kahn. The semantics of a simple language for parallel programming. In Proc. of IFIP 74, pages 471–475. North-Holland, 1974.Google Scholar
- H. Liu and R. E. Miller. Generalized fair reachability analysis for cyclic protocols. In IEEE/ACM Transactions on Networking, pages 192–204, 1996.Google Scholar
- N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. Principles of Distributed Computing, pages 137–151, 1987.Google Scholar
- R. Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.Google Scholar
- A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. of 16th ACM Symp. Principles of Programming Languages, pages 179–190, 1989.Google Scholar
- S.K. Rajamani and J. Rehof. A behavioral module system for the pi-calculus. In Proc. of Static Analysis Symposium (SAS), July 2001.Google Scholar
- Sun. Java message service. http://java.sun.com/products/jms/.
- W3C. Web service choreography interface (WSCI) version 1.0. available at http://www.w3.org/2003/01/wscwg-charter.
- W3C. Web services description language (WSDL) version 1.1. available at http://www.w3.org/TR/wsdl, 2001.