A relational algebraic approach to protocol verification

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