Journal
THEORETICAL COMPUTER SCIENCE
Volume 328, Issue 1-2, Pages 19-37Publisher
ELSEVIER SCIENCE BV
DOI: 10.1016/j.tcs.2004.07.004
Keywords
E-service; asynchronous communication; communicating finite state automata; conversation protocol; realizability; composition; verification
Categories
Ask authors/readers for more resources
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 Buchi 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 Buchi automaton, (2) The properties of the protocol are verified on the Buchi automaton specification, and (3) The peer implementations are synthesized from the protocol via projection. (C) 2004 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available