This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
On Conditions for Defining a Closed Cover to Verify Progress for Communicating Finite State Machines
November 1989 (vol. 15 no. 11)
pp. 1491-1494
The closed cover technique is a technique for verifying progress for two communicating finite state machines exchanging messages over two lossless and FIFO channels. It was first introduced by Gouda. A set of global states is called a closed cover if it satisfies some conditions given in Gouda?s paper, but an intuitive description of why one of the conditions is necessary is not provided. It is found that the definition of a closed cover is too restrictive in one paper and incorrect in the other. This correspondence clarifies this and suggests improved definitions for a closed cover which are increasingly less restrictive.

[1] M. G. Gouda, "Closed covers: To verify progress for communicating finite state machines,"IEEE Trans. Software Eng., vol. SE-10, no. 6, pp. 846-855, Nov. 1984.
[2] M. G. Gouda and C. K. Chang, "Proving liveness for networks of communicating finite state machines,"ACM Trans. Program. Languages and Syst., vol. 8, no. 1, pp. 154-182, Jan. 1986.
[3] M. G. Gouda, L. E. Rosier, and H.-C. Yen, "A theory of closed covers: To decide progress of communicating finite state machines," inProc. 23rd Annu. Allerton Conf. Communication, Control, and Computing, Urbana, IL, Oct. 1985, pp. 914-922.
[4] T. Y. Choi and R. E. Miller, "Protocol analysis and synthesis by structured partitions,"Comput. Networks ISDN Syst., vol. 11, pp. 367- 381, 1986.

Index Terms:
progress verification; closed cover; communicating finite state machines; lossless; FIFO channels; structural partition technique; finite automata; protocols
Citation:
A. Chung, D.P. Sidhu, "On Conditions for Defining a Closed Cover to Verify Progress for Communicating Finite State Machines," IEEE Transactions on Software Engineering, vol. 15, no. 11, pp. 1491-1494, Nov. 1989, doi:10.1109/32.41341
Usage of this product signifies your acceptance of the Terms of Use.