On the Verification of Wireless Transaction Protocol Using SGM and RED

Pao-Ann Hsiung, Farn Wang, and Ruey-Cheng Chen
Institute of Information Science
Academia Sinica, Taipei, Taiwan.
( RTCSA'00, December 2000.)


The exponentially large sizes of state-spaces have been a major obstacle in formal verification, especially in model-checking, which are due to high process concurrency, and large constants that are compared to clock variables and to discrete variables. We show how an intelligent permutation of reduction techniques and a good selection of data-structures can be used to decrease the effect of the above explosion factors. First, a well-accepted experiment platform for the scalable verification of real-time systems, called State-Graph Manipulators, is used to verify Wireless Transaction Protocol (WTP), which is a part of a fast-permeating world standard, Wireless Application Protocol (WAP). Application results show how SGM handles large clock constants and large discrete constants efficiently. Second, a recently proposed Region Encoding Diagram (RED) technology is used to show how state-space size explosions due to high concurrency can be efficiently handled in WTP verification.