×

zbMATH — the first resource for mathematics

Conversation protocols: a formalism for specification and verification of reactive electronic services. (English) Zbl 1071.68002
Summary: This paper focuses on the realizability problem of a framework for modeling and specifying the global behaviors of reactive electronic services (e-services). In this framework, Web accessible programs (peers) communicate by asynchronous message passing, and a virtual global watcher silently listens 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 realize the protocol 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, and (3) The peer implementations are synthesized from the protocol via projection.

MSC:
68M10 Network design and communication in computer systems
68M12 Network protocols
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] M. Abadi, L. Lamport, P. Wolper, Realizable and unrealizable specifications of reactive systems, in: Proc. of 16th Internat. Colloq. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 372, Springer, Berlin, 1989, pp. 1-17.
[2] Abdulla, P.; Jonsson, B., Verifying programs with unreliable channels, Inform. comput., 127, 2, 91-101, (1996) · Zbl 0856.68096
[3] Alfaro, L.D.; Henzinger, T.A., Interface automata, (), 109-120
[4] R. Alur, K. Etessami, M. Yannakakis, Realizability and verification of MSC graphs, in: Proc. 28th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, Vol. 2076, 2001, pp. 797-808. · Zbl 0986.68518
[5] Alur, R.; McMillan, K.; Peled, D., Model-checking of correctness conditions for concurrent objects, Inform. comput., 160, 167-188, (2000) · Zbl 1003.68067
[6] Business Process Execution Language for Web Services (BPEL), Version 1.1. http://www.ibm.com/developerworks/library/ws-bpel, May 2003.
[7] Business Process Modeling Language (BPML). http://www.bpmi.org.
[8] Brand, D.; Zafiropulo, P., On communicating finite-state machines, J. ACM, 30, 2, 323-342, (1983) · Zbl 0512.68039
[9] Bultan, T.; Fu, X.; Hull, R.; Su, J., Conversation specificationa new approach to design and analysis of e-service composition, (), 403-410
[10] M. Chiodo, P. Giusto, A. Jurecska, L. Lavagno, H. Hsieh, A. Sangiovanni-Vincentelli, A formal specification model for hardware/software codesign, in: Proc. of the Internat. Workshop on Hardware-Software Codesign, October 1993.
[11] Clarke, E.M.; Grumberg, O.; Peled, D.A., Model checking, (2000), The MIT Press Cambridge, MA
[12] Courcoubetis, C.; Vardi, M.; Wolper, P.; Yannakakis, M., Memory-efficient algorithms for the verification of temporal properties, Formal methods system design, 1, 275-288, (1992)
[13] Emerson, E.A., Temporal and modal logic, (), 995-1072 · Zbl 0900.03030
[14] Finkel, A.; McKenzie, P., Verifying identical communicating processes is undecidable, Theoret. comput. sci., 174, 1-2, 217-230, (1997) · Zbl 0902.68127
[15] X. Fu, T. Bultan, J. Su, Conversation protocols: a formalism for specification and verification of reactive electronic services, in: Proc. Eighth Internat. Conf. on Implementation and Application of Automata, Lecture Notes in Computer Science, Vol. 2759, July 2003, pp. 188-200. · Zbl 1279.68210
[16] Garland, S.J.; Lynch, N., Using I/O automata for developing distributed systems, Foundations of component based systems, (2000), Cambridge University Press Cambridge
[17] P. Graunke, R.B. Findler, S. Krishnamurthi, M. Felleisen, Modeling web interactions, in: Proc. of 12th European Symp. on Programming, Lecture Notes in Computer Science, Vol. 2618, 2003, pp. 238-252. · Zbl 1032.68575
[18] J.E. Hanson, P. Nandi, S. Kumaran, Conversation support for business process integration, in: Proc. of Sixth IEEE Internat. Enterprise Distributed Object Computing Conference, 2002.
[19] Hoare, C.A.R., Communicating sequential processes, Commun. ACM, 21, 8, 666-677, (1978) · Zbl 0383.68028
[20] Hull, R.; Benedikt, M.; Christophides, C.; Su, J., E-servicesa look behind the curtain, (), 1-14
[21] IBM, Conversation support for agents, e-business, and component integration, http://www.research.ibm.com/convsupport/.
[22] Kahn, G., The semantics of a simple language for parallel programming, (), 471-475
[23] Liu, H.; Miller, R.E., Generalized fair reachability analysis for cyclic protocols, (), 192-204
[24] Lynch, N.; Tuttle, M., Hierarchical correctness proofs for distributed algorithms, (), 137-151
[25] Milner, R., Communicating and mobile systemsthe π-calculus, (1999), Cambridge University Press Cambridge
[26] Peng, W., Single-link and time communicating finite state machines, (), 126-133
[27] Pnueli, A.; Rosner, R., On the synthesis of a reactive module, (), 179-190
[28] A. Pnueli, R. Rosner, On the synthesis of an asynchronous reactive module, in: Proc. of 16th Internat. Colloq. on Automata, Languages, and Programs, Lecture Notes in Computer Science, Vol. 372, 1989, pp. 652-671. · Zbl 0686.68015
[29] S.K. Rajamani, J. Rehof, A behavioral module system for the pi-calculus, in: Proc. of Static Analysis Symposium (SAS), Lecture Notes in Computer Science, Vol. 2126, 2001, pp. 375-394. · Zbl 0997.68514
[30] Sun, Java Message Service. http://java.sun.com/products/jms/.
[31] Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/2002/NOTE-wsci-20020808/, August 2002.
[32] Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/wsdl, March 2001.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.