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.