理论计算机科学中的软件构件部署问题

理论计算机科学电子笔记182（2007）17-32www.elsevier.com/locate/entcs软件构件部署Meriem Belguidoum1和Fabien Dagnat2法国布雷斯特-伊鲁瓦兹技术中心布列塔尼ENST计算机科学系摘要基于分布式的系统难以部署主要有两个原因：结构的复杂性和部署任务的复杂性。当前的工具不能正确地管理这些复杂性，因为它们允许的描述缺乏表现力。缺乏对系统和组件要求的适当描述，无法确保安全安装和拆卸。 目标本文的目的是提出一种形式化的部署依赖。 这些依赖关系表示在逻辑语言与部署引擎相关联，该部署引擎允许在待证明的系统中保留字：组件部署、部署依赖、安全部署。1引言由于组件有趣的特性，构建系统的组件方法越来越受欢迎。我们可以想象，软件将很快成为非常大的组件集合，组件的重用和共享将 成为惯例。然而，组件通常是由不同的团队开发的，它们的依赖关系并没有明确规定。因此，安装（或卸载）一个组件通常是一场赌博，因为所有的依赖关系都很难找到。使用当前的方法，安装可能不会成功[15]（安装的组件不工作），安装或卸载可能不安全并破坏系统。为了面对基于组件的系统的发展，我们的目标是建立一个具有正式基础的工具，以确保部署的成功和安全。在本文中，我们提出了形式化的静态部署系统，确保成功和安全的安装和卸载。是什么意思1电子邮件：meriem. enst-bretagne.fr2电邮地址：fabien. enst-bretagne.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.02918M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17静态的是，我们不解决互连的动态重新配置 在系统中。这里介绍的工作没有考虑到部署行动的具体实现。 我们只提出一个推理框架 授权或禁止部署此外，我们的工作是基于这样一个事实，即组件带有对其需求的精确 the system.核心概念是依赖性的概念，它抽象了组件和硬件需求之间的联系。在安装过程中使用冗余，以确保满足要求，在卸载过程中使用冗余，以确保满足要求。本文定义了依赖关系，如何指定它们，并描述了如何在安装和卸载期间正确管理它们本文的组织结构如下。首先，第2节介绍了组件部署的概念，并使用邮件服务器的示例说明了部署依赖性。接下来，第3节介绍了依赖关系部署的描述，第4节介绍了环境约束的描述。 然后，在第5节和第6节中，我们分别给出了组件在目标系统上的安装和卸载以及组件在目标系统上的效果管理的形式化描述。最后，我们在第7节讨论了相关的工作，并在第8节提出了一些未来的工作来结束本文。2组件部署在本文中，我们使用一个基本的抽象概念的组件。 组件提供需要服务的服务。组件和服务通过其名称进行标识。指定所需的服务，并给出其名称（可能还有其提供者的名称）。这项工作可以应用于任何支持命名服务和组件以及所需服务和所提供服务概念的请注意，使用名称来指定需求需要有一些组件和服务字典。在开放环境中，这个要求可能是一个限制，但实际上已经被Linux的打包系统所使用。为了克服这一限制，需要努力使服务和组件能够使用其他形式的标识（例如，服务的接口类型组件软件是一组相互连接的组件。这种互连是软件架构，通常使用架构描述语言（ADL）（如Fractal ADL [3]或xADL [10]）进行设计。 图1示出了Linux系统上的邮件服务器的这种体系结构。 它由四个组件组成：Post fix，一个扮演邮件传输代理（MTA）角色的SMTP服务器，Fetchmail，允许通过电子邮件传输协议（例如，，Pop）（消息被重定向到本地传输），Procmail，一种管理收到的邮件并允许（例如）过滤邮件的邮件传递代理（MDA）。最后，Sylpheed，一个用于阅读和撰写邮件的邮件管理器，称为邮件用户代理（MUA）。3这意味着组件不隐藏需求或结果。M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1719FDS≥ 1380SMAmavisFDS≥ 852poclientMTA后固定fetchmailFDS≤ 1508SylpheedDocPopclientMDAspell-DictProcmailfetchmailMTA<$Smanager数据库MDAFDS≤ 248AV垃圾邮件过滤器Sanitizer AntiSpamSylpheedMUA检查MTA MDA MUA AVAntiSpam图1.一、组装与邮件服务器相关的组件组件在系统中的安装/从系统中的卸载对应于组件向系统的添加/从系统的移除。这些行动的成功需要：(i) 系统提供组件（正在安装）所需的资源和服务。(ii) 组件（正在安装）或其中一个服务与已安装的服务不兼容。(iii) 系统中的其他组件为了回答这些问题，我们需要（1）目标系统的资源（2）它的体系结构和（3）组件描述。资源在这里由一组环境变量抽象。我们假设为资源描述（例如管理信息格式[5]）选择了一个标准的名称和赋值。这些值是由传感器获得的，因此不会被我们的规则修改系统的体系结构记录了系统中所有组件之间的互连。这样一个完整的显式架构（如果存在的话）由于其规模而难以管理。此外，构建它可能非常困难，因为依赖关系通常部分隐藏。因此，与其监督所有的安装和卸载脚本，我们提倡使用组件之间相互依赖的近似值。第4节将更详细地讨论这种近似。组件的描述必须足够精确以表达链接提供的服务符合其要求。这种灰盒描述指定了参数化契约的内部依赖关系[17]，也就是说，输出（提供的服务）与它们所依赖的条目（所需的服务）相关联。 这些链接将在下一节中定义20M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17·⇒¬¬3产品质量标准在本节中，我们给出了所需服务和所提供服务（同一组件或两个组件）之间关系的精确定义这种关系称为依赖关系。已经介绍的邮件服务器示例在图14中示出了依赖性。依赖关系有三种主要形式，依赖关系是强制性的，可选的或否定的：• 强制性依赖关系（用实线表示）是一项严格要求。 如果没有填充，则无法安装。例如，邮件服务器需要一个具有特定CPU或特定库等的终端。• 可选依赖性（由虚线表示）指定该组件可以提供可选服务。在不阻止安装的情况下，不得提供此类服务（如果未满足其要求）。例如，如果Amavis服务可用，则postfix可以提供用于扫描消息以防止病毒的服务。否则可以安装postfix并提供MTA服务，但不提供AV服务• 否定依赖性（由否定表示）指定禁止安装的冲突。冲突可能与服务或组件有关。例如，如果已经安装了另一个MTA（例如sendmail），则无法安装postfix（内部）依赖性描述语言5使用由以下语法定义的依赖性和谓词的概念，其中s表示服务的名称，c表示组件的名称D：：= P s |D·D |D #D|什么？ DP：：= true|PP|QQ：：= QQ|RR：：=[v Oval]|s|c|C.S|S联系我们| ≥ |<| ≤ |为|=/这些操作符的精确语义将由可安装性和安装规则（分别为图4和图6）。直觉上，依赖关系可以是两个依赖关系的合取或析取，？或者简单的依赖关系P s指定服务s的需求P。这些要求以合取范式的一阶谓词语言表达，以简化安装规则。 五个原始条件（R）表示环境变量[v Oval]值的比较，与服务s或组件c的冲突，或由精确组件c.s或任何组件s提供的服务的要求。 这种谓词的例子见图1在所需接口上（左侧）。重要的是要注意，组件可能会禁止它提供的服务。提供%s的组件可以使用此功能来禁止（将来）安装提供s（<$ss）的任何其他组件。4与真实情况相比，依赖关系被简化了[5]有一种更人性化的语言存在，但不在本文的范围内M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1721−→⎪FGGPF−→GCP F FE⎪Ctx={c|（c，−）∈Ctx. C}−AMAVIS.amavisPOSTFIX.av SANITIZER.消毒剂PROCMAIL.avSPAM.spamassassinPROCMAIL.spamassassinC1.libFETCHMAIL.popclientSYLPHEED.MUASYLPHEED.CorrectorPOSTFIX.MTAPROCMAIL.MDAC2.libC3.libC4.libSPELL.spelldictionnary图二、 图1的邮件服务器的依赖关系图14上下文描述目标系统的资源和体系结构由以下概念建模：的上下文。理想情况下，它可以是所有组件（系统的一部分）的依赖关系的联合。 但是，这种结合的计算（和操纵）是不现实的。因此，需要一个安全的近似（这个联盟）。确保安全安装时，我们必须了解可用的服务（及其提供商）和已安装的组件，以检查服务的要求和配置。 我们还需要环境变量的值。为了安全卸载，我们需要保留服务之间的所有潜在依赖关系。在本文中，上下文由（1）存储值的环境，变量的使用，（2）一组四元组（c，s，s，c），为每个安装的组件c存储其提供的服务s、禁止的服务s和禁止的组件c和（3）依赖图存储依赖项。 的节点是可用服务及其提供者（C.S）和边是一对节点N1N2，这意味着N2需要N1。 每条边（箭头上方）都按类型标记的依赖性，无论是强制性的M或可选的O。图2示出了图1的邮件服务器的依赖关系图。依赖图是由它的标记边的集合定义的。它在安装期间构建，在卸载期间使用。这意味着边n1 n2in 表示n2可用，需要n1。 它 这意味着n1在n2之前可用，也就是说，该图不包含循环。在实践中，这可能是一种限制，因为两个组件可能相互依赖。我们认为，这种循环应该通过构建复合组件来解决，这些组件将这种循环隐藏在系统中。 这种合成操作目前尚无法提供，留待今后工作。为了简化规则的表述，让我们定义可用/禁止的服务和组件7：Ctx={Ps|（−，Ps，−，−）∈ Ctx. C}FS（Ctx）= {Fs|（−，−，Fs，−）∈ Ctx. C}FC（Ctx）={|（−，Fc）∈Ctx. C}6实际上，它引入了高耦合，禁止单独安装或拆卸。7. 本 文 采 用 了 一种点表示法来直接访问元组的特定成员，并用作匹配任何内容的joker。22M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17►⇒►E. E.图三. 安装阶段5安全安装在我们的方法中，抽象安装分两个阶段进行（见图3）。首先，我们通过评估当前上下文中的组件依赖性来检查是否可以安装（可安装性）然后，如果安装是可能的，我们计算它对上下文的影响。一旦具体安装完成，此事件用于更新抽象上下文。5.1安装性在授权安装组件之前，我们必须确保（1）它没有被禁止，（2）它所需的服务在上下文中可用，以及（3）它确实不提供违禁服务。更正式地说：定义5.1（可安装性）如果组件未被禁止并且D通过图1的检查规则验证，则具有依赖性D的组件c可安装在上下文Ctx（Ctx c：D）内。第四章：CCOMP：Ctx<$CDc∈/FC（Ctx）Ctx-C：D图4的检查规则确保组件的强制 对于一个简单的依赖关系P s，这意味着P的值为真，并且s不被禁止（CT）。上下文Ctx中谓词P的求值遵循经典逻辑，并在图的第一部分（规则CtxP P）中给出在此阶段，忽略可选依赖项（COPT），因为如果不阻止组件安装，这些依赖项可能不可用当两个依赖关系有效时（CAND），依赖关系的合取被解析，并且当两个依赖关系中的一个有效时（COR L和CO rL），它们的析取被解析。（c）《公约》第10条。没有是的端安装安装性上下文组件依赖M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1723►►¬¬¬ ∨ ¬ ⇒PTRUE：CtxPtrue同品种器械：PAND：CtxQMPQ1CtxQMPQ2CtxQ1Q2CtxPR1POR L：CtxCVPR1CVP2PNOTS：s∈/AS（Ctx）CtxPsCtxPR2采购订单：CtxCVPR1CVP2PNOTC：c∈/AC（Ctx）CtxPcCtx。E（v）OVCtxCVP[vO V]PS服务： s∈AS（Ctx）CtxCVPsPC OMP：（c，Ps，−，−）∈Ctx. Cs∈ PsCtxCtxPc.s学历：CT：Ctx<$Ps∈/FS（Ctx）CtxCtxPtxCAND：CtxCD1CtxCD2Ctx-CD1·D2COPT：CtxCXC？DCtxCtxD1CtxCtxCD1#D2CtxCtxD2CtxCtxCD1#D25.2安装见图4。 安装规则一旦组件被证明是可安装的，我们需要计算它在系统上的安装效果。该事件包括新的可用服务、新的禁用服务、新的禁用组件和新的依赖关系（由依赖关系图表示）。在给出安装规则之前，我们将通过定义两个操作来展示如何计算此效果：CalcF（确定禁止的服务和组件）和依赖图计算。首先，通过收集组件依赖谓词的否定项来计算组件禁止的服务和组件。这是由下面定义的函数CalcF唯一值得讨论的情况是析取。实际上，析取的几个子项可能禁止服务（或组件）.例如，在依赖关系表达式a b S中，a或b可以被禁止。为了跟踪这种可能性，可以建立一个复杂的系统来记录哪些底片是（真正）需要的。如果a可用，则在此处b）我们可以保持b（resp.a）当它们都不可用时，我们保持析取。我们选择在这里介绍一个更简单的系统，因为我们认为精度方面的好处不值得它的成本。也就是说，在一个析取中，所有带有否定谓词的服务和组件都是被禁止的（在析取的情况下，被禁止的服务的集合与在合取的情况下是相同的PVAR：CORL：CORR：24M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17⎪CalcF（<$s）={s}，⎪⎩G计算F（Q1<$Q2）= F1<$F2，F1<$F2 其中CalcF（Qi）=Fi，FiCalcF（R1<$R2）=F1<$F2，F1<$F2其中CalcF（Ri）=Fi，FiSSCCSCSSCCSCGTRUE：Ctx，c，sGtrueGAND：Ctx，c，sGQ1G1Ctx，c，sGQ2G2Ctx，c，sGQ1Q 2 G1 G2GOR：Ctx，c，sGR1G1Ctx，c，sGR2G2Ctx，c，sGR1 G 1 G2GVAR：Ctx，c，sG[vO V]GNOT S：Ctx，c，sG<$sJGNOT C：Ctx，c，sG<$cjGS服务器：GS ERVC：（cJ，Ps，−，−）∈ Ctx. C sJ∈ PsCtx，c，s<$GcJ.sJ<${cJ.sJ−M→c. s}sJ∈AS（Ctx）Ctx，c，s<$GsJ<${cJ.sJ−M→c.s|（cJ，Ps，-，-）∈Ctx. C <$sJ∈Ps}图五. 图形计算规则定义5.2（CalcF）函数CalcF计算来自谓词的禁止服务集和禁止组件集CalcF（true）=CalcF（s）=CalcF（c.s）=CalcF（[vO V]）=CalcF（<$c）=，{c}依赖关系图是在安装阶段使用上下文和正在安装的组件提供的服务构建的。为此，依赖关系图收集组件添加的所有依赖关系定义5.3（图计算）当在上下文Ctx中提供服务s时，由组件c引入的依赖图是根据图5的规则从其谓词P（Ctx，c，sGP G）计算的。导致新依赖性的唯一规则是那些指定服务要求的规则。规则GSERV在服务的每个潜在提供者和需要它的服务之间添加依赖关系。规则GSERV C确保cJ提供sJ并产生相应的依赖关系。最后，安装的定义如下：M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1725►⇒ ⊥►⇒ ⊥►⇒ ⊥1 2 1 2 12⇒·F FGPSSCSSC我 12SSSSC1C2T_（max）：Ctx，c，s<$GP<$Gs∈/FS（Ctx）CalcF（P）=Fs，FcCtx，c<$I（P_（max））<${s}，Fs，Fc，GCtxPPCtx，cI（Ps）s∈FS（Ctx）Ctx，cI（Ps）Ctx，cIO点1：Ctx，CI？D，，，Ctx，cIDPs，Fs，Fc，GCtx，CI？ DPs，Fs，Fc，{s−O→sJ|s−−→sJ∈G}Ctx，c第一章：Ctx，ctID1·D21D2IAND2：Ctx，ctID1·D2Ctx，cID1P1，F1，F1，G1Ctx，cID2P2，F2，F2，G2IAND3：Ctx，cD·DPP，FF，FF，G GCtx，cID1Ps，Fs，Fc，GCtx，cID1#D2Ps，Fc，Fs，GIORR：Ctx，cID1Ctx，cID2Ps，Fs，Fc，GCtx，cID1#D2Ps，Fs，Fc，G见图6。 安装规则定义5.4（安装）在上下文Ctx中具有依赖性D的组件c的安装有四个方面：提供的服务s，禁止的服务s，禁止的组件c和依赖性（图）。这些结果是客观的，由图6的规则所限定。Ctx，cIDPs，Fs，Fc，GCtxIc：DPs，Fs，Fc，G如果P为假（INOT1）或s被禁止（INOT2），则P s的结果否则，s是可用的，禁止的服务和组件由CalcF计算，图形由图5的规则（IT）计算。可选依赖项？如果D被定义（IOPT1），则D具有与D几乎相同的效果，并且D的依赖关系被转换为可选的。否则，它没有效果（IOPT2）。在合取词D1D2中，D1和D2必须有效，则其结果是其结果的并集（IA和3）。否则，它是unfined（IAND1和IAND2）。最后，析取如果D1被验证，则D1#D2是D1的值（IOR L），反之则是D2的值（IORR输入1：INOT2：IO患者：IORL：ICOMP：226M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17OM⎪⎨案子 请注意，析取具有if的语义，即第二个依赖项 只有当第一个没有被验证时才使用在本文中，我们认为，我们的形式化推理引擎不照顾更新环境变量。具体部署引擎更新物理上下文，传感器将其带到正式引擎。5.3安装示例让 在 具 有 描 述 { （ FDS = 500000 ） } 、 { （ C1 ， Slib ， ， ） 、 （ C2 ， SAmavis，，）}、的系统中的（SAmavisSAV）。后缀的可安装性由图7的第一部分给出的证明推导出来。这个证明确保库存在，sendmail不存在，可用磁盘大小（FDS）大于所需的大小，并且所提供的服务SMTA不被禁止。请注意，由于SAmavis的要求是可选的，因此未对其进行探索。由于后缀是可安装的，安装阶段遵循并通过图7的第二部分中的证明计算安装后缀的效果（CPX）（SMTA的需求谓词表示为P）。在此阶段，检查可选依赖性以确定其是否提供服务（在此，其贡献SAV服务）。安装postfix后，提供MTA服务（SMTA）和防病毒（SAV），并禁止组件sendmail（CSM依赖图G对应于导出的依赖图的并集从两个子依赖性，即G={C2.SAmav是−→CPX.SAV， C1.Slib−→CPX.SMTA}。因此，在安装postfix，上下文变为：{（FDS= 500000）}，{（C1，Slib，Sllb，Sllc），（C2，SAmavis，Sllc，Sllc），（CPX，{SMTA，SAV}，Sllc，{CSM}）}，⎪⎩{C2.SAmavis−O→CPX.SAV,C1.Slib−M→CPX.SMT A}6安全拆卸部件c的拆卸也分两个阶段进行。首先，我们通过确保（使用依赖图）没有c提供的服务来检查其可行性。另一个组件需要。然后，我们计算卸载的效果，即从上下文中删除c以及与服务相关的边，c在依赖关系图中提供为了管理卸载，我们使用在安装过程中构建的依赖关系图。 如果一个组件提供的服务没有被其他组件使用，则可以删除该组件。因此，对于每个提供的服务，我们必须检查另一个组件的（强制）服务是否需要它。因此，如果服务未被使用（即，它是依赖图的叶）或者它仅是M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1727可安装性：500000≥ 1380CtxβFDS≥1380CSM∈/{ C1， C2}Ctx P-CSMSlib∈ {Slib，SAmavis}CtxPSlibCtxP[FDS≥1380]CSMSlibSMTA∈/CtxCQC[FDS≥1380]CtxCQC [FDS ≥1380] Ctx CQCSMCQCCtx-C？（SAmavisSAV）CtxC（[FDS≥1380]CSMSlib SMTA）·？（SAmavisSAV）安装方式：Slib∈ {Slib，SAmavis}Ctx，CPX，SMTA<$GSlib<${C1.Slib−M→CPX.SMTA}Ctx，CPX，SMTAG<$CSMCtx，CPX，SMTAG[FDS≥1380]Ctx，CPX，SMTA<$GP<${C1.Slib−M→CPX.SMTA}SMTA∈/<$CalcF（P）=<$，{CSM}Ctx，CPX<$I（P<$SMTA）<${SMTA}，<$，{CSM}，{C1.Slib−M→CPX.SMTA}SAmavis∈ {Slib，SAmavis}Ctx，CPX，SAVGSAmav是{C2.SAmav是−M→CPX.SAV}SAV ∈/<$CalcF（SAmavis）=<$，<$Ctx， C PX<$I（SAma vis<$SAV）<${SAV}， <$，<$，{C2.SAma vis−M→CPX.SAV}Ctx ， CPX<$I ？ （ SAmavisSAV ） {SAV} ， {C2.SAmavis−O→CPX.SAV}Ctx， C PXI（ PSMTA ） ·？（SAma visSAV）{SMTA ， SAV}， ，{CSM}，G见图7。后缀的可安装性和安装证明可选服务（直接或间接）需要（在图中，来自它的所有路径必须由绿色弧组成定义6.1（强制依赖（MD））依赖图中组件c提供的服务s的强制依赖（MD）集合定义如下：MD（G，c.s）={{cJ.sJ} <$MD（G，cJ.sJ）|c.s−M→cJ.sJ∈G}定义6.2（可卸载性）组件c可以从上下文Ctxi保证其提供的所有服务都没有强制依赖性：（c，Ps，−，−）∈ Ctx. C{MD（G，c.s）|s ∈ Ps}=CHECK-DI：CtxCtxDc28M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17LDAPPerlPerl LDAPApacheSVNPerlPerl LDAPWebAuthLDAPSVNAuthLDAPLDAP图8.第八条。一个依赖关系图的例子在上下文Ctx上卸载组件c的后果涉及必须从依赖图中移除的节点集。这组节点包含所有c提供的服务和依赖于它们的所有（可选）服务。一旦进行混凝土拆除，Ctx将通过删除c（以及它提供的服务、禁止的服务和禁止的组件），并且从G中移除8该e的所有节点。定义6.3（可选依赖（OD））依赖图中组件c提供的服务s的可选依赖（OD）集定义如下：OD（G，c.s）={{cJ.sJ} OD（G，cJ.sJ）|c.s−O→cJ.sJ∈G}定义6.4（拆卸）部件c的拆卸具有以下效果：效果：（c，Ps，−，−）∈ Ctx. C让我们通过一个例子来说明具有可选依赖项的组件的卸载。 假设我们想要一个通过Apache和Perl使用LDAP身份验证的Subversion服务器SVN。组件LDAP-Perl允许根据组件LDAP的属性对用户进行身份验证。这些部件必须按照精确的顺序安装（见图8）。首先，安装LDAP和Perl以启用组件LDAP-Perl的安装。此组件提供服务S LDAP-Perl可供APACHE选择使用，以提供身份验证服务SWebAuthLDAP 。 最 后 ， SVN 可 以 使 用 此 服 务 来 提 供 自 己 的 身 份 验 证 服 务 SSVNAuthLDAP。让我们来看看组件LDAP-Perl的卸载以及服务SLDAP-Perl的删除。根据可拆卸性定义6.2，我们需要确定MD。在图的左侧9、我们可以看到，8G \N={n1−−→n2|n1−→n2∈ G <$n1∈/N<$n2∈/N}CtxEc{{c.s}外径（Ctx. （G，c.s）|s∈ Ps}M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1729--GPerl.perlPerl.perl见图9。 删除LDAP-Perl依赖关系图，依赖于此服务的所有路径都有可选弧。事实上，这个服务只被APACHE使用（可选），然后是SVN。因此，MD为空，可以卸载Perl-LDAP根据定义6.4，要删除SLDAP−Perl，我们必须删除依赖于它的所有节点OD的演算给出SWebAuthLDAP，SSVNAuthLDAP。因此，这些服务被删除，而组件APACHE和SVN仍然安装。所得到的依赖图在图9的右手侧示出。7相关工作基于构件的系统的描述和管理是当前研究的热点。 部署工具（如COACH [9]）和部署规范（如 OMG [13]不支持对部署依赖的描述。在这些框架中可以表达的约束仅限于对目标环境的约束。在体系结构描述语言（ADL）[12，6]中，描述集中在结构视图上，并集中在组件的高级逻辑视图上，而不考虑物理视图（对物理环境的真实影响）。存在行为ADL，如π-ADL [14]，但未解决展开问题。据我们所知，[8]是唯一一个扩展ADL以指定部署约束的工作。他们的方法是描述对组件位置的约束。这些约束使得能够描述对硬件、简单软件依赖性和协同定位的要求。然而，忽略卸载的问题，它们不必处理软件依赖关系。我们的工作旨在涵盖逻辑和物理视图的描述或表达语言的部署约束规范。为此，我们遵循[17]使用参数化条件来指定依赖关系（即，所提供的服务根据可用服务而不同）。 在Reussner的论文中，这种方法仅限于 质量属性。在[11]中，提出了一种表示和管理组件系统中依赖关系的体系结构。这种表示用于组件实现，这些组件实现是可靠的，并且自动适应环境中的动态变化。 在这项工作中，依赖描述被假设为已经存在且一致，而在我们的方法中，我们的目标是证明规范的一致性。LDAP.ldapGPERL−LDAP.perl−ldap APACHE.webAuthldapSVN.SvnAuthLdapG'LDAP.ldapG'30M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17最后，很少有工作检查部署的安全性。EDOS项目旨在管理大量软件包之间的依赖关系。他们建立了一个正式的系统来检查可安装性。在他们的上下文中，可安装性比我们的要难得多，因为如果系统不允许安装组件，他们会试图确定启用安装所需的最小包集。 他们证明了这个问题是NP完全的，但表明这不是实践中的问题。[18]中提出的另一项工作涉及软件配置管理问题。它通过定义一种基于规则的形式语言来表示配置知识，从而形式化了Debian的软件包系统。每个规则（表达一个需求）都使用稳定模型语义转换为逻辑程序[7]。这项工作的重点是这种特殊形式的语义，而不是复杂的依赖关系的管理最后两项工作与Debian Linux发行版的软件包管理有关。软件包和组件之间的主要区别是一个软件包只提供一个服务。此外，组件可以根据上下文提供可变数量的服务需要一种更本文介绍了这样一种语言，它有规则，以保证安装和卸载的安全8结论和今后的工作本文提出了一种构件安装和拆卸的形式化方法。它旨在提供一个安全的部署框架，保证安装和卸载的成功。 确保这种安全性的关键概念是是依赖的概念。 一个依赖抽象了一个组件连接，它是强制性的还是可选的，是积极的（必需的）还是消极的（禁止的）。通过扩展需求的语法（允许提供者规范）和引入依赖图的概念，这些依赖的描述和管理包含了我们以前的工作[2，1所有潜在的依赖关系都被这个依赖关系图（在安装过程中构建）近似，以确保安全卸载。 一个简单的原型相关联的证明已经开发出来在OCaml中。 这个概念验证原型目前用于测试我们的方法关于Fractal组件的部署[4]。我们正朝着两个主要方向努力。第一，我们的目标是确保部署的保障。为此，部署系统应该尊重的属性. .）是必须的。然后，我们的目标是证明我们的系统确保这些属性。第二个方向是扩展我们的系统，以克服其目前的局限性。两个主要限制是：• 需要进行配置操作、更换操作和组装操作。需要执行replace操作以允许组件升级。事实上，由于我们的系统不允许卸载提供服务的组件9.虚拟包的概念并不具有与真实服务相同的表达能力M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）1731其他组件使用的错误，升级组件并不等同于先卸载再安装。组装操作需要使用其子组件的依赖关系来计算组合组件的依赖关系。• 组件和服务标识，在我们当前的方法名称中，一个他们本不该拥有的中心位置 服务的标识必须扩展为包括接口类型和版本信息。这意味着在确定服务之间的依赖关系时，从名称相等更改为子类型的形式。引用[1] Belguidoum，M.和F. Dagnat，软件组件中部署依赖性的分析，在：SAC[2] Belguidoum ， M. ， F.Dagnat 和 A. Beugnard ， Analysedesde pendan cespourlede eploiementautomatiquedec om posant s，in：Jour neesCom posants200 5，LeCroisic，France，2005，pp. 57比68[3] Bruneton，E.，Fractal的发展，法国电信研发（2004）。网址fractal.objectweb.org/[4] 布鲁顿，E、T. Coupaye和J.陈志华，分形理论与应用，北京大学出版社（2003）.网址fractal.objectweb.org/[5] 分布式管理任务组，公共信息模型（CIM），CIM基础设施规范，DMTF（2005）。网址www.dmtf.org/standards/cim[6] Garlan，D.，R. T. Monroe和D. Wile，Acme：基于组件的系统的体系结构描述，在：G。T. Leavens和M.Sitaraman，editors，Foundations of Concentration-Based Systems，Cambridge University Press，New York，2000 pp.47比67[7] Gelfond，M.和v.Lifschitz，The stable model semantics for logic programming，第五届国际逻辑编程会议论文集（1988），pp.1070-1080.URLhomepages.inf.ed.ac.uk/dcspaul/publications/ggf12.pdf[8] Hoareau，D.和Y. Mah o，基于约束的动态网络中分布式组件的部署，载：计算系统架构（ARCS2006），LNCS（2006）。[9] 何礼文例如，IST COACH项目（2003年），部署和配置规范，可[10] 哈雷河M. Guntersdorfer，P. Oreizy，N. Medvidovic和R. Taylor，xADL：启用以架构为中心的工具与XML的集成，在：Proc. 第34届夏威夷系统科学国际会议，第9卷（2001年），p. 9053[11] Kon，F.，“基于代理的分布式系统的自动配置”，博士论文，部门计算机科学，伊利诺伊大学厄巴纳-香槟分校（2000年）。[12] Medvidovic，N.和R.N. Taylor，A classification and comparison framework for softwarearchitecture description languages，Software Engineering26（2000），pp.70比93URLciteseer.ist.psu.edu/medvidovic97classification.html[13] OMG，Deployment and Configuration of Compatient Based Distributed Applications，Specification version 4，OMG（2006）。网址www.omg.org/cgi-bin/doc?正式/06-04-02[14] Oquendo，F.，π-ADL：一种基于高阶类型π-演算的体系结构描述语言，用于指定动态和移动软件体系结构，SIGSOFT Softw. Eng. Notes29（2004），pp. 1-14号。[15] Parrish，A.美国，B. Dixon和D. Cordes，基于组件的软件部署的概念基础。Journal of Systems andSoftware57（2001），pp.193-20032M. Belguidoum，F.Dagnat/Electronic Notes in Theoretical Computer Science 182（2007）17[16] R. Di Cosmo，《关于软件开发的正式管理的报告》，可交付WP 2-D2.2，EDOS项目（2006年）。[17] Reussner，R.，I. Poernomo和H.Schmidt，软件组件的合同和质量属性，在：W。Weck，J. Bosch和C.Szyperski，editors，Proc.8thURLciteseer.ist.psu.edu/703313.html[18] Syrjéanen， T. ，Arule-basedformalmodelforsoftwarereconfiguration ， Research ReportA55 ，HelsinkiUniversity of Technology ， Laboratory for Theoretical Computer Science ， Espoo ， Finland（1999）.