FORMAL MODELS OF COMMUNICATION SERVICES - A CASE-STUDY

Recent work on communication systems has considered a rich variety of services, each providing users or application programmers with a distinctive functionality. The communication system will change over time. as new technology allows improved performance. Users will also need to choose between variations of supplied functionalities. For these reasons. it is important that the system describe services separately from the details of the protocol that provides them. That is, an ''abstraction barrier'' must exist between users and service providers. Designers can provide this by specifying a service in a formal method, just as particular protocols have traditionally been specified. Particular protocols must also provide the service that they claim. This article illustrates how formal methods can be used to describe (and reason about) these advanced services. Several systems have proposed a multicast primitive, in which an application can send a message to more than one destination at a time. In the Isis system, several different multicast primitives provide different guarantees about relative order of delivery between messages. The author presents a simplified atomic multicast as an example service and Input/Output Automata for the formal model. He shows how to represent the service specification, a protocol, and implementations of that protocol. He also sketches how to prove the correctness of the protocol and implementation, that is, how to show that the specified service is actually provided.