| Why
different? |
|
|
|
|
|
|
|
|
|
|
|
| • | Z-like
specifications are not suitable for direct |
|||||||||
| model
checking |
||||||||||
| • | The
primary problem is that the data structures are |
|||||||||
| generally
unbounded, taking the problem out of |
||||||||||
| the
realm of model checking |
||||||||||
| • | Even
simple bounded data structures generally |
|||||||||
| cause
massive state space explosions |
||||||||||
| • | Abstraction
into a model-checkable problem is |
|||||||||
| feasible,
but not generally possible to automate |
||||||||||
