UC Santa Barbara

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 Buchi 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 axe 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 axe verified on the Buchi automaton specification, (3) The peer implementations axe synthesized from the protocol via projection.