ISSN:
1432-0452
Keywords:
Communication protocol
;
Formal model
;
Specification
;
Analysis
;
Formal description technique
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
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 5) states, while the system state analysis producesO(w 3) states. The system state analysis is then combined with an inductive proof, extending the analysis to all nonnegative integersw.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF02252957
Permalink