Policy Analysis and Verification by Graph Transformation Tools

Policies are used to control the behavior of large-scale systems. After policies are designed and before policies are implemented, it should be possible to analyze the policies and verify that they behave as expected. Graph transformations provide a good method to carry out the analysis and verification because of the intuitive representation of policies and the mature theory. Here, we show how graph transformations can simulate PONDER policies and use the graph tools AGG and GROOVE to do the static and dynamic analysis.