Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints
Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints
复制标题
具有图约束的基于目录的一致性协议的自动验证
DOI：
--
复制
发表时间：
2011
影响因子：
0.8
通讯作者：
Ahmed Rezine
中科院分区：
文献类型：
--
作者：
P. Abdulla;G. 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.