Protocol verification using relational algebra

Quynh-Anh Nguyen and Marcus A. Maloof

A communication protocol is a set of rules governing data exchange between two communicating processes. Specification of these protocols is critical for ensuring an error-free framework for implementing and executing communication systems. The purpose of protocol verification is to test protocol specifications and detect any operative errors. Due to the important roles communication protocols play in today's world of information processing, it is vital that they are specified and verified in the most effective and efficient means. Finite-state machines provide a natural model for specifying protocols. When represented using transition tables, which correspond directly to a relational data model, the algorithms necessary to verify protocols can be specified in relational algebra. This paper describes a system that represents protocols as relations and implements protocol verification algorithms using relational algebra in a logic programming framework. Using this system, experiments were conducted on several synthetic communication protocols to determine if the protocols were well-behaved.

Paper available in PostScript (gzipped) and PDF.

Nguyen, Q.-A., & Maloof, M.A. (1993). Protocol verification using relational algebra. Proceedings of the 23rd Annual Virginia Computer User's Conference, 47–51. Blacksburg, VA: Department of Computer Science, Virginia Tech.

@inproceedings{nguyen.vcuc.93,
  author = "Nguyen, Q.-A. and Maloof, M.A.",
  title = "Protocol verification using relational algebra",
  booktitle = "{Proceedings of the Twenty-third Annual Virginia Computer
    User's Conference}",
  year = 1993,
  pages = "47--51",
  publisher = "Department of Computer Science, Virginia Tech",
  address = "Blacksburg, VA"
}