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

101Citations
Citations of this article
36Readers
Mendeley users who have this article in their library.

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. © 2004 Elsevier B. V. All rights reserved.

Cite

CITATION STYLE

APA

Fu, X., Bultan, T., & Su, J. (2004). Conversation protocols: A formalism for specification and verification of reactive electronic services. In Theoretical Computer Science (Vol. 328, pp. 19–37). https://doi.org/10.1016/j.tcs.2004.07.004

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free