University of Texas at Austin Department of Computer Sciences
Networking Research Laboratory
Department of Computer Sciences
The University of Texas at Austin

Director: Simon S. Lam (more publications)

A Relational Notation for State Transition Systems

Simon S. Lam and A. Udaya Shankar

The relational notation has two basic constructs: state formulas that represent sets of states, and event formulas that represent sets of state transitions. A relational specification consists of a state transition system, given in the relational notation, and a set of fairness assumptions. We present a theory of refinement of relational specifications. Several refinement relations between specifications are defined. To illustrate our concepts and methods, three specifications of the alternating-bit protocol are given. We also apply the theory to explain "auxiliary variables." Other applications of the theory to protocol verification, composition, and conversion are discussed. Our approach is compared with the approaches of other authors.

Index Terms:
Communication protocols, distributed systems, fairness, projection mapping, refinement, specification, temporal logic, auxiliary variables
* A. Udaya Shankar is on the faculty of the Department of Computer Science, University of Maryland, College Park
Authors' Note:
This paper subsumes our Protocol Verification via Projections paper published in the 1984 issue of IEEE-TSE. Both papers are concerned with the refinement mappings between a protocol with multiple functions, say A, and a set of simple protocols which together provide the functions of A. In the 1984 paper, the simple protocols are called image protocols of A. In this paper, A is said to be a refinement of each of the simple protocols. The protocol example at the end of this paper provides a good illustration of how to use invariants to encode refinement mappings.