Verification of the WAP Transaction Layer Using the Model Checker SPIN

Yu-Tong He


This report presents a formal methodology of formalizing and verifying the Transaction Layer Protocol (WTP) design in the Wireless Application Protocol (WAP) architecture. Corresponding to the Class 2 Transaction Service (TR-Service) definition and the Protocol (TR-Protocol) design, two models at different abstraction levels are built with a finite state automation (FSA) formalism. By using the model checker SPIN, we uncover defects in a latest approved version of the TR-Protocol design, which can lead to deadlock, channel buffer overflow and unfaithful refinement of the TR-Service definition. As an extended result, a set of safety, liveness and temporal properties is verified for the WTP to be operating in a more general environment which allows for loss and re-ordering messages.