Title :
On the projection method for protocol verification
Author_Institution :
Dept. of Comput. Sci., Ottawa Univ., Ont., Canada
Abstract :
S.S. Lam and A.U. Shankar (1982) have proposed 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´ appears to mean that `the image protocol system is live (respectively, safe) if and only if the original protocol system is live (respectively, safe). It is shown that the `only if´ part is not true for certain liveness properties, and a remedy is suggested.
Keywords :
protocols; image protocol system; projection method; protocol verification; Fault tolerance; Fault tolerant systems; Protocols; Real-time systems; Software reliability; Timing; Projection method; protocol verification; safety and liveness properties;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1986.6312998
