Processes participating in a communications protocol are usually modeled by finite-state machines interacting each other. Protocol verification is a procedure to validate the logic correctness of these interaction sequences and detect the potential design errors. A relational approach is proposed to represent a finite-state machine as a transition relation. On this basis, relational algebra can be utilized to derive the global-state transitions of the system. Furthermore, the logic errors of the protocol such as deadlocks, incomplete specifications and nonexecutable interactions can all be formulated in terms of relational algebra. This approach has been implemented on the INGRES and DBASE-III database systems running on various machines and applied to the verification of several protocols including the CCITT X.21. Protocol verification represents a non-traditional data processing application of relational database systems.
展开▼
