This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
PROSPEC: An Interactive Programming Environment for Designing and Verifying Communication Protocols
March 1988 (vol. 14 no. 3)
pp. 327-338

The PROSPEC software environment for designing and verifying communication protocols is described. It integrates several tools that implement methods for protocol verification and construction (i.e., fair reachability analysis, multiphase construction, and protocol projection). The system provides a unified graphical interface to facilitate the application of these methods and creates an interactive environment for specifying, verifying, and designing communication protocols. PROSPEC was used successfully to design and verify versions of BSC, X.21, X.25, and Telnet document transfer protocols.

[1] S. Aggarwal and R. P. Kurshan, "Automated Implementation from Formal Specification," inProtocol Specification, Testing, and Verification IV, Y. Yeminiet al., Eds. Amsterdam, The Netherlands: North-Holland, 1985.
[2] S. Aggarwal, D. Barbara, and K. Z. Meth, "SPANNER: A tool for the specification, analysis, and evaluation of protocols,"IEEE Trans. Software Eng., vol. SE-13, pp. 1218-1237, Aug. 1987.
[3] K. A. Bartlett, R. A. Scantlebury, and P.T. Wilkinson, "A note on reliable full-duplex transmission over half-duplex link,"Commun. ACM, vol. 12, no. 5, May 1969.
[4] T. P. Blumer and D. P. Sidhu, "Mechanical verfication and automatic implementation of communication protocols,"IEEE Trans. Software Eng., vol. SE-12, pp. 827-843, Aug. 1986.
[5] G. v. Bochmann, "Finite state description of communication protocols,"Comput. Networks, vol. 2, no. 4/5, pp. 361-372, Oct. 1978.
[6] G. V. Bochmann and C. A. Sunshine, "Formal methods in communication protocol design,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 624-631, Apr. 1980.
[7] G. v. Bochmannet al., "Experience with formal specifications using an extended state transition model,"IEEE Trans. Commun., vol. COM-30, pp. 2506-2513, Dec. 1982.
[8] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323-342, Apr. 1983.
[9] T. Y. Choi and R. E. Miller, "A decomposition method for the analysis and design of finite state protocols," inProc. 8th Data Commun. Symp., Oct. 1983, pp. 167-176.
[10] T. Y. Choi, "Formal techniques for the specification, verification and construction of communication protocols,"IEEE Commun. Mag., vol. 23, no. 10, pp. 46-52, Oct. 1985.
[11] C. Chow, M. Gouda, and S. Lam, "An exercise in constructing multi-phase communication protocols," inProc. ACM SIGCOMM'84, 1984, pp. 42-47.
[12] C. H. Chow, M. G. Gouda, and S. S. Lam, "A discipline for constructing multi-phase communicating protocols,"ACM Trans. Comput. Syst., vol. 3, no. 4, pp. 315-343, Nov. 1985.
[13] C.-H. Chow, "A discipline for verification and modular construction of communication protocols," Ph.D. dissertation, Dep. Comput. Sci., Univ. Texas at Austin, Dec. 1985.
[14] C.-H. Chow, "Using PROSPEC to design and verify communication protocols," inProc. GLOBCOM '86, Dec. 1986.
[15] E. Clarke, "Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach," inProc. 10th ACM Symp. Princ. Programming Languages, 1983, pp. 117-127.
[16] D. M. Cohen and E. J. Isganitis, "Automatic generation of a prototype of a new protocol from its specification," inProceeding of GLOBECOM '86, Dec. 1986.
[17] M. G. Gouda, "An example for constructing communicating machines by stepwise refinement," inProc. 3rd IFIP Workshop Protocol Specification Testing, and Verification, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: North-Holland, 1983, pp. 63- 74.
[18] M. G. Gouda and Y. T. Yu, "Protocol validation by maximal progress state exploration,"IEEE Trans. Commun., vol. COM-32, pp. 94-97, Jan. 1984.
[19] 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.
[20] M. G. Gouda, C. H. Chow, and S. S. Lam, "On the decidability of livelock detection in networks of communicating finite state machines," inProc. 4th Int. Workshop Protocol Specification, Testing and Verification, June 1984.
[21] M. G. Gouda and Y. T. Yu, "Synthesis of communicating finite state machines with guaranteed progress,"IEEE Trans. Comput., vol. C-32, no. 7, pp. 779-788, 1984.
[22] 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.
[23] C.-T. Hsieh, "Models and algorithms for the design of store-and-forward communication networks," Ph.D. dissertation, Dep. Comput. Sci., Univ. Texas at Austin, 1987.
[24] S. S. Lam, "Data link control procedures," inComputer Communications, Vol. 1, Principles, W. Chou, Ed. Englewood Cliffs, NJ: Prentice-Hall, 1983, ch. 3, pp. 81-113.
[25] S. S. Lam and A. U. Shankar, "Protocol verification via projections,"IEEE Trans. Software Eng., vol. SE-10, no. 4, pp. 325-342, July 1984.
[26] S. S. Lam, C.-H. Chow, M. G. Gouda, and A. U. Shankar, "Interactive verification and construction of communication protocols in PROSPEC," inProc. IEEE INFOCOM'86, 1986, pp. 67-75.
[27] S. S. Lam, "Protocol conversion," Technical Report TR-87-05, Dep. Comput. Sci., Univ. Texas at Austin, Feb. 1987; see alsoIEEE Trans. Software Eng., this issue, pp. 353-362.
[28] C. V. Ramamoorthy, S. T. Dong, and Y. Usuda, "An implementation of an automated protocol synthesizer (APS) and its application to the X.21 protocol,"IEEE Trans. Software Eng., vol. SE-11, no. 9, pp. 886-908, Sept. 1985.
[29] R. R. Razouk and G. Estrin, "Modeling and verification of communication protocols in SARA: The X.21 interface,"IEEE Trans. Comput., vol. C-29, no. 12, pp. 1038-1052, Dec. 1980.
[30] R. Razouk, "Modeling X.25 using the graph model of behavior," inProc. 2nd Int. Workshop Protocol Specification, Testing and Verification, May 1982.
[31] J. Rubin and C. H. West, "An improved protocol validation technique,"Comput. Networks, Apr. 1982.
[32] L. E. Rosier and M. G. Gouda, "Deciding progress for a class of communicating finite state machines," inProc. Conf. Information Sciences and Systems, Princeton Univ., 1984.
[33] A. U. Shankar and S. S. Lam, "An HDLC protocol specification and its verification using image protocols,"ACM Trans. Comput. Syst., vol. 1, no. 4, pp. 321-368, Nov. 1983.
[34] M. Sherman and H. Rudin, "Using automated validation techniques to detect lockups in packet switched networks,"IEEE Trans. Commun., vol. COM-30, pp. 1762-1767, July 1982.
[35] C. Sunshine, "Formal techniques for protocol specification and verification,"Computer, vol. 12, no. 9, pp. 20-27, Sept. 1979.
[36] C. H. West and P. Zafiropulo, "Automated validation of a communications protocol: The CCITT X.21 recommendations,"IBM J. Res. Develop., vol. 22, pp. 60-71, Jan. 1978.
[37] Y. T. Yu and M. G. Gouda, "Deadlock detection for a class of communicating finite state machines,"IEEE Trans. Commun., vol. COM- 30, no. 12, pp. 2514-2518, Dec. 1982.
[38] Y. T. Yu and M. G. Gouda, "Unboundedness detection for a class of communicating finite-state machines,"Inform. Processing Lett., vol. 17, pp. 235-240, Dec. 1983.
[39] P. Zafiropouloet al., "Towards analysing and synthesizing protocols,"IEEE Trans. Commun., vol. COM-28, pp. 655-660, Apr. 1980.

Index Terms:
communication protocols verification; specification; PROSPEC; interactive programming environment; fair reachability analysis; multiphase construction; protocol projection; graphical interface; BSC; X.21; X.25; Telnet document transfer protocols; interactive programming; programming environments; protocols; software tools
Citation:
C.H. Chow, S.S. Lam, "PROSPEC: An Interactive Programming Environment for Designing and Verifying Communication Protocols," IEEE Transactions on Software Engineering, vol. 14, no. 3, pp. 327-338, March 1988, doi:10.1109/32.4653
Usage of this product signifies your acceptance of the Terms of Use.