This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Relational Algebraic Approach to Protocol Verification
February 1988 (vol. 14 no. 2)
pp. 184-193

Communications protocols are usually modeled by a pair of finite-state machines that generate the interaction between processes. Protocol verification is a procedure to validate the logical correctness of these interaction sequences and to detect potential design errors. A relational approach is proposed to represent a finite-state machine as a transition table. On this basis, the well-established theory of relational databases can be utilized to derive the global-state transitions of the system. Furthermore, logical errors of a protocol such as deadlocks, incomplete specifications and nonexecutable interactions can be formulated in terms of relational algebra. This approach has been implemented on the INGRES database system and applied to the verification of several protocols.

[1] 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.
[2] G. V. Bochmann, "Finite description of communication protocols," inComputer Networks 2. Amsterdam, The Netherlands: North-Holland, pp. 361-372.
[3] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323-342, Apr. 1983.
[4] E. F. Codd, "A relational model of data for large shared data banks,"Commun. ACM, pp. 377-387, June 1970.
[5] E. F. Codd, "Relational completeness of database sublanguages," inData Base Systems(Courant Inst. Computer Symp. 6). R. Rustin Ed. Englewood Cliffs, NJ: Prentice-Hall, 1972, pp. 65-98.
[6] D. Maier,The Theory of Relational Databases. Rockville, MD: Computer Science Press, 1983.
[7] D. Skeen and M. Stonebraker, "A formal model of crash recovery in a distributed system,"IEEE Trans. Software Eng., vol. SE-93 no. 3, pp. 219-228, May 1983.
[8] M. Stonebraker,et al., "The design and implementation of INGRES,"ACM Trans. Database Syst., vol. 1, no. 3, Sept. 1976.
[9] C. A. Sunshine, "Survey of protocol definition and verification techniques," inComputer Networks 2. Amsterdam. The Netherlands: North-Holland, 1978, pp. 346-350.
[10] C. W. West and P. Zafiropulo, "Automated validation of a communications protocol: The CCITTX.21 recommendations,"IBM J. Res. Develop., vol. 22, no. 1, pp. 60-71, Jan. 1978.
[11] P. Zafiropulo, "Protocol validation by duologue-matrix analysis,"IEEE Trans. Commun., vol. COM-26, no. 8, pp. 1187-1193, Aug. 1978.
[12] P. Zafiropouloet al., "Towards analysing and synthesizing protocols,"IEEE Trans. Commun., vol. COM-28, pp. 655-660, Apr. 1980.
[13] Recommendations X.21 (Revised), Pub. by CCITT (International Telegraph and Telephone Consultative Committee), Geneva, Switzerland, Rep. AP VI-No. 55-E, Mar. 1976.
[14] SUN MicroINGRES Manual (Version 2.0), Microsystem Inc., Aug. 1984.

Index Terms:
protocol verification; logical correctness; finite-state machine; transition table; relational databases; global-state transitions; deadlocks; INGRES; database theory; finite automata; program verification; protocols; relational databases
Citation:
T.T. Lee, M.Y. Lai, "A Relational Algebraic Approach to Protocol Verification," IEEE Transactions on Software Engineering, vol. 14, no. 2, pp. 184-193, Feb. 1988, doi:10.1109/32.4637
Usage of this product signifies your acceptance of the Terms of Use.