Automatic Verification of Directory-Based Consistency Protocols
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 Proceedings of the 3rd Workshop on Reachability Problems (RP), 2009,
Last version (pdf) 2009