This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
On the projection method for protocol verification
Nov. 1986 (vol. 12 no. 11)
pp. 1088-1089
To-Yat Cheung, Distributed Computing Research Group, Department of Computer Science, University of Ottawa, Ottawa, Ont., Canada K1N 9B4
Shankar and Lam propose a projection method for protocol verification. They claim that the method guarantees the faithfulness of the safety and liveness properties of a protocol system. Although not clearly defined, “faithfulness” (as implied in many places in their article) means “the image protocol system is live (respectively, safe) if and only if the original protocol system is live (respectively, safe).” This paper shows that the “only if” part is not true for certain liveness properties and suggests a remedy.
Index Terms:
Protocols,Real-time systems,Timing,Software reliability,Fault tolerance,Fault tolerant systems,safety and liveness properties,Projection method,protocol verification
Citation:
To-Yat Cheung, "On the projection method for protocol verification," IEEE Transactions on Software Engineering, vol. 12, no. 11, pp. 1088-1089, Nov. 1986, doi:10.1109/TSE.1986.6312998
Usage of this product signifies your acceptance of the Terms of Use.