摘要: The method of projections is a new approach to reduce the complexity analyzing nontrivial communication protocols. A protocol system consists network entities and channels. Protocol interact by exchanging messages through channels; in transit may be lost, duplicated as well reordered. Our intended for protocols with several distinguishable functions. We show how construct image each function. An specified just like real protocol. said faithful if it preserves all safety liveness properties original concerning projected smaller than can typically more easily analyzed. Two examples are employed herein illustrate our method. application this verify version high-level data link control (HDLC) described companion paper.
sci-hub.se 参考文章(15)
Simon S Lam, A. Udaya Shankar, VERIFICATION OF COMMUNICATION PROTOCOLS VIA PROTOCOL PROJECTIONS. ,(1982)
A. Udaya Shankar, Simon S. Lam, An Illustration of Protocol Projections Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 343- 360 ,(1982)
A. Udaya Shankar, Simon S. Lam, PROTOCOL PROJECTIONS: A METHOD FOR ANALYZING COMMUNICATION PROTOCOLS. IEEE. ,(1981)
James F. Kurose, The Specification and Verification of a Connection Establishment Protocol Using Temporal Logic Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 43- 62 ,(1982)
Rami R. Razouk, Modeling X.25 Using the Graph Model of Behavior Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 197- 214 ,(1982)
Simon S. Lam, A. Udaya Shankar, On Time-Dependent Communication Protocols and Their Projections Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 215- 235 ,(1982)
Lansing Sloan, Mechanisms that enforce bounds on packet lifetimes ACM Transactions on Computer Systems. ,vol. 1, pp. 311- 330 ,(1983) , 10.1145/357377.357382
Daniel Brand, William H Joyner, Verification of protocols using symbolic execution Computer Networks. ,vol. 2, pp. 351- 360 ,(1978) , 10.1016/0376-5075(78)90014-4
Gregor V. Bochmann, Finite state description of communication protocols Computer Networks. ,vol. 2, pp. 361- 372 ,(1978) , 10.1016/0376-5075(78)90015-6
P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand, Towards Analyzing and Synthesizing Protocols IEEE Transactions on Communications. ,vol. 28, pp. 651- 661 ,(1980) , 10.1109/TCOM.1980.1094687