Issue No. 11 - Nov. (1986 vol. 12)
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.
Protocols, Real-time systems, Timing, Software reliability, Fault tolerance, Fault tolerant systems, safety and liveness properties, Projection method, protocol verification
T. Cheung, "On the projection method for protocol verification," in IEEE Transactions on Software Engineering, vol. 12, no. , pp. 1088-1089, 1986.