Web服务XML文档的子模式关系建模与计算复杂度分析

理论计算机科学电子笔记162（2006）147-152www.elsevier.com/locate/entcs一种用于Web服务的Samuele Carpineti1 Cosimo Laneve2博洛尼亚大学计算机科学系Mura Anteo Zamboni，7，40127 Bologna，Italy摘要最近提出了几种模式语言来描述XML文档。这种语言的关键概念是用于类型检查的子模式关系我们提出了一个模式语言的建模XML文档包含通道模式（输入和输出）的能力，我们描述了两个子模式算法。第一个使用模拟关系;第二个检查模式的结构。我们证明了算法的等价性，并讨论了它们的计算复杂度。关键词：Web服务，契约，XML类型，子类型1引言最近已经提出了几种语言来描述XML文档的树结构，通常称为模式。最流行的建议是DTD、XML-Schema、RELAX NG和正则表达式类型[4]。这些建议主要是因为它们的表达能力（由语言描述的树的集合）和子模式的概念，它定义了模式之间的关系（偏序）。在这些建议中，正则表达式类型是一种简单而强大的语言，具有基于包含树集的可判定子模式关系。 众所周知，这种子模式关系在计算上是昂贵的正则表达式不能充分描述Web服务交换的XML文档。事实上，Web服务需要表达和传递包含对远程服务的引用的文档[6]-1电子邮件地址：carpinet@cs.unibo.it2电子邮件地址：laneve@cs.unibo.it1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.029148S. 卡尔皮内蒂角Laneve/Electronic Notes in Theoretical Computer Science 162（2006）147L：：=标签| a（标签）表1模式语言。S：：=schema| ⊥empty schema| L + L(union)| L\L（差异）| ~(any label)| ()void schema| KBS κ通道图式| L [S], S sequence schema| S + Sunion schema| U模式名称业务）。从技术上讲，这种困难可以通过将服务提升到第一类实体并委托一种使用Web服务描述扩展的模式语言来提供最低级别的安全性来解决。然而，子模式关系的计算成本变成了一个问题，在松散耦合的情况下，如Web服务。在这种情况下，来自不受信任方的数据需要在处理之前进行验证。虽然验证需要相对于正则表达式类型的数据大小的线性计算复杂性，但当数据携带端点时，情况并非如此。在这些情况下，验证简化为子模式关系，从而变成指数关系。更准确地说，当数据携带端点时，接收者必须验证端点的模式（WSDL文档）是否为了克服这个问题，我们通过丢弃诸如a[S]，SJ+a[T]，TJ等不确定模式来降低正则表达式类型的表达性，并使用具有输入/输出功能的通道模式扩展语言[5]。最终的语言很简单，表达能力足以描述携带端点的XML文档，并配备了多项式代价的验证算法（和子模式关系）。这种语言是描述Web服务合同的首选语言对其他更具表现力的候选项的分析，例如详细说明输入/输出操作数量或其确切顺序的候选项，是我们未来研究的一部分。这个扩展摘要的结构如下。在第2节中，我们介绍了语言。在第3节中，我们定义了两个子模式关系。文中给出了等价性证明我们参考了较长的版本[1，2]以了解详细的动机和技术细节。2模式语言模式的句法类别由表1中的语法定义，其中术语κ用于i，o和io的范围。 标号L表示元素a，b，. ... 标签a表示单例{a};L+LJ和L\LJ表示并集以及L和LJ的对应集合的差（表示空标签集合的每个差都是非法的）;~表示整个标签集合我们写a∈L，其中a是由L表示的集合的标号。S. 卡尔皮内蒂角Laneve/Electronic Notes in Theoretical Computer Science 162（2006）147149模式S描述结构相似的文档集，包括端点模式不描述文档;（）描述空文档;L[S]，T描述以L中的标签开始的序列，包含模式S的文档，然后是模式T的文档;Sκ描述具有能力κ并携带模式S的值的端点。渠道能力定义了什么可以在特定信道模式上执行各种输入和/或输出操作具有能力i的通道模式描述用于输入文档的端点;具有能力o的通道模式描述用于输出文档的端点;具有能力io的通道模式描述用于输入和输出的端点。 S + T描述模式S或模式T的文档; U是描述由其定义E（U）表示的文档的模式名称。 E是相互递归定义U = S的全局环境。函数E受以下有限性约束 设const（S）是包含S中模式名的最小集合，且如果U∈ const（S）则const（E（U））∈const（S）。映射E保留以下属性：• 对于每个U∈dom（E），集合const（U）是有限的。这个性质意味着模式定义了树正则语言[3]。以下是几个简单的例子：U=a[（）]，U+（）定义了一个带有标签a的随机长序列;U=a[U]+（）定义了任意嵌套的文档;Empty=Empty定义了文档的空集（Empty实际上是Empty的语法糖）。值得注意的是，我们的模式语法的两个限制首先，模式名称只能出现在尾部位置。该语法阻止了对非根树的定义，例如a[（）]n，b[（）]n（在上下文无关树语法中，子树不能被定义）。类似的约束也涉及通道模式第一个约束是强制树正则性的标准权宜之计;最后一个约束是强制树正则性的标准权宜之计。ter与下面的确定性概念一起保证了多项式子模式关系。设μ在内部模式表示（），L（S;T）上变化.设S↓μ，表示S有一个句柄 μ，是最小关系，使得：（）↓（）⟨S ⟩κ ↓⟨⟩κSL[S]，T↓L（S;T）如果S↓μ和T↓μJS+T↓μ如果S↓μ或T↓μ如果E（U）↓μ，则U↓我们注意到模式可能不保留句柄。这是一个例子，一个[a]，a[（）]，n.定义2.1（确定的模式）确定的模式的集合是最小的一个，使得：(i) 确定了（）和（）(ii) 如果S已确定，则确定Sκ150S. 卡尔皮内蒂角Laneve/Electronic Notes in Theoretical Computer Science 162（2006）147(iii) [10][11][12][13][14][15][16][17][18][19][1(iv) S+T确定，前提是S和T确定，并且如果S↓L（SJ;SJJ）且T↓LJ（TJ;TJJ）则L<$LJ=<$;(v) 故，“定”是指“定”，即“定”。Deter minene在这种情况下，定义将注意到XML Schema中标记的确定性约束。3子模式关系在本节中，我们分析两个子模式关系。第一个使用基于句柄概念的模拟关系。第二部分通过分析图式的句法结构来比较图式。定义3.1（子模式模拟）子模式模拟是确定模式上的最大关系4，使得S4T意味着：(i) 如果S↓（），则T ↓（）;(ii) 如果S↓i（SJ）是nT↓i（TJ），且SJ是4TJ;(iii) 如果S↓o（SJ），则T↓o（TJ）和TJ4SJ;(iv) 如果S↓（SJ），则(a) T↓ [2] ∑（TJ）和SJ4TJ和TJ4S;(b) 或T↓ [2]i（TJ）和SJ4TJ;(c) 或T↓ [0，0]（TJ）和TJ4SJ;(v) 如果S↓L（SJ;SJJ），则存在I使得，对于每个i ∈I，T ↓Li（TJ;TJJ），L Li/=， L我我L i，S J4 T J和S JJ4 T JJ。i∈I i i在下面的结构子模式定义中，我们使用了一组假设A.这个集合包含模式对（U，S）（第一个元素总是一个常量模式名），用于存储子模式关系已被验证的模式对。这种权宜之计确保了算法的终止。定义3. 2Let≤betpre-orderoncapabiio：oandletfirst（T）=S↓L（SJ;SJJ）L这是一个简化的子结构：A是最小的关系关闭下的可交换的工会和下表2中的规则。规则（BOT）指出，S是最小的模式;规则（LBOT），（SBOT），建立了L [S]，SJ是S的子模式，如果S和SJ之间的一个等价于S。 规则（chan-i）、（chan-o）和（chan-io）将子模式简化为通道构造函数的参数;它们分别在参数上建立协变、逆变和不变关系。规则（UNIONR）允许我们删除右边的联合的分支（这实际上已经足够了，因为模式是确定的）;（UNIONL）允许我们将左边的联合模式的子模式减少到它的每个分支的子模式。规则（RSEq）和（LSEq）定义子模式关系，S. 卡尔皮内蒂角Laneve/Electronic Notes in Theoretical Computer Science 162（2006）147151表2子模式。（无效）（）：A（）A（BOT）：AS（LBOT）S：AAJL[S]，SJ：ATAJ（SBOT）SJ：AAJL[S]，SJ：ATAJ（CHAN-I）K≤iS：AT<$AJ中文（简体）（CHAN-O）K≤oT：ASAJ中文（简体）（CHAN-IO）S：ATAJT：AJSAJJ你好，我是说：ATioAJJ（RSEq）L^L^JS：ATAJSJ：AJTjAJJL[S]，SJ：ALJ[T]，TJ<$AJJ（伦敦证交所q）LJ=第一t（T） L^L^jL^（L<$LJ）[S]，SJ：AT<$AJ（L\LJ）[S]，SJ：AJTJ<$AJJL[S]，SJ：AT+TJ<$AJJ（UNIONR）S：ATAJS：AT+TJAJ（工会L）S：ATAJSJ：AJTAJJS+SJ：ATAJJ（名称）（U，T）∈AU：ATA（NAMEH）AJ=A<${（U，S）}E（U）：AJS<$AJJU：AS AJJ（NAMER）S：AE（U）AJS：AUAJ序列的如果参数已经是序列，则前者适用。这条规则与（UNIONR）一起，允许挑出右参数的序列分支，如果有的话。 值得注意的是，（RSEq）和（UNIONR）并不能证明~[（）]，（）<：a[（）]，（）+（~\a）[（）]，（）. 在这种情况下，需要进行验证，该操作由（LSEq）执行。最后三条规则是关于模式名称的。规则（名称L）表示子结构U：如果对（U， T）位于（高度）集合中，A. Rule（NAMER）在名称U是正确参数时展开名称U。规则（NAMEH）是唯一的一个，在假设中，增加了集合A。Theorem3. 3 （ Ccompatibilityy ） Let U4Rforeveryy （ U ， R ） ∈A.S<：AT<$AJ当且仅当S4T.Proof （ Sketch ） （ N ） ToprovethatS< ： ATAJimpliessS4TwarueeeenthefS<：ATAJ. （二）L etS4T. 为您提供最佳使用体验，出于技术、分析及推广目的，我们构造一个证明树，并证明它的有限性。这个论证是通过对三元组（n，S，T）的结构的归纳得出的，其中n是所有可能假设的集合的基数（它是有限的）减去当152S. 卡尔皮内蒂角Laneve/Electronic Notes in Theoretical Computer Science 162（2006）147前假设的集合A，而S，T分别是模式S，TQS. 卡尔皮内蒂角Laneve/Electronic Notes in Theoretical Computer Science 162（2006）147153Theorem3. 4（复杂性）Analg orit he ri f esS<：ATi mAJinpolyn omial时间。该算法使用两个表At和Af来存储模式的通用对（不仅仅是对（U，T））。At用于其子模式关系已被验证或正在被验证的模式;Af存储其关系已被验证为假的模式。在算法的每一步，一个新的对（其分量是S和T的子项）被添加到At或从At移动到Af。算法总是终止，因为当每对子项在At或Af中时，算法终止。此外，它在多项式时间内终止，因为S和T的不同子项是关于S和T的大小的多项式。引用[1] Carpineti，S.和C. Laneve，A basic contract language for Web services，收录于：Proceedings of theEuropean Symposium on Programming（ESOP 2006），LNCS（2006），（即将出版）。[2] Carpineti，S.，C. Laneve和L.皮杜塞？帕多瓦尼Web服务技术实验项目（2006年），可在http://www.cs.unibo.it/PiDuce/上获得。[3] Comon，H.，M. 多谢河Gilleron，F.Jacquemard，D.Lugiez，S.Tison和M.托马西，特里自动机技术和应用，可在http://www.grappa.univ-lille3.fr/tata（1997）上获得，2002年10月1日发布。[4] 细谷，H.，J. J. C. Pierce，XML正则表达式类型，ACM SIGPLAN通知35（2000），pp. 1122.网址citeseer.ist.psu.edu/hosoya00regular.html[5] 皮尔斯湾C.和D. Sangiorgi，Typing and subtyping for mobile processes，in：Logic in ComputerScience，1993，Full version inMathematical Structures in Computer Science6，No. 5，1996.[6] Web服务寻址工作组，Web服务寻址（ws-addressing），可从以下网站获得：http://www.w3.org/Submission/2004/2004），August，10 th2004.