DocumentCode :
970215
Title :
Protocol Verification via Projections
Author :
Lam, Simon S. ; Shankar, A.Udaya
Author_Institution :
Department of Computer Science, University of Texas, Austin, TX 78712.
Issue :
4
fYear :
1984
fDate :
7/1/1984 12:00:00 AM
Firstpage :
325
Lastpage :
342
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;
fLanguage :
English
Journal_Title :
Software Engineering, IEEE Transactions on
Publisher :
ieee
ISSN :
0098-5589
Type :
jour
DOI :
10.1109/TSE.1984.5010246
Filename :
5010246
Link To Document :
بازگشت