Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints

Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine

We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings.

In International Journal of Foundations of Computer Science, 2011,

Last version (pdf) 2011