Integrated Methods for Protocol Specification and Verification
Benedetto L. DiVito · 1982
A methodology for the formal specification and deductive verification of protocols is presented. Protocol modules are modeled as sequential processes and abstract behavioral specifications are given for each. In concurrent systems such processes are connected by buffers and communicate by passing messages, as in the Gypsy model of concurrency. Methods similar to those of Gypsy for verifying safety properties are discussed and illustrated with an example, the data transfer protocol introduced by Stenning. The methodology is geared toward the use of automated verification technology. A fully mechanical proof of the example in this paper was obtained using the Boyer-Moore theorem prover. 2 1