Consequently workstation memory and computer power are often overwhelmed by the sheer number and size of the underlying system states. State exploration can therefore only be performed on very small systems.
|
A problem immediately arises: It is not usual
for real life systems of even modest complexity to have hundreds of
millions of underlying states, with each state requiring hundreds of
bytes of storage space.
Consequently workstation memory and computer power are often overwhelmed by the sheer number and size of the underlying system states. State exploration can therefore only be performed on very small systems. |
 |
We tackle this problem in two ways:
Firstly, we use a probabilistic storage technique based on hash compaction. This technique has a very low memory usage that depends only on the number of states, not on their size. Secondly, we implement our state generator in parallel to exploit the memory and processing power of a network of workstations or a parallel computer (e.g. the Fujitsu AP3000). |