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

XML SCHEMA CONSTRAINTS EXTRACTION BASED ON MODEL CHECKING

作　　者：刘科[1] 杨红丽[1] 廖湖声[1] 吕关锋[1] 高雁飞[2] 

机构地区：[1]北京工业大学,北京100124 [2]北京建筑工程学院,北京100044

出　　处：《计算机应用与软件》2012年第11期160-164,共5页Computer Applications and Software

基　　金：北京市自然科学基金项目(4082003);中科院软件所项目(40007012201106);北京市教育委员会科研计划面上项目(KM201010016003)

摘　　要：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.

关 键 词：模型检查 时态逻辑公式 XML SCHEMA Schema特征 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]