Issue No. 02 - February (1988 vol. 14)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.4637
<p>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.</p>
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
T. Lee and M. Lai, "A Relational Algebraic Approach to Protocol Verification," in IEEE Transactions on Software Engineering, vol. 14, no. , pp. 184-193, 1988.