部署上下文信息增强的组件兼容性：基于类型的应用程序一致性

可在www.sciencedirect.com在线获取理论计算机科学电子笔记279（2）（2011）17-31www.elsevier.com/locate/entcs使用部署上下文信息增强基于类型的组件兼容性1普雷梅克·布拉达捷克共和brada@kiv.zcu.cz比尔森西波希米亚大学计算机科学与工程系摘要基于组件的应用程序中的一致性和兼容性一直是许多方法的主题和方法，从形式上健全的实际执行困难的实用规则，比较版本元数据，或只是弱保证。这对于许多日常使用的工业组件框架来说尤其如此。在本文中，我们贡献了一个正式的描述方法，确保应用程序运行时类型的一致性，通过执行基于类型的可替代性检查的一部分，组件绑定和更新过程。该方法考虑了当前部署的组件版本的环境，并在检查中使用其所谓的上下文补充。这种新颖的方法克服了兼容性的标准概念的局限性，允许非逆变器上的组件的表面上所需的一面。该方法已在OSGi组件框架中成功实现，在本文的后面部分，我们将分享通过执行。关键词：组件，应用程序一致性，子类型，兼容性，部署上下文1介绍组件框架在软件工程中已经变得司空见惯，并且越来越多地用于开发具有复杂体系结构的软件系统。越来越多的项目看到了Spring或OSGi等框架的好处，尽管它们在底层组件模型方面相对简单尽管使用组件管理复杂的体系结构更容易，但这些体系结构的安全演化-特别是在整个演化过程中保持应用程序的内部一致性-仍然是一项具有挑战性的任务。 对于动态架构（那些可以在1这项工作得到了捷克共和国赠款机构的部分支持，赠款编号为201/08/02661571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.00918P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）应用程序运行时），其中架构师不能完全预料到变化，并且不一定由任何规则或模式控制在我们的工作中，我们解决了需要一致性验证的常见场景-由另一个组件动态替换当前部署在架构中的组件，无论是完全不同的组件（导致可替换性验证）还是当前组件的新版本（导致作为特殊情况的向后兼容性验证）。验证由Wegner和Zdonik [25]总结的可替代性的一般原则管理：无论何时，只要预期当前组件，替换组件都应该可用，而客户不会注意到它。1.1本文的目标和结构安全替代的研究方法旨在通过形式化方法保证可靠的替代性。然而，在这些方法中使用的模型往往太复杂而不能被普通软件开发者使用，并且这些方法通常会受到禁止的算法或空间复杂性的影响（参见图1）。例如[15，16]）。另一方面，工业系统几乎只使用相当简单的Meta数据，最常见的是版本标识符（例如，[18]），手动标记组件与其先前版本兼容。这种方法的主要缺点是依赖于人工翻译来提供正确的元数据而导致的在本文中，我们描述了一个面向实践的方法来验证黑盒组件的可替代性。它旨在通过相对简单的组件规范方法在当今的组件框架中易于使用，同时提供关于可替换性的高级别正式支持保证。因此，该方法使用（子）类型关系作为其基础，因为其形式强度足以防止严重的运行时错误，同时其评估可以在实践组件模型的当前状态上进行，具有相对简单性和低算法复杂度。该方法仅在组件的可替代性的正式验证方面是强有力的，因为手头的组件规范允许。大多数情况下，它将因此为当前的工业组件框架提供更好的类型安全保证，但它能够包含额外功能属性兼容性的评估[14]或高级形式检查（例如，断言行为协议合规性[19]），其中适当的数据可作为组件规范的一部分该方法的一个新颖而重要的方面是通过考虑组件部署的环境（例如，应用程序架构或组件框架的容器）（以下称为部署上下文），可以克服标准子类型的限制-所提供的特性的严格协方差和所需特性的逆变性本文的结构如下。以下部分概述了组件可替代性的最新技术水平。第3节包含组件类型和部署上下文的基本形式定义，第4节定义P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）19语境可替代性的概念。论文的第二部分是对形式部分的验证。在第5节中，我们描述了OSGi组件框架的方法的实现，并讨论了我们遇到的几个基本问题。在第6节中对该方法的形式和实践方面进行了评估，并在论文的最后对后续工作进行了说明2相关工作这项工作有助于在组件框架中的正确性和鲁棒性的挑战领域这仍然是一个相关的问题，因为例如Taylor [23]指出，在面向服务的体系结构研究中，“很少关注跨服务的. .）边界在一个非常高的抽象层次上，Georgas等人[12]在运行时使用应用程序架构模型来管理其演变。可以在控制进化（适应）的政策上指定约束条件，以保护选定的建筑属性。然而，这项工作并没有提供有关模型、约束条件和检查方法的具体细节。许多研究方法都使用具有全局完整性属性的整体方法来解决这一需求[21，11]。例如，Chaki等人[9]使用组合推理和动态假设保证检查来提供形式上合理的可替代性评估，其实际属性与我们的上下文属性相似。然而，这些方法中的大多数都是基于高级形式系统（例如模型检查，行为子类型），通常由专门的规范符号支持。这些方法倾向于支持禁止的算法或状态复杂性[16，9]，并且符号倾向于太复杂而不能被使用。软件开发者[15]很少有研究工作涉及到工业组件框架的使用。 Polakovic等人[20]使用编译时类型一致性验证和错误处理代码的组合，为资源受限的组件模型由于资源需求，我们的做法在这些情况在其精神上最接近我们的工作是Belguidoum和Dagnat这可以防止同一组件功能（例如消息传递服务）的多个冲突实现使上下文不变量无效。虽然这是一个重要的观察结果，但可替代性本身是在相当抽象的层面上形式化的，并且需要进一步细化服务比较方法、组件安装（卸载）效果和禁止依赖表示，以使该方法完全适用最后但并非最不重要的是，已经提出了几种使用类型系统的方法[11，17]。此外，它们还可以实现多组分替代，这超出了本文提出的方法然而，他们的方法尚未得到验证20P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）工业组件框架。3组件类型和部署上下文为了为基于类型的可替代性和兼容性验证提供一个良好的基础，必须提供一个在比较组件的类型级别上的正式模型。在本节中，我们将描述这样一个模型以及组件部署上下文视图的表示3.1组件接口以某种形式的分发包可用的组件实现可以包括许多不同的元素-可执行代码、元数据、资源对象等。 组件接口的所有元素（即可访问的在组件的黑盒的表面上我们以组件类型的形式捕获组件接口的结构，这是一种结构化数据类型[8]，包含所有这些元素及其在组件间交互中关于组件及其接口元素的信息被假设为可以从某种规范中获得;实现的内部被抽象出来，因为组件是一个黑盒。定义3.1组件接口元素是一个元组e=（n，T，r，o，a），其中n∈String{}是元素的名称（可能为空），T是元素的类型（在各自的规范语言类型系统中），r ∈{ provided，required }是元素在组件接口上的角色，o ∈ Boolean是元素在运行时是否存在的指示组件接口元素的示例包括： 接口或类、EJB组件实现的Java接口（在本例中，e.n=1）2或SOFA组件的原始类型的属性。元素的可选性可以直接在组件规范中指示（如OSGi中定义3.2设EC={ei}i∈I（对于有限索引集I）是一个组件实现C的所有可观察的组件接口元素的集合从它的黑盒子外面C的组件类型C是一对提供的和必需的元素集：C=（EP，ER）|（EP<$ER= EC）（EP<$ER=）whee（e∈EP：e.r= p rovide d）2符号注释：在整个文本中，我们使用点符号来表示元组的各个部分，因此对于A=（a，b），表达式A. a表示A结构的第一部分P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）21⎨·如果e.r=必需，则e.a ≤ e. a。iji⎩（作为C的运行时实例的组件是一个元组c=（id，C，P，R），其中id是实例的唯一标识，C是其组件类型，P和R是实际存在于实例接口的接口元素的集合（我们将把表达式元素角色（提供的，必需的）在组件类型中是有区别的，这有一个基本的原因：它会在类型操作（即匹配和子类型比较）期间影响组件的处理。在这方面，组件类型的定义及其相关的（子）类型规则，虽然类似于标准的结构化数据类型，但反映了基于组件编程的核心概念组件元组的后两部分表示在给定时间的有效类型。它认为c.P<$c.C.EP和c.R<$c.C.ER是因为（某些）可选元素可以被实例省略我们还注意到，Ct1/=t2·c.P/t1在C.R。c.P/t2，同样接口元素的子类型关系是标准的自反传递关系，因此它是类型的前序定义3.3如果下列条件都成立，我们说组件接口元素ei是元素ej的子类型（记为ei：ej）• ei.T<：ej.T（元素类型处于子类型关系中）;• ei.r=ej.r;如果ei.r=prvided，如果ei.r=必需，则e j.oei.o• 如果ei.r=p，则ei.a≥ej.a，下一小节将正式描述部署组件的环境。3.2组件上下文我们在介绍中指出，捕获特定组件的部署环境对于评估可替换性非常有用。此组件部署上下文包含使用该组件的环境中的其他组件和体系结构连接。环境可以是组件集群（组件应用程序的紧密耦合部分）、基于组件的应用程序或围绕运行时框架中已部署组件的整个运行时环境定义3.4组件实例c的部署上下文是一个元组D=（K，B），其中K={ci}i∈I，c∈K是存在于22P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）∈c的部署环境，并且B ={（ep，er）|<$Cp， Cr∈K·（Cp/= Cr）<$（ep∈Cp.P）<$（er∈Cr.R）<$eris bound to ep}是上下文中组件元素之间的绑定。如果所有组件间绑定都被正确解析（包括绑定元素类型的匹配），并且组件正确运行，则部署上下文D在架构上是一致的从可替换性的角度来看，这种环境的一个子集是部署上下文中的组件补充，这一点特别有趣。补集的模型使用与上一小节中描述的组件类型定义3.5假设架构上一致的上下文D和组件c D.K，C型部件。D中c的语境补语是一个“虚”补语，即C <$D =（P <$，R <$），• P<$={e|（εcr∈D. K·crc，e∈crc. R）n（ep∈c.P·（ep，e）∈D. {\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}{\fnarial black\fs12\bord1\shad0\4aH00\fscy110}{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}由C• R<$=scs.P|cs∈D。K，cs/=c其能够满足组件补语可以被看作是c在给定时间的一个反效类型（参见：组件实例的P、R元素集）。它从组件的角度捕获上下文的以下两个(i) 组件提供的元素的实际使用情况，如对其他组件的特定必需元素的绑定所给出的(ii) 环境中可用的元素可能满足任何c图1.一、体系结构中的组件和构成其上下文补充的元素从类型的角度来看，可以对上下文补语进行一些有趣的观察。它们被归纳为下面的引理。引理3.6（上下文补语的性质）假设一个类型为C=（P，R）的成分c和它的上下文 补 语 C<$D= （ P<$ ， R<$ ） a 符 合 上 述 定 义 。 LetPJ={eJ| （ eJ∈P ） <$ （ e<$∈P<$$>·（eJ，e<$）∈D. B）}的实际约束条款的效力。那么它认为，P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）23(i) PJP（并非所有条款都需要约束）。(ii) e <$∈P<$，e∈P·（e，e<$）∈D。B：e.T<：e<$.T（上下文的绑定请求元素可以具有通用类型）。(iii) e∈R·e.o=false<组件更多可能具有专门类型的元素）。证据 这些属性的证明很简单：(i) 如果所有e∈c.P都绑定到上下文中的客户端元素，则PJ= P;否则，|P| − |PJ|是未绑定的提供元素的数量。(ii) 假设有一个必要的元素nte<$x的某个复合物ntcx∈D。K与c的一个 给定的元素e（因此e<$x∈R<$）有e<$x.T<：e.T. 将提供的电子邮件绑定到其他组件所需的电子邮件时ty pe-不安全，因为e不能覆盖e x的所有ty pe特征。这违反了部署上下文的架构一致性假设。(In实践中，运行时框架将拒绝建立这样的先验绑定。(iii) （a）一个sample=pample，意味着非可选的必需元素不绑定到任何相应的这再次违反了架构一致性假设。（b）假设e.T<：e′.T，这是一种类似于第2点的情况。e和e之间的绑定的类型e不安全最终会导致c的故障，这与假设相矛盾（具有相同的实际解释）。Q最后要注意的是，P<$捕捉的是与实际使用的c.P元素相关联的元素的真实类型，而不仅仅是这些元素的类型，并且在P<$R<$集合中没有元素名称唯一性的要求。图中给出了成分补语的概念1.一、 Component Gate部署在一个简单的架构中，绑定到Control和ParkingPlace组件。 在运行时框架中安装了一个附加的TraprocLane组件。Gate的部署上下文包括R <$set中它提供的接口的两个部分，以及作为其P<$set的框架工作中可用的其他三个提供的接口。4组件可替代性第1节介绍的可替代性原则提供了概念的在基于组件的软件工程的背景下，可以通过考虑当前最先进的组件模型中可用的功能来详细说明。如果替换组件满足以下一般要求[4]，则可替换当前部署在一致应用程序架构中的组件24P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）(i) 向其环境提供相同的操作接口（在语法和类型级别）。(ii) 交换与当前数据相同的数据（关于它们的位置和格式）。(iii) 符合当前组件在其参与的所有交互(iv) 展示兼容的额外功能（服务质量）特性。在这里提出的方法中，我们集中在第一个领域，这是对问题的故意简化。这一决定的理由是基于使用工业组件框架时所面临的挑战。在那里，高级方面的规范不可用，或者在大多数情况下不能从实现中重建;因此，特别是语义兼容性很难验证。因此，我们需要将可替代性的正式概念仅仅建立在作为标准组件开发过程的产品的工件和抽象之上。这导致我们（a）使用组件分发包中直接可用的信息-半形式化的组件接口规范，开发过程中创建的可能的元数据，以及运行时组件内省提取的数据;（b）使用形式基础的最小公分母-类型系统及其子类型规则-这些规则始终适用于任何编程或规范语言，并对替代组件的运行时安全性的结论现在让我们定义基于类型的可替换性的基本类型（在[6]的早期版本接下来的部分将介绍考虑部署上下文的新型可替换性定义4.1我们说一个（替换）分量类型R=（PJ，RJ）是（当前）分量类型C=（P，R）的严格可替换的，如果（<$e∈P<$eJ∈PJ：eJ.n=e.n<$eJ：e）<$（<$eJ∈RJ<$e∈R：eJ.n=e.n<$e<：eJ）。 这个事实表示为RC。该定义对应于对“垂直”压缩的自然理解[ 3 ]：替换组件就其名称和类型而言提供至少相同的并且最多需要相同的组件接口元素（与元素的可选性无关）。它在组件类型级别上使用了协变和逆变的共同概念（参见。[24]或[7]）。这个定义确保了任何一对具有C和R类型的组件实例及其替换的先验可替换性。4.1语境可替代性可替代性原则告诉我们，这个属性不仅仅涉及两个组件（当前的，替换的）：我们还需要考虑客户端对它们的使用。从这个角度来看，组件接口的提供部分和需求部分的变化并不等同于可替代性。P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）25在许多基于组件的架构中，并不是所有组件提供的功能都被利用，即绑定到客户端。因此，根据具体情况，在给定的就业背景下评估可替代性时，可以忽略这些未使用的功能。类似地，在组件演化过程中添加新特性是很常见的，这导致需要添加相应的依赖项以使它们工作。在编程语言研究中，这导致了协方差的概念在部署软件组件的情况下，我们可以利用部署上下文的知识，并将替换组件的扩展需求与上下文组件提供的任何需求相匹配从架构的角度来看，这是一个干净的解决方案，因为组件应该不知道谁在提供所需的功能，只要它符合其声明的规范。这导致以下定义：定义4.2给定一个当前部署的C类型组件c及其上下文补集C<$D，我们可以说，如果R<$C <$D成立，则（补集）补集R=（PJ，RJ）在上下文上可替换C，即如果（补集E<$∈P<$eJ∈PJ：eJ<：e<<$） 这表示为RDC。简而言之，上下文可替换替换组件提供至少与当前组件的客户端所使用的那些相同的特征，并且最多需要上下文中可用的那些。可以说它与上下文是横向兼容的[3]。图二、新组件版本与当前部署的上下文补充继续上一节中介绍的示例，图2显示了Gate组件的第二个版本，它将替换原来的版本。 它的需求明显大于原始版本，而且其中一个提供的接口改变了类型。然而，将Gate v2与其当前部署版本的上下文补充进行比较表明，它实际上可以在给定的架构中使用（假设LaneGateStats接口是CountingStats的子类型）。直觉上，人们会认为严格的可替代性意味着上下文。命题4.3（严格可替换性意味着上下文）假设成分c和r分别具有类型C和R。它认为，<$D·c∈D.K： RCRDC，也就是说，如果R是严格可替换的C，那么它也是上下文可替换的C在任何架构上一致的部署上下文D。26P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）∀≺是的。我们首先要保证 D：CDC‐D的意思是C“fits in”its（an y）con text。使用标准符号C=（P，R）和C<$D=（P<$，R<$），可以分两部分完成：• e<$∈P<$• 10. A. A. B. C. D. D.E<. E.（|R| ≤|R¯|）和引理3.6第3项。从这个命题的假设我们有R<$C，上面说E是C <$C<$D，并且由于可替换关系是过渡的，因此R<$C<$D。Q这一事实在某些常见情况下可能是有用的，例如在特殊情况下，组件向后兼容性：对于组件的后续版本，我们可以很容易地证明在组件发布时与其前一个版本的严格可替换性，在其元数据中存储适当的指示，并在升级组件时使用它。只有当没有这样的指示时，才必须在组件绑定或升级时进行可替代性评估此时，执行上下文可替换性检查也是有意义的由于其时间依赖性，组件的有效类型（实际使用的提供和必需元素）和部署上下文都可能在组件实例的生命周期中发生一旦在升级过程中验证了兼容性，则需要通过其他方式不断验证和确保架构一致性5OSGi框架在我们之前的工作[6]的基础上，我们为OSGi框架[18]实现了一个上下文可替代性验证器验证器的总体技术设计是由实际效用需求驱动的几个目标驱动的。其中一个是简化的范围（评估后续bundle3修订版的兼容性，而不是任何对任何的可替代性检查），另一个是在主机框架中的非侵入式集成。验证器应用程序具有一组OSGi bundle的形式实现的总体架构包括三个层-简单的用户界面，bundle和上下文表示加载器加上可替换性验证器（比较器），以及底层Java类型系统模型和子类型规则实现。前两层如图3所示。一旦上下文补充包和替换包的类型表示被Loader包创建（形成一个树形数据结构，提供了基本类型和循环引用），它们就被提交给包比较器，后者实现了可替换性验证。其工作结果基本上是一个3Bundle是OSGi对组件的术语P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）27注释类型树它被聚合到一个关于bundle和complement之间的类型关系的断言中。Substitution Verifier包包含了整个过程，负责激活加载器和比较器，并为用户解释其结果图三. OSGi bundle兼容性验证器有几个基本的问题，上下文可替换性的实现首先，它必须在运行时实现元素子类型关系，并选择合适的类型表示来执行它。其次，需要有一种方法从各种源中提取此组件类型和上下文补充表示在下面的段落中，我们将讨论我们解决OSGi案例中这些问题的方法5.1类型表示基本问题是获取和表示组件规范中包含的元素类型的方法。通常，这个问题被委托给相关的语言编译器;然而，在我们的情况下，需要一个运行时组件类型表示以及从安装和替换组件中获取它的机制。额外的复杂性是，在OSGi中，规范数据分散在几个地方（清单文件作为关键点，XML和其他额外的元数据，例如用于声明性服务，以及bundle实现的字节码）。由 于 没 有 合 适 的 OSGi bundle 的 运 行 时 类 型 表 示 ， 我 们 创 建 了 一 个 名 为BundleTypes的自定义构建模型[1]。它由捕获整个包的选定特征的域类组成，包括模块层（其导出和导入的包）和服务层（提供的和依赖的服务）。然后，这个表示引用一个称为JavaTypes的低层模型，它捕获各个Java类的类型信息类型表示的重构根据所讨论的束使用不同的方法。对于替换包，我们使用字节码分析，ASM库4由自定义类加载器包装此外，还创建了存根4http://asm.ow2.org/28P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）对于共享（JRE，OSGi核心，. . .）或无法访问的类。必须使用这些技术，因为替换版本的捆绑包只能作为文件夹中的独立.jar文件访问特别是对于导入的包，我们从bundle字节码中提取的类和操作引用组装它们的类型表示[2为了获得当前bundle的类型表示及其上下文补充，我们使用标准的OSGi框架服务（包管理，bundle Meta数据和类加载器方法）和Java反射API。这些信息很容易获得，因为捆绑包5.2子类型和兼容性验证关于子类型关系实现，算法的设计必须协调类型关系的理论概念（如前一节所用）与Java作为实际规范语言所采用的规则、其链接机制和OSGi框架的运行时系统之间的差异。最突出的是，Java在其类型匹配规则中使用子类化而不是子类型化[10]，并将子类型化与二进制兼容性区分开来[13]。这个关系实际上是底层元素“subtype”关系的来源在bundle可替代性验证器中，子类型由JavaTypes层评估，结果由BundleTypes层聚合，以表示OSGi bundle的模块和服务层的兼容性。尽管OSGi在模块层有丰富的特性和修改器（可选的导入、它们中的大多数在出口方面没有明显的可替代性，并且在进口方面的有效类型（其反映了这些改性剂的效果）很容易获得。在服务层，元素的可替换性是隐式验证的-所有服务接口必须在导出/导入的包中声明，以便在模块层处理它们的类型比较6评价和经验教训所提出的组件可替代性验证方法可以被认为是一种相当简单的方法。它只使用类型规则作为基础，而忽略了更强大的语义和行为兼容性。除了前面几节中给出的原因之外，这种设计还可以基于以下基本原因进行辩护：该方法对它所应用的组件接口元素的类型没有任何限制。因此，它可以包含与我们的组件类型模型兼容的任何语义或行为规范我们的方法可以应用的一种高级组件接口元素的例子是起源于SOFA组件模型的行为协议[19]。在这种情况下，协议遵从关系扮演P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）29元素子类型的作用。关于所介绍的OSGi可替代性验证器，我们想分享几个观察结果。为了获得导入包的类型表示，使用的字节码分析技术是可行的解决方案，但这两种方法都不完全可靠-例如，字节码不需要包含返回类型类操作。 解决这个问题的唯一好办法可能是以某种方式将引用类的类型信息包含在组件分发包中。此外，对于独立（未安装）和运行的捆绑包，可靠地获得捆绑包服务的完整列表基本上是困难的。第一种情况的原因是，bundle元数据不需要静态声明使用简单核心OSGi模型5的服务，因此即使bundle使用具有显式指定的替代声明性服务模型，也可能找不到某些服务。在后一种情况下，情况只是部分好一些：bundle导出和使用的服务集可以通过框架API获得，但它们 可能会随着时间的推移而改变。因此，bundle上下文表示仅在bundle绑定的当前快照（可能还有历史记录）上，并且可能不包括所有的元素。因此，由于组件模型的性质，OSGi框架的组件可替换性评估将始终避免潜在的错误。替代性验证器的当前实现有几个缺点。在bundle表示和比较级别，它不处理片段bundle和可选导入。它还有意地省略了动态导入和绑定依赖（OSGi世界中已知的不良实践）。此外，所选择的架构-将工具实现为用户空间包-支持其可移植性，但阻止集成到包安装/解析/更新过程中（这将是一个理想的目标，因为它将提供用户透明的兼容性验证）。这些问题是进一步改进执行工作的主题。7结论在本文中，我们提出了形式化的定义和实际实现，一种组件可替代性验证方法。它的主要贡献是新颖地使用组件这种基于类型的可替代性验证可以包装成易于使用的工具和数据，以促进其实际使用。我们团队实现的一个实用扩展是自动创建正确的语义版本标识符5不推荐使用Export-Service和Import-Service清单标头30P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）OSGi框架。关于进一步的研究，该方法的正式定义应该扩展到组件集群（例如，支持更大的应用程序子集的安全替换），并更具体地应用于动态架构中的组件间关系。OSGi的实际实现需要提供组件模型中缺失的方面，并克服框架中更紧密集成的问题。引用[1] Bauml，J.和P. Brada，OSGi中的自动化版本控制：组件软件一致性保证机制，在：欧洲微电子SEAA（2009年）。[2] Bauml，J.和P. Brada，从Java字节码重构类型信息以实现组件兼容性，在：第五届字节码语义，验证，分析和转换研讨会（ETAPS 2010卫星活动），帕福斯，塞浦路斯，2010年。[3] Belguidoum，M.和F. Dagnat，Formalization of component substitutability，Electronic Notes onTheoretical Computer Science215（2008），pp.75比92[4] Beugnard，A.，J. - M. 我也是，N。 Plouzeau和D. Watkins，Making commonponents cont r act aware，Computer 32（1999），pp. 38比45[5] Brada，P.， 布拉格查尔斯大学论文（2003年）。[6] Brada，P.和L.Valenta，使用子类型关系的组件可替代性的实际验证，在：第32届欧洲微电子SEAA会议论文集（2006年），pp。38比45[7] Bruneton ， E. ， T.是 的 ， M 。Leclercq ， V.Qu'ema 和 J.-B.Stefani ，Thefractalcomponentmodelanditssupportinjava：Experienceswithauto-adaptiveandreconfigurable systems，Software Practice and Experience 36（2006）. 公元1257-1284年。[8] 卡尔代利湖，类型系统，载：计算机科学与工程手册，CRC出版社，1997年。[9] Chaki，S.，E. Clarke，N. Sharygina和N. Sinha，Veri fication of evolving software via componentsubstitutability analysis，Formal Methods in System Design32（2008）。[10] 库克，W。R.，W.希尔和P.S. Canning，Inheritance is not subtyping，in：POPL125-135.[11] Desnos，N.，M.于查德角Urtado，S. Vauttier和G. Tremblay，Automated and unexpectedaccessiblecomponent substitution ， in ： Proceedings of 10th International Symposium on Compatient-BasedSoftware Engineering，Lecture Notes in Computer Science 4608/2007（2007）。[12] Georgas，J.，A. van der Hoek和R. Taylor，Using architectural models to manage and visualize runtimeadaptation，IEEE Computer42（2009），pp.52比60[13] Gosling，J.，B.乔伊，G。Steele和G. Bracha，[14] Jeek，K.和P. Brada，在功能和额外功能属性方面的组件兼容性验证-工具支持，在：第12届企业信息系统国际会议论文集（2010年），pp.510-514[15] Leavens，G.，K. Leino和P. Mller，Specification and Verification Challenges for Sequential Object-Oriented Programs，Formal Aspects of Computing19（2007），pp.159比189[16] Ma ch，M.，F. Pla′sensil和J. Kofron，行为预测验证：飞行状态爆炸，国际计算机与信息科学杂志6（2005），第10 页。22-30分钟。[17] McCamant ， S. 和 M.D. Ernst ， Formalizinglightweightverificationofsoftwarecomponentcomposition ， in：Proceedings of SAVCBS 2004：Specification and Verification of convenent-basedSystems，Newport Beach，CA，USA，2004，pp. 47比54P. Brada/Electronic Notes in Theoretical Computer Science 279（2）（2011）31[18] OSGi联盟，[19] Pl'apastasil， F. 和S. 陈文辉，软件工程，2002，第28期。[20] Polakovic，J.，S. Mazare，J. B. Stefani和P. - C. David，基于组件的嵌入式系统，在：第10届基于组件的软件工程国际研讨会论文集，计算机科学讲义4608/2007（2007）。[21] Stuckenholz，A.，作为布尔优化问题的组件更新，理论计算机科学电子笔记182（2007），pp。187[22] Szyperski，C.， 组件技术-什么，在哪里，以及如何？第25届国际软件工程会议（ICSE 2003），俄勒冈州波特兰，2003年。[23] 泰勒河N.，N. Medvidovic和P. Oreizy，运行时软件适配的架构风格，在：2009年IEEE/IFIP软件架构联合工作会议欧洲软件架构会议论文集，2009年。[24] Vallecillo，A.， J. Hernandez和J. M. Tr oya，Componentinterte ro pe rability，Te chnical ReportITI-2000-37，Uni versidaddeM'alaga，Spain（2000）.[25] Wegner，P.和S. B. Zdonik，继承作为一个增量修改机制或什么样的是和不一样，，322（1988），pp.55比77