Verification of a revised WAP wireless transaction protocol

The Wireless Transaction Protocol (WTP) is part of the Wireless Application Protocol (WAP) architecture and provides a reliable request-response service. The state space method of Coloured Petri Nets has been used to analyse a revised version of WTP, to gain a high level of confidence in the correctness of the design. Full state space analysis allows us to prove properties of the protocol for maximum values of the retransmission counters used in GSM networks (values are 4). However, the size of the state space grows rapidly as the maximum counter values are increased. We apply the sweep-line method to take advantage of the progress present in the protocol, notably the progression through major states of the protocol entities, and the increasing nature of the retransmission counters. The sweep-line method allows us to prove properties of the protocol for larger counter values, including those used in Internet Protocol (IP) networks (where the maximum values are 8). As a result, verification of WTP can be performed for the two most important networks (GSM and IP), the ones for which the WAP standard gives recommended maximum values for the retransmission counters.