More Web Proxy on the site http://driver.im/

article

Conversation protocols: a formalism for specification and verification of reactive electronic services

Authors:

Jianwen SuAuthors Info & Claims

Theoretical Computer Science, Volume 328, Issue 1-2

Pages 19 - 37

https://doi.org/10.1016/j.tcs.2004.07.004

Published: 29 November 2004 Publication History

Abstract

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.

References

[1]

{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.]]

Digital Library

[2]

{2} P. Abdulla, B. Jonsson, Verifying programs with unreliable channels, Inform. Comput. 127 (2) (1996) 91-101.]]

[3]

{3} L.D. Alfaro, T.A. Henzinger, Interface automata, in: Proc. Ninth Annual Symp. on Foundations of Software Engineering, 2001, pp. 109-120.]]

Digital Library

[4]

{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.]]

Digital Library

[5]

{5} R. Alur, K. McMillan, D. Peled, Model-checking of correctness conditions for concurrent objects, Inform. Comput. 160 (2000) 167-188.]]

Digital Library

[6]

{6} Business Process Execution Language for Web Services (BPEL), Version 1.1. http://www.ibm.com/ developerworks/library/ws-bpel, May 2003.]]

[7]

{7} Business Process Modeling Language (BPML). http://www.bpmi.org.]]

[8]

{8} D. Brand, P. Zafiropulo, On communicating finite-state machines, J. ACM 30 (2) (1983) 323-342.]]

Digital Library

[9]

{9} T. Bultan, X. Fu, R. Hull, J. Su, Conversation specification: a new approach to design and analysis of e-service composition, in: Proc. 12th Internat. World Wide Web Conf., 2003, pp. 403-410.]]

Digital Library

[10]

{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]

{11} E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking, The MIT Press, Cambridge, MA, 2000.]]

[12]

{12} C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods System Design 1 (1992) 275-288.]]

Digital Library

[13]

{13} E.A. Emerson, Temporal and modal logic, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science: Volume B: Formal Models and Semantics, Elsevier, Amsterdam, 1990, pp. 995-1072.]]

Digital Library

[14]

{14} A. Finkel, P. McKenzie, Verifying identical communicating processes is undecidable, Theoret. Comput. Sci. 174 (1-2) (1997) 217-230.]]

Digital Library

[15]

{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.]]

Digital Library

[16]

{16} S.J. Garland, N. Lynch, Using I/O automata for developing distributed systems, Foundations of Component Based Systems, Cambridge University Press, Cambridge, 2000.]]

Digital Library

[17]

{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.]]

Digital Library

[18]

{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.]]

Digital Library

[19]

{19} C.A.R. Hoare, Communicating sequential processes, Commun. ACM 21 (8) (1978) 666-677.]]

Digital Library

[20]

{20} R. Hull, M. Benedikt, C. Christophides, J. Su, E-services: a look behind the curtain, in: Proc. 22nd ACM Symp. on Principles of Database Systems, 2003, pp. 1-14.]]

Digital Library

[21]

{21} IBM, Conversation support for agents, e-business, and component integration, http://www.research. ibm.com/convsupport/.]]

[22]

{22} G. Kahn, The semantics of a simple language for parallel programming, in: Proc. of IFIP 74, North-Holland, Amsterdam, 1974, pp. 471-475.]]

[23]

{23} H. Liu, R.E. Miller, Generalized fair reachability analysis for cyclic protocols, in: IEEE/ACM Transactions on Networking, 1996, pp. 192-204.]]

Digital Library

[24]

{24} N. Lynch, M. Tuttle, Hierarchical correctness proofs for distributed algorithms, in: Proc. Sixth ACM Symp. Principles of Distributed Computing, 1987, pp. 137-151.]]

Digital Library

[25]

{25} R. Milner, Communicating and Mobile Systems: the π-Calculus, Cambridge University Press, Cambridge, 1999.]]

Digital Library

[26]

{26} W. Peng, Single-link and time communicating finite state machines, in: Proc. of Second Internat. Conf. on Network Protocols, 1994, pp. 126-133.]]

