This paper discusses a case study on the formal verification of a realistic and useful protocol, in the wireless applications domain. The protocol considered is the wireless transaction protocol (WTP) of wireless application protocol (WAP) 2.0. The verification is carried out using the well-known model checking tool Spin. An interesting aspect of the work is that the verification exercise revealed certain bugs in the protocol, thereby establishing the utility of formal verification. A corrected version of the protocol is shown to satisfy all the requirements of the protocol.

The paper is very useful for those interested in knowing more about formal verification, and in applying these methods for other protocols.

The various issues involved in the formal verification of protocols are clearly discussed, to a reasonable extent. Though it is beyond the scope of a journal paper to provide complete details of verification, sufficient details are given to help readers understand the issues and complexity of the verification task. Certain methodological issues for formal verification are also discussed at the end of the paper, which would be useful for beginners in the area. The superiority of the Spin tool is also well explained, using a detailed comparison of the verification effort with another tool.

The paper could have been proofread better; there are some typographical errors. Section 3.1 elaborates on five basic elements in the WAP protocol design, and it is stated at the beginning of Section 3.2 that these five elements would be incorporated in the formalization. However, I could not see this clearly, in particular, how the assumption and the protocol service definitions are formalized.

Overall, this is an interesting paper, discussing an interesting and useful application of formal verification using the Spin tool.