Information Assurance

9.9. Future Work and Conclusion

We are now producing scenario graphs so large that humans have a hard time interpreting them. We plan to address the problem of size in several ways:

• Apply optimization techniques from the model checking literature to reduce the size of scenario graphs. For example, we can use symmetry and partial-order reduction techniques. One open problem is what a set of “all counterexamples” means when using the counterexample-guided abstraction and refinement model checking technique.

• Find ways to compress either or both the internal representation of the scenario graph and the external one displayed to the user.

  • One novel approach we took was to apply the Google PageRank algorithm to the graphs we produce [27]. We use the ...