Title :
Protocol Verification via Projections
Author :
Lam, Simon S. ; Shankar, A.Udaya
Author_Institution :
Department of Computer Science, University of Texas, Austin, TX 78712.
fDate :
7/1/1984 12:00:00 AM
Abstract :
The method of projections is a new approach to reduce the complexity of analyzing nontrivial communication protocols. A protocol system consists of a network of protocol entities and communication channels. Protocol entities interact by exchanging messages through channels; messages in transit may be lost, duplicated as well as reordered. Our method is intended for protocols with several distinguishable functions. We show how to construct image protocols for each function. An image protocol is specified just like a real protocol. An image protocol system is said to be faithful if it preserves all safety and liveness properties of the original protocol system concerning the projected function. An image protocol is smaller than the original protocol and can typically be more easily analyzed. Two protocol examples are employed herein to illustrate our method. An application of this method to verify a version of the high-level data link control (HDLC) protocol is described in a companion paper.
Keywords :
Communication system control; Computer languages; Control systems; Image analysis; Protocols; Safety; Transfer functions; Communicating processes; communication protocols; distributed systems; image protocols; message-passing networks; method of projections; protocol analysis; verification;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1984.5010246