基于模型检测技术的XML乐观并发控制协议

XML optimistic concurrency control protocol based on model checking technology

XML并发控制协议可用于保证多个用户同时访问XML文档时的事务隔离性。由于XML数据的半结构化特点和访问接口的特殊性,现有XML并发控制协议随着文件规模的增大、并发客户的增多,系统事务性能大幅下降。基于模型检测技术提出了一种新的乐观并发控制协议XOCC-MC。通过将XML文档对应的DTD文档转换为系统模型,将事务操作中的XPath转换为CTL公式,利用模型求值判断节点间是否存在A/D关系,进而根据冲突矩阵判断事务之间的冲突关系。与现有乐观并发控制协议相比,XOCC-MC协议在文件规模大、并发客户数多的情况下表现出较好的事务性能。

XML concurrency control protocol can be used to ensure the isolation of transactions while multiple users accessing the same XML document concurrently. Due to the semi-structured characteristics and the particularity of access interface of XML data,the performance of existing XML concurrency control protocols reduce dramatically with the increase of file size and customer numbers. This paper proposed a new optimistic concurrency control protocol based on model checking technology （XOCC-MC）, which converted DTD corresponding XML document to system model, translated the XPaths to the CTL formulas, and used model evaluation result to judge whether there was an A/D relationship between nodes. Then it judged transaction conflicts according to the conflict matrix. Experimental results show that XOCC-MC has better performance than other protocols when the XML file size is large and the number of concurrent clients is more.