[27]

{27} A. Pnueli, R. Rosner, On the synthesis of a reactive module, in: Proc. of 16th ACM Symp. Principles of Programming Languages, 1989, pp. 179-190.]]

Digital Library

[28]

{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.]]

Digital Library

[29]

{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.]]

Digital Library

[30]

{30} Sun, Java Message Service. http://java.sun.com/products/jms/.]]

[31]

{31} Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/2002/NOTE-wsci-20020808/, August 2002.]]

[32]

{32} Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/wsdl, March 2001.]]

Cited By

Di Stefano LDe Nicola RInverso O(2022)Verification of Distributed Systems via Sequential EmulationACM Transactions on Software Engineering and Methodology10.1145/349038731:3(1-41)Online publication date: 7-Mar-2022
https://dl.acm.org/doi/10.1145/3490387
Edixhoven LJongmans S(2022)Realisability of Branching PomsetsFormal Aspects of Component Software10.1007/978-3-031-20872-0_11(185-204)Online publication date: 10-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-20872-0_11
Coto ABarbanera FLanese IRossi DTuosto E(2022)On Formal Choreographic Modelling: A Case Study in EU Business ProcessesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_13(205-219)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_13
Show More Cited By

Index Terms

Conversation protocols: a formalism for specification and verification of reactive electronic services

Recommendations

Realizability of Choreographies Using Process Algebra Encodings

Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and ...
Analyzing Conversations of Web Services

A conversation is the global sequence of messages exchanged among the components of a distributed system. Conversations provide a promising model for specifying and analyzing the interactions among the peers participating to a composite Web service. In ...
From Security Protocols to Pushdown Automata

Formal methods have been very successful in analyzing security protocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying, for example, privacy-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 328, Issue 1-2

Implementation and application of automata

29 November 2004

211 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 29 November 2004

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Di Stefano LDe Nicola RInverso O(2022)Verification of Distributed Systems via Sequential EmulationACM Transactions on Software Engineering and Methodology10.1145/349038731:3(1-41)Online publication date: 7-Mar-2022
https://dl.acm.org/doi/10.1145/3490387
Edixhoven LJongmans S(2022)Realisability of Branching PomsetsFormal Aspects of Component Software10.1007/978-3-031-20872-0_11(185-204)Online publication date: 10-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-20872-0_11
Coto ABarbanera FLanese IRossi DTuosto E(2022)On Formal Choreographic Modelling: A Case Study in EU Business ProcessesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_13(205-219)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_13
Dai FChen HQiang ZLiang ZHuang BWang LZhang X(2020)Automatic Analysis of Complex Interactions in Microservice SystemsComplexity10.1155/2020/21287932020Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.1155/2020/2128793
Akroun LSalaün G(2018)Automated verification of automata communicating via FIFO and bag buffersFormal Methods in System Design10.1007/s10703-017-0285-852:3(260-276)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10703-017-0285-8
Farah ZAit-Ameur YOuederni MTari K(2017)A correct-by-construction model for asynchronously communicating systemsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0421-619:4(465-485)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10009-016-0421-6
Jongmans SArbab F(2016)Global consensus through local synchronizationScience of Computer Programming10.1016/j.scico.2015.09.001115:C(199-224)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1016/j.scico.2015.09.001
Jongmans SClarke DProença J(2016)A procedure for splitting data-aware processes and its application to coordinationScience of Computer Programming10.1016/j.scico.2014.02.017115:C(47-78)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1016/j.scico.2014.02.017
(2015)Choreographies in the wildScience of Computer Programming10.1016/j.scico.2014.11.015109:C(36-60)Online publication date: 1-Oct-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.11.015
Meyer APufahl LBatoulis KFahland DWeske M(2015)Automating data exchange in process choreographiesInformation Systems10.1016/j.is.2015.03.00853:C(296-329)Online publication date: 1-Oct-2015
https://dl.acm.org/doi/10.1016/j.is.2015.03.008
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents