基于模型检查的XML Schema特征提取

XML SCHEMA CONSTRAINTS EXTRACTION BASED ON MODEL CHECKING

XQuery用于查询XML文档,对XQuery查询优化有助于提高查询效率,有重要的研究意义。树模式把XQuery表示成树结构的查询,如何基于XML Schema对树模式进行优化是当前的研究热点,需要利用XML Schema的一些特征进行树模式优化,因此如何自动提取XML Schema的特征是需要解决的问题。提出基于模型检查的XML Schema特征提取方法。首先把XML Schema转换成Schema图,进而转换成模型检查器NuSMV的输入模型,从而可以对时态逻辑公式表示的XML Schema特征进行检查,提取的孩子关系以及子孙关系特征可以用于树模式优化。

XQuery is used in querying the XML documents,the optimisation of XQuery can help to improve the efficiency of query,therefore has the research significance.Tree pattern expresses the XQuery query as the tree structure query,how to optimise tree pattern based on XML Schema is the research focus at present,there is the need to utilise some of XML Schema constraints to optimise the tree pattern.Therefore,how to extract Schema constraints automatically is a problem to be solved.We propose a method of XML Schema constraints extraction based on model checking.Specifically,the XML Schema is transformed into Schema graph first,and then transformed into the input model of model checker NuSMV,thus,we can check the XML Schema constraints expressed in temporal logic formula,and the child and descendant relations being extracted can be used to optimise the tree pattern.