异构组件的粘合语言：理论计算机科学电子记录

114《理论计算机科学电子札记》66卷第4期（2002）网址：http://www.elsevier.nl/locate/entcs/volume66.html19页异构规格组件GwenSalauên，MichelAllemand，ChristianAttiogb'e1IRIN，法国摘要在本文中，我们提倡一种方法来结合形式规格化组件。我们的工作旨在构建或重用特定组件，并使用由最小但足够的操作符集组成的粘合语言将它们组合起来。胶水允许在一个人的处置与异构组件作为基本实体的利益是多方面的：对系统的不同方面进行建模，允许使用许多现有的规范语言，以简单和图形化的方式将组件之间的链接化，使组件的重用更容易。一个关于自动售货机的案例研究被指定来说明这种方法可以如何实际使用。关键词多形式主义规范，异构组件，粘合语言，操作语义学。1介绍形式化方法的使用是关键软件系统开发中不可避免的一步。因此，正式规范遵循需求分析，是开发的基础。一个问题是，复杂软件系统的所有方面既不能用一种方法来指定也不能用一种方法来验证。联合使用几种形式化方法，称为多形式主义，集成或异构规范，是必要的描述这样的系统。另一方面，组件的概念已经在几个领域出现了几年。组件起源于软件领域，它们代表一个独立的编程单元，可能使用接口与其他单元组合。这个想法是恢复在这里，并适用于解决目前的问题，是指定使用异构形式组件的实际系统。我们强调，在本文件中，1电 邮 地址：{salaun，allemand，attiogbe}@ irin.univ-nantes.fr2002年由ElsevierScienceB出版。 诉操作访问根据C CB Y-NC-N D许可证进行。萨拉温115模块被同义地使用（我们使用模块作为指定模块的简写）。这项工作的动机如下。首先，软件系统的不同方面必须用适当的形式主义来具体化，并且必须用适当的工具来形式化地验证。使用单一的形式主义是不够的，以指定复杂系统的不同部分。此外，这些不同的形式主义必须以正式的方式联系起来。另一个目标是简化用各种语言编写的特定模块的重用。第二个动机允许重用已知子问题的现有解决方案。这里提出的工作是基于异构组件，因此，使结构化和重用组件更容易。这种结构对于掌握系统的复杂性很有用。最后，我们增加了组合的可读性，因为我们选择了一种带有图形符号的链接语言。事实上，组件之间的链接首先以图形的方式表达，然后再通过这些组合的完整表达进行文本我们的建议的基本思想是组成异构规范- i fication模块。我们从[2]中遵循的方法中获得灵感。先前的研究旨在以异构的方式将进程代数Promela与代数规范Larch的语言相结合。然而，这项工作也存在一些局限性，特别是由于提案没有正式化。在本方法中，我们考虑到许多语言相比，最初的工作。我们的方法是面向控制的，并且允许立即满足异构规范的动机该建议有正式的基础，但直接面向务实的目标。本文的其余部分组织如下。在第2节中，我们的方法的形式基础分为三个步骤：精确地定义组件作为规范的基本实体，定义连接规范组件的胶合语言，形式化这种胶合的语义。 第三节将介绍一个关于自动售货机的案例研究。第四节介绍了相关的工作。我们在第5节中作了总结性评论。2我们方法在下文中，我们希望组成的语言被分为两个主要的家族。语言要么是面向数据的，要么是面向行为我们只考虑基本语言，也就是说，我们不考虑已经组合的语言，如LOTOS [7]。这是合理的，因为基本语言更适合指定复杂系统的精确方面第一个家族包含关于数据的形式主义，即专注于静态方面（代数规范，Z [23]，B [1]）。第二种是面向行为的语言，处理动态方面萨拉温116（Process algebras，transition systems）关于数据语言，我们不必面对语法或语义不一致的问题。我们假设在面向代数（代数规范）和面向状态（Z，B）的语言之间有很强的分离。实际上，这似乎是不直观的，例如，将B模块与指定抽象数据类型的另一个模块组合在一起。此外，这个限制在第一步中很有用，可以使粘合语言的语义更容易。主要的问题是在语义层面上，由于异构的基础（谓词逻辑和集合论与代数集）。关于动态形式主义，虽然不允许模块内容之间的强语法链接，但连接模块没有困难，因为有一个基于LTS2的公共语义模型。对这些不同方面的全面研究可以在[5]中找到。2.1组件我们称之为规范组件或模块，这是用前面描述的语言之一编写的规范。用代数规范语言编写的规范模块可以包含一个或多个抽象数据类型的定义。以类似的方式，以进程代数编写的模块可以由多个进程组成。因此，我们考虑组件的一般定义，而不仅仅包含单个声明。动态组件包含过程定义或转换系统定义。当我们提到动态模块的一个行为时，我们考虑这些定义之一（例如一个过程或一个过渡系统）。这种精确性对于简化读者对2.4小节中以下语义定义的理解是很重要的。由于我们的方法是控制驱动的，动态组件构成了主要的行为。因此，静态模块（包含数据规范）是独立的，而对应于动态行为的模块利用这些数据。对于动态模块，我们在行为和数据之间有很强的联系。这些链接主要是通过价值传递来表达的。更准确地说，进程代数在不同的层次上处理数据：动作参数、进程参数和保护或条件结构。对于基本跃迁系统，相互作用主要位于跃迁的标号中。如果使用更高级的转换系统（例如Statecharts [12]），链接可以出现在其他级别（例如警卫）。这些基础在[20]中得到了精确的研究，我们在当前的方法中考虑了这种形式化2.2Gluing语言现在，我们处理模块之间可能的链接，我们特别详细地将胶水描述为一组操作符，我们向指定者建议将2 标签转换系统。萨拉温117件.这些操作符与要链接的语言家族有很强的联系。这些胶合结构是最小的，并且可能被认为不够复杂。相反，这种语言对于规范连接第3节中所示的规范组件来说是非常有意义的。对于静态组件的组成，以及两种类型组件之间的联系，引入了导入操作符。为了组成动态组件，我们使用类似于并行组合的进程代数中遇到的操作。我们对链接的选择不会引起关注点的强烈分离，这与[4，17]中提出的方法不同，其中粘合原理基于同步产品[3]。然而，这些作品的缺点（主要是难以表达的链接和有限的可读性）没有出现在我们的建议。现在，我们从我们的胶水中可用的不同连接可能性开始：STATIC-STATIC，MANIC-STATIC，MANIC-DYNAMIC3。静-静。关于代数特殊化模，我们只考虑模的输入;为了这个目的引入了运算符IMPORT。在第一阶段，我们避免给出许多结构化的可能性，以保持简单的组合语言。关于Z或B模，算子USE足以描述一个模被另一个模使用。数据模块（公理或面向状态）被分开处理，因为它们的链接操作符有不同的含义;因此，不同的名称被用来区分它们。静电干扰。对于这些链接，我们使用操作符NEED来表示DYNAMIC组件需要STATIC组件。由于我们在控制驱动规范上工作，因此动态模块需要这种构造来解释出现在动态行为中的数据。动力学。我们提出了一个非常通用的部件组合操作符SYN-PC，它可以实现多路同步通信。该算子与基本LOTOS或CSP的广义复合算子接近，并且具有相似的意义。 它使它可能是几个特定模块的组合，因此它们包含的行为的组合。 它有一个参数，一套交流-模块自身同步的事件。HIDE被提议作为隐藏操作符。这种构造对于隐藏例如在超级组件4内的动作是有用的。改名 运算符集还包含结构RENAME 加强重用模块的特性（特别是出现数据的DYNAMIC模块）。此运算符应用于指定程序希望重命名不同标识符的模块。3 在下文中，STATIC代表面向数据的模块，而DYNAMIC表示有礼貌的人。4由其他成分组成的成分萨拉温118语言：：=重新命名|连接重命名：：=重命名ID+ ID+移动连接：：=静态-静态-组合|化学-静态-组成|动态合成静态-静态-组成：：=IMPORT ASL-STATIC-MOTORICAL ASL-STATIC-MOTORICAL|使用SL-STATIC-MOSTIC SL-STATIC-MOSTIC化学-静态-组成：：=需要 电子邮件：info@mos.com.cn化学-动态-组成：：=SYN-PC药物-药物-药物+作用 *| 隐藏动作+动态合成抽象语法。现在，我们精确地形式化了关于模块的相互连接的部分，并且我们在图1中总结了在我们的方法中可用的不同链接操作符。图1.一、内核扩展文法语法中出现的一些非终结符由于对应于基本的词汇实体，所以没有详细说明。大多数操作符都是面向对象的，特别是RENAME、IMPORT、USE和NEED。因此，例如对于导入，存在指示源模块和目标模块的标识符。同样，对于重命名，有两个列表：第一个对应于要替换的标识符，第二个包含替换先前值的新值。重命名仅适用于一个模块。出现在列表中用于重命名的标识符可以是术语、操作、动作、事件或其他。此词汇表取决于用于编写重命名完成的模块保持非常通用，我们使用术语标识符。这些标识符在一个模块中是唯一的，并且在更高的级别上是唯一的（以其组件的名称为前缀）。最后，我们注意到，与其他的并行复合算子不同，连接动态模块的并行复合算子是多方向的。2.3澄清一些特征在本节中，我们的目标是澄清我们的方法中所涉及的一些要点和可能性。组件特性。首先，在我们的工作中，组件被认为是规范级别，而更一般地说，软件组件表示编程级别。在软件组件中，接口是访问组件服务的入口点。此外，由于组件和其客户端5是在相互不知情的情况下开发的，因此存在5使用服务的组件萨拉温119以确保安全的互动。组件在其中演化的环境必须提供条件，以便组件可以运行;这称为上下文依赖性。最后，在其接口后面的实现的不同的可视化是可能的;主要的抽象是白盒，玻璃盒和黑盒。在这项工作中，接口是不必要的，因为组件要么由规范设计，因此是白盒，要么直接重用，在这种情况下被视为玻璃盒（这是我们的选择）。然后，开发人员总是可以看到每个模块的内容（黑盒抽象是不可能的），以获得声明的行为，操作或其他的含义，并因此将它们连接起来在我们的提案中，前面的接口、契约和上下文依赖的概念并不相同，但是通过胶合语言及其语义来捕获和管理底层思想。抽象与具体的组件。 按照我们的方法，静态和动态组件要么是抽象的，要么是具体的。抽象组件包含数据类型、操作或行为的定义。在描述一个特定系统时，我们首先用索引名称对抽象组件进行建模;然后我们使用通过重命名或实例化抽象组件而获得的具体组件。没有下标的抽象成分和具体成分混合在一起。此外，它们可以使用前面定义的操作符链接到抽象数据组件。当具体数据由动态行为管理时，它们隐式地出现在具体动态组件中。图2显示了一个系统示例，说明了抽象级别的这种差异。涉及动态组件的链接不使用抽象动态组件来表示，而是使用具体的动 态 组 件 来 表 示 ， 因 为 我 们 假 设 对 于 同 一 抽 象 动 态 模 块 （ 例 如Dynamici），我们可以选择不同的抽象数据组件来解释具体数据项。图例说明：抽象模块混凝土动态模块混凝土数据胶合语言Module Instantiation图二、包含抽象和具体组件的示例静态动态1动态2OthDynamic动态iOthDynamic萨拉温120超级组件。 我们现在讨论连接超级组件（或层次组件）的可能性.这种可能性对于构造许多连接的组件是非常有趣的。它简化了表示，并使隐藏子级别细节成为可能。其主要思想是在Statecharts中出现超级国家[12]。每个模块可以由不同的子组件组成。在与超级组件连接的情况下，只有其动态行为可以参与链接（而不是数据部分）。事实上，全球规范是由控制驱动的;因此，人工组件是可见的，但数据组件是不可见的。然而，如果指定器需要访问任何层次级别的某个模块的抽象数据，它可以建模与此模块和更高级别上使用的另一个模块的连接。必须小心，因为层次级别之间的这种连接可能会损害整个规范的可读性分享数据。在动态模块中嵌入具体数据是很自然的，并且在更广泛的范围内不排除动态模块之间的数据共享。要共享的数据将由一个简单的过程或过渡系统管理，该系统提供访问和修改具体数据的最小行为。然后，通过这种嵌入数据的动态行为点对点与广播通信。让我们考虑一种情况，其中两个动态组件使用胶合语言的并行组合操作符连接。其中一个组件采用点对点通信，另一个组件采用广播通信。在这种情况下，考虑了一个发送者和多个接收者的情况（参见下一个语义规则）。另一方面，几个接收者和一个接收者的情况是没有意义的，因此既不被我们的算子考虑，也不被相应的语义规则考虑。参数化组件。在大多数语言中，尤其是在程序级，组件被参数化以增强其可重用性.在我们的方法中，考虑了参数化，但没有显式地进行参数化，即，例如，在定义步骤中不出现参数化（例如，M [P1，...，Pn]）。在这里，组件参数特别用于表示泛型位置，可能出现在我们的规格组件中。作为一个例子，图3显示了在第三个数据模块中导入两个数据模块（Product和Stock），在第三个数据模块中，股票是用Product数据类型显式实例化的。因此，定义库存的组件使用通用术语参数化，并且每个导入库存的组件都被归纳参数化，除非该参数在源组件中实例化2.4胶合语言的操作语义在这一部分中，我们形式化了我们的胶合语言的每个操作符的含义。在更广泛的范围内，我们详细介绍了全局行为的语义萨拉温121×→DynCompoP（s：库存[产品]）=.StaCompo1产品=...StaCompo2库存[T] =.图三. 参数化元件由连接的组件组成。存在两种主要的推理规则。静态规则不诱导系统的演 化 。 这 种 类 型 的 规 则 涉 及 重 命 名 操 作 符 和 STATIC-STATIC 和DYNAMIC- STATIC链接。它们描述了背景的丰富，或适当评价功能的构建。对于语义-动态组合，语义被视为LTS。推理规则用于详细描述每个操作员的行为演变。LTS的形式定义是一组状态S、一组标签L和一个类型为S L的转换关系S.动态组件的语义以及连接动态组件的胶水运算符的语义被认为是LTS的抽象定义。环境. 为了定义语法运算符的含义，我们使用三种环境。第一个被称为ASL-E（代数规范语言环境），并为包含用代数规范表示的数据类型的模块存储信息。该环境被绑定到数据模块，并且精确地是元组<签名、公理、评估函数>，其中签名表示操作名称及其输入/输出参数，并且公理是约束每个操作的角色的众所周知的代数公理。第二个环境专用于以面向状态的语言编写的模块，称为SL-E（状态语言环境）。它由一个元组<签名，属性，评估函数>组成，其中签名具有与以前相同的意义另一方面，属性收集不同的东西：变量、不变式和B机器或Z模式中出现的初始化。更准确地说，这些属性对应于描述状态空间所必需的不同部分。在大的，静态模块之间的链接是有用的，以建立评估功能，这将被用来解释出现在动态的be-的数据。求值函数主要从数据定义（代数公理，或面向状态的语言的属性）计算。下文将对这一计算进行深入研究最后，环境E适合于动态模块以保持元组<签名，评估函数>来自行为模块和数据模块之间的不同输入链接。因此，该环境包含操作及其评估功能。 这些信息用于解释动态部分中出现的具体数据与The萨拉温122结论静态-静态-组成：：=进口 ASL-STATIC-MOSTIC ASL-STATIC-MOSTIC可以执行模块名称以区分模块之间的连接中的两个环境例如，如果M是一个模块，DE是一个绑定到数据模块的环境，那么M.DE可以避免混淆。符号和变量。在下文中，针对框中给出的每个抽象语法规则详细描述推理规则。用于编写规则的格式是：前提。labelof函数返回动作的标识符。paramof函数返回动作中的参数集。Exp[T/V]逻辑符号用于在表达式中用T项替换变量V。实验时间在这里，这个符号被扩展到在整个模块中执行替换。函数in、out和other分别验证动作是输入、输出还是无方向。 asl-ex函数表示从以代数规范编写的数据模块中提取签名和代数公理。sl-ex函数表示从用状态语言编写的数据模块中提取签名和属性（变量、初始化和不变式）。 前面的两个函数都是解析函数，从不同的数据模块中提取所需的信息∈B函数测试行为是否是动态模块的一部分。约束函数表示一个环境被绑定到一个模块。eval-extr函数从签名、公理或属性中提取eval函数。exist-const函数表示模块之间存在一个构造（作为参数给出），并且该构造被处理以增强源模块的环境。该函数的参数是结构和相关模块的名称。在语义规则中，我们区分了小写字母和大写字母的一些符号。对于签名、代数公理和性质，小写字母中的符号对应于局部定义，而大写字母中的符号表示从模和它们之间可能的联系推导出例如，σi表示单个模块的签名，而Σi表示从多个模块收集签名的签名。eval函数的表示法也以同样的方式进行了区分。最后，我们在表1中收集了出现在推理规则中的变量。推理规则。我们并不打算在本文中列出所有规则。我们只是举例说明了胶水的一些操作符的含义：IMPORT，NEED，SYN-PC。缺失的规则可以在[22]中找到。萨拉温123表1变量描述可变描述M，Mi模块σi，Σ i，Σi带元运算符集axi，AX，AXi代数公理P面向状态规范F，Fi，G行为α，β操作（输入、输出、内部、其他）一组动作bound（M2，ASL−E2）ASL−E2=N2，AX2，EVAL2>bounded（M1，ASL−E1）ASL−E1=，， ε>bound（M2，ASL−E2）ASL−E2=N2，AX2，EVAL2>bound（M1，ASL−E1）ASL−E1=N1，AX1，EVAL1>asl−ex（M1）=<σ1，ax1>1=σ1AX1=ax1AX21J1=AX1J=AX1AX2eval−extr（A1，AX1）=EVAL1ASL−E1J=A1，AX1，EVAL1>exist−const（IMPORTM1M2）bounded（M1，ASL−E1J）eval−extr（J1，AX1J）=EVALJ1ASL−E1J=J1，AX1J，EVALJ1>exist−const（IMPORTM1M2）bounded（M1，ASL−E1J）左规则描述了一个模（M2）被M1的第一次输入。这里和其他规则的解读是：如果由一组签名、一组公理和评估函数组成的环境ASL-E2绑定到代数模块M2，并且绑定到代数模块M1的环境ASL-E1为空，并且签名和公理从M1模块中提取，并且源模块的评估函数从两个模块的签名和公理构建，并且新的ASL-E1环境由签名的并集、公理的并集和相应的评估组成。函数是从输入中推导出来的，那么这个环境就绑定到M1模块上。我们假设两个模块的签名中没有冲突（空交集）;在建模过程中，规范必须小心。不同的名字意味着不同的意义。在这个假设下，由于态射（例如重命名），我们可能有一个签名与另一个签名相同;然而，在这种情况下，所涉及的模块被认为是不同的。作为输入结果之一的评估函数是根据两个模块的签名和公理计算的，如下一部分所述萨拉温124静态成分：：=需要静态成分静态成分化学-动态-组成：：=SYN-PC药物-药物-药物+作用 *在推广前一个规则的正确规则中，ASL-E1环境不是空的，因为该模块已经导入了其他模块。新的签名和公理集以及新的eval函数使用合适的集合来计算。bound（M2，ASL−E）ASL−E= N，AX，EV AL><结合（M1，E）EJ=E{，EV AL>}<结合（M1，E）EJ=E{，EV AL>} set）：术语列表本地结果：termslistinit（i）对于param中的每个peval-fct<$find（first-op（p），E）result（i）<$eval-fct（p）inc（i）返回结果eval函数的计算。 我们有两种类型的求值函数，这取决于数据规范语言的类型：面向公理的或面向状态的。对于代数规范，评价函数对应于项重写函数。重写系统是通过应用排序算法从代数公理获得的，确保终止和连续性，如[15]中所述。重写选择是合理的，因为它适合于操作语义，因此使我们能够保持在实用和可执行的上下文中。为了应用这些算法，我们将自己限制在数据类型的初始语义上，因为重写系统对一组公理的解释只有在初始模型的情况下才真正有意义[6]。对于具有松散语义的代数规范语言，我们将它们限制在它们的初始代数（例如，参见[14]关于CASL [9]）。排序算法的输入是聚集在ASL-E元组中的签名和公理。更进一步说，逻辑中有更多的困难，而不仅仅是初始/松散的解释问题。例如，一种代数规范语言可以使用强等式，另一种是弱等式，第三种是存在等式。如果我们希望共同管理这种不同的语言，我们有义务防止基于不兼容逻辑的语言混合。因此，我们将这些模块之间的组合限制为非冲突逻辑。对于面向状态的语言，评价函数是从这种模块中提取的签名和属性计算的。对于每个操作名称，该函数将名称与应用于状态空间的行为绑定在一起，这会导致对该状态空间的修改。状态空间的特征在于SL-E元组中的属性Pi，即变量、初始化和不变量。eval函数在[22]中有详细说明。萨拉温1273示例说明：自动售货机在本节中，我们将研究自动售货机案例。系统必须接受用户插入的硬币和饮料的订单。如果投入的硬币足够，机器会提供饮料，并在必要时返还该系统由两部分组成：现金兑换机和饮料分配器。为了简化这个例子，我们假设了一些关于机器的限制：所有的饮料都有相同的价格;订单的取消不受管理。在[22]中，我们提出了自动售货机的两个规范，它们的基础非常相似，但在用于指定组件的基本语言中却足够不同：（1）过程代数和代数规范，（2）标记转移系统和B。在本文中，我们选择进程代数来指定并发方面，代数规范来建模数据。在我们的例子中，规范中使用了两种以上的语言。我们首先总结了这个系统的数据类型和建模过程，以及使用的形式主义：Nat写在CASL，饮料和股票在落叶松，用户CCS中的CashChanger（CC）流程和CSP中的DrinkDistributer（DD使用四种语言来实现这样简单的规范可能是令人惊讶的;然而，这里的唯一目标是说明我们方法的可能性。包含Nat的模块在CASL中指定用于以前的工作[21]，并直接重用。用Larch编写的模块是从[19]中提出的处理发票订单系统的规范中获得的。通过重命名操作符RENAME的应用程序进行更新。下一个代码显示饮料是从Product数据类型推导出来的，替代了产品库存。 下面的第一个列表包含名称 第二个是他们的替代品。重新命名 Drink，drink，drinkref，eq drink，add drink，removeedrink>MPro duct，Stock现在，我们展示了重新命名和定义库存后获得的部分组件。setname STOCKdeclare Sort Stockdeclareop空库存：->库存添加饮料：饮料，天然，库存->库存增加量：饮料，天然，库存->库存减少量：饮料，天然，库存->库存：饮料，库存->布尔...萨拉温128下面在CCS中描述的CC代理是用饮料的价格和机器中可用的硬币数量参数化的。它开始检索由用户插入的钱的总和，以及要交付的饮料。然后，CC与饮料分销商通信以验证所订购的饮料是否可用，并接收作为布尔值的答案。如果饮料是可用的，金额是足够的，并且现金兑换机拥有足够的硬币来返还钱，那么它向分销商表示饮料可以交付，等待这个动作完成，返还钱，并将其硬币数量与饮料价格增加。CC（drinkprice：Nat，coinnb：Nat）d=efgetCoin（c：Nat）.getDrink（d：Drink）. isAvailable（d）.availableAnswer（b：Bool）.（if（b/\drinkprice<=c/\（c-drinkprice）<=coinnb）然后将饮料（d）。完了 giveCoin（c-drinkprice）.CC（drinkprice，coinnb+drinkprice）+ if（b/\drinkprice=c/\（c-drinkprice）=coinnb）然后giveCoin（c）。CC（drinkprice，coinnb））DD流程在CSP中描述，并使用其管理的饮料库存进行参数化。它有两种行为。 第一个对应于库存中给定饮料的可用性。第二个行为描述了向用户提供饮料，以及更新库存中该饮料的量。DD（st：Stock）=是否可用？d：饮料→可用答案！库存（d，st）→ DD（st）Q送饮料？d：Drink→ giveDrink→完成→DD（减少量（d，s（0），st））用户代理对于系统的规范是不必要的。然而，我们插入它，以便有更多的相互作用的过程，而不仅仅是两个代理。它的行为包括投入硬币，订购饮料，并等待饮料被交付和硬币被归还。在图4中，我们介绍了指定模块以及它们之间的链接关于这些连接，它们首先包括由声明其他数据类型的模块导入定义自然数的代数模块。之后，动态模块需要Drink和Stock排序，以及包含它们的模块。最后，用CCS和CSP编写的模块与SYN-PC运算符并行组成。Larch模块中Drink和Stock排序之间的联系用宿主形式表示。它不是用我们的胶合语言编写的，这使得特定模块的连接成为可能。现在，我们提出了代数模之间的不同联系的文本和综合形式，萨拉温129CASL落叶图例说抽象数据类型或过程进口组件链路需要需要SYN−PC需要CSPCCSCCS用户CCDDNat喝股票图四、自动售货机规格的模块组成数据类型模块和其他包含进程定义的模块之间的使用。IMPORTMDrink，StockMNatNEED MDD MDrink，Stock NEED MCC MDrink，Stock NEED MUser MDrink，Stock我们阐明了在CCS和CSP中编写的模块之间的SYN-PC组成链接。详细描述要组合的模块和进程（在模块中定义）同步它们的动作就足够了。SYN-PCMDDMCCM用户{isAvailable，availableAnswer，deliverDrink，done，getCoin，getDrink，giveCoin，giveDrink}4相关作品我们的工作可以与几个具有相同目标的工作进行比较，即组合特定组件。然而，在实现这一目标的道路上存在着困难。现在介绍其中一些建议。[22]中报告了与相关工作的更全面比较。 首先，我想说的是，软件组件主题中的一个重要参考文献是[24]。Szyperski对软件组件的定义可以是：“软件组件是一个组合单元，只有合同指定的接口和显式的上下文依赖关系。软件组件可以独立部署，并由第三方组成”。这个定义在我们的工作中并没有保留在我们的方法中，组件是基本实体，但它们是特定的单元，而不是编程单元。在[18]中提出的工作中，作者的目标是用基于状态和基于事件的语言来指定系统。他们特别使用行动系统萨拉温130和CSP进程代数来建模组件。Große-Rhode提出ATS（代数转换系统）作为组件的形式化模型[11]。ATS对应于一个语义框架，作为一个共同的基础，在这个基础上，可以解释用不同语言编写的规范。AltaRica [4]和Korrigan [17]是相似的语言，特别是基于转换系统。这两种方法都使用Arnold和Nivat的同步产品[3]来粘合不同的特定组件。许多研究人员致力于开发模型，形式主义和机制来描述并行和分布式系统建模的异构组件的集成[16]。这一做法是基于协调的概念。这些工作面向编程方面，而我们专注于具体化方面。 协调模型由三部分组成：实体/组件、连接组件的媒介和模型的语义框架。在介绍我们的工作时遵循了这一方法最后，在过去的十年中，软件架构[10]已经成为软件工程的一个重要领域。体系结构是将系统组织为交互组件的集合。ADL（架构描述语言）是一种形式化的建模符号，它关注整个软件应用程序的高级结构一些ADL允许使用像Wright和CSP这样的形式化方法，但其他ADL除了自己定义的符号外没有任何形式化的符号。最后，形式规格说明能够以类似且更正式的方式捕获架构5总结发言在本文中，主要目的是用一种形式化和用户友好的方法来规范复杂系统。这种方法使规范人员能够组成异构规范组件。组件用现有的形式语言（代数规范，Z，B，进程代数，转换系统）进行规范。 我们提出了一个简单的和最小的语言组成模块使用这些形式主义。形式化了连接算子的操作语义。一个案例研究被指定为这项工作的具体说明。与相关工作相比，我们的方法提出了许多利益。首先，不同方面（静态和动态）的覆盖是由于允许的语言的多样性，以及它们对指定不同的相关方面的适用性而实现的。此外，这种形式主义的多样性为具体化者提供了具体化语言选择的自由。组件的重用也得到了简化，因为数据和动态行为之间的链接是非常通用的。胶合语言基于简单的操作符，具有易于理解的语义。最后，由于在指定步骤中可以使用图形表示，因此可读性得到了提高。尽管这一提议在异性恋领域引入了创新，萨拉温131对于不同的规范，该解决方案是这种方式的第一次尝试。克服了许多困难，例如语义规则定义或eval函数的计算。另一方面，可以对本工作的不同基本概念进行改进。 例如，粘合语言可以可以扩展其他操作符，如时间属性或行为之间的优先级，以增强其表达能力。另一个步骤将是组件内部行为和数据之间的严格形式化今后工作的主要方向是进一步发展核查工作。因此，我们的目标是向规范提供一个完整的规范环境，在其中可以执行仿真，证明和测试。我们不希望从头开始开发一个新的工具箱，但我们更愿意重用现有的工具。关于验证方面，我们特别旨在使用PVS [13]等高阶工具证明全局规范上的属性。引用[1] J. R. 阿布里尔B书。剑桥大学出版社，1996年。[2] M.Allemand和C.Attiog b'e.具体化形式的实用组合。1999年在法国WADT'99上发表[3] A. 阿诺德财务系统和通信系统的管理。Masson，1992年。[4] A. Arnold，G. Point，A. Gri Pastaault，和A.罗兹描述并发系统的AltaRica形式化。Fundamenta Informatica，40，1999.[5] C. Attiogb'e. 本文介绍了几种常用的集成方法：一些锁和轮廓。技术报告00.8，综合区域信息网，南特大学，2000年。[6] M. 比多伊特 另外，一种语言可以帮助我们发展对特定类型的预测。 博士论文，Uni versi t'edeP-Sud-Cen n tre d' Ors a y，1989年。[7] T. Bolognesi和E.布林克斯玛介绍ISO规范语言LOTOS。在宾夕法尼亚大学。J.van Eijk ， C. A. Vissers 和 M. Diaz ， editors ， The Formal DescriptionTechnique LOTOS，pages 23Elsevier Science Publishers North- Holland，1989.[8] CoFI。通用框架倡议为代数规范和发展，电子档案。可通过WWW7和FTP8访问的笔记和文档。[9] CoFI语言设计任务组。CASL -CoFI代数规范语言-摘要（版本1.0.1）。Documents/CASL/Summaryin [8]，2001.7http://www.brics.dk/Projects/CoFI8ftp://ftp.brics.dk/Projects/CoFI萨拉温132[10] D. Garlan和M. 肖软件体系结构导论。在V.Ambriola和G. Tortora，编辑，软件工程和知识工程进展，第1卷，第1-40页。世界科学出版公司，1993年。[11] M. 大罗德 代数变换系统及其组成。在E. Astesiano，编辑，FASE'98会议记录施普林格出版社[12] D.哈雷尔Statecharts：A Visual Formalism for Complex System. Science ofComputer Programming，8（3）：231[13] J. Crow ， S. Owre， J. Rushby ， N. Shankar和 M. Srivas。 PVS简 介 。《WIFT'95会议录》计算机科学实验室，SRI国际。[14] H. Kirchner和C.林盖森使用ELAN重写引擎执行CASL等式规范注[8]，2000年，T-9[15] J. W. 克洛普术语重写系统。In S.Abramsky，D.M. Gabbay和T. S. E. Maibaum，编辑，Handbook of Logic in Computer Science，第2卷，第1章，第1牛津大学出版社，1992年。[16] G. A. Papadopoulos和F. 阿巴布 协调模式和语言。在大型系统工程中，计算机进展第46卷。中国科学技术出版社，1998年.[17] P. 我的天 Korrigan