formal specification and verification of a connection establishment protocol
This paper presents an exercise in the verification of a connection establishment protocol. A specification language named SPEX, tailored for the needs of communications protocols, is proposed, and its relation to a semi-automated verification system, AFFIRM, is discussed. This language is then used to specify a connection protocol currently being used. Certain errors are uncovered by analysis using the verification system. However, the major portion of the protocol's operation are shown to be correct.
formal specification verification connection paper exercise specification language language communication protocols relation systems errors analysis automation