Information Assurance

9.7. Practical Experience

9.7.1. Performance

In practice we found that the explicit-state algorithm has good performance: the speed to generate the attack graph is linear in the number of reachable state transitions [3]. We also found that for our limited number of examples, our explicit-state algorithm is better than our symbolic algorithm in terms of time to generate graphs. In all of our examples, our models are large due to their large number of state variables, but at the same time they have a very small reachable state space. Thus, we have a double whammy against the symbolic algorithm: smaller reachable state spaces are better for explicit-state model checking, and larger numbers of state variables are worse for symbolic model checking. ...