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
Abstract
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.