Specification and analysis of a data transfer protocol using systems of communicating machines

Summary A model for communication protocols calledsystems of communicating machines is used to specify a data transfer protocol with variable window size (e.g., HDLC), which is an arbitrary nonnegative integer, and to analyze it for freedom from deadlocks. The model uses a combination of finite state machines and variables. This allows the size of the specification (i.e., number of states and variables) to be linear in the window size, a considerable reduction from the pure finite state machine model. A new type of analysis is demonstrated which we callsystem state analysis. This is similar to thereachability analysis used in the pure finite state model, but it provides substantial simplication by reducing the number of states generated. For example, with the protocol in this paper, ifw is the window size, then the global analysis producesO(w ⁵) states, while the system state analysis producesO(w ³) states. The system state analysis is then combined with an inductive proof, extending the analysis to all nonnegative integersw. Gilbert M. Lundy, Jr was born in New Orleans, Louisiana, in 1954. After completing schools in Plano, Texas, he attended Texas A & M University, receiving the B.A. in mathematics (1976). From 1977–81 he served as a Lieutenant in the U.S. Army, based at Fort Ord, California. From 1981–84 he was a software engineer at E-Systems, in Dallas, Texas. During this period he also completed the M.S. program in Computer Science at the University of Texas at Dallas. From 1984 to 1988, he was a graduate student at Georgia Institute of Technology, receiving the Ph.D. in 1988. His research was in the formal modeling of communication protocols for computer networks. Since September 1988, he has been an Assistant Professor of computer science at the U.S. Naval Postgraduate School in Monterey, CA. He teaches classes and performs research in computer networks and communications. Raymond E. Miller received his Ph.D. degree from the University of Illinois, Urbana-Champaign, in 1957. He was a Research Staff Member at IBM Thomas J. Watson Research Center, Yorktown, Heights, NY, from 1957 to 1980, Director of the School of Information and Computer Science at Georgia Tech from 1980 to 1987, and is currently a Professor of Computer Science at the University of Maryland, College Park, and Director of the NASA Center of Excellence in Space Data and Information Sciences at Goddard Space Flight Center. He has written over 90 technical papers in areas of theory of computation, machine organization, parallel computation, and communication protocols. Dr. Miller is a Fellow of the American Association for the Advancement of Science, a Fellow of the IEEE and a member of ACM. Among his numerous society activities he served as an ACM Council Member-at-Large from 1976–1982, Editor in Chief of the Journal of the ACM from 1972–1976, a Board Member of the Computing Research Association from 1983–1991, and President of the Computing Sciences Accreditation Board from 1985–1987. Currently he is a member of the Board of Governors of the IEEE Computer Society and Vice President for Educational Activities.This research was performed while the authors were at Georgia Institute of Technology