动态重构构件系统的层次时序规范

理论计算机科学电子笔记108（2004）69-81www.elsevier.com/locate/entcs基于动态重构构件系统的层次时序规范Nazareno Aguirrea，b，1Tom Maibaumb，1aDepartamentodeComputacio'n，FCEFQyN，UniversidadNacionaldeR'oCuarto，Enlacerutas8y36Km. 601，RoCuarto（5800），Cordoba，Argentina英国伦敦大学国王学院计算机科学系，摘要我们研究了基于可重构组件的系统的时间规范是如何分层组织的。 我们这样做，通过扩展以前介绍的声明性原型语言，承认层次子系统的定义。每个子系统都有一个内部架构，由内部交互（简单）子系统和基本组件组成。子系统的内部架构可以在“运行时”通过重新配置操作进行更改子系统的概念提供了一个额外的粗粒度模块化单元，补充了组件的概念。由于组件交互是通过协调来实现的，因此组件或子系统可以由与系统的其余部分隔离的逻辑理论来表示。这一点，再加上按层次组织一个规范的可能性，对推理有着特殊的影响，因为它允许我们进一步将证明任务定位到规范的相关子部分。保留字：软件架构、动态重构、时序逻辑1介绍软件架构可以被视为软件工程的一个分支，它强调系统的高层结构[9，7]。系统的体系结构是用组件来描述的，这些组件可以相互作用1 作者naguirre@dc.exa.unrc.edu.artom@dcs.kcl.ac.uk。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.01370N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）69通过定义的连接器。连接器是组件之间的通信手段，并且具有比其他通信机制更少内聚的特定属性，因为它们在组件的定义之外在过去几年中，一个备受关注的话题是在运行时改变系统架构的可能性，这一特性通常被称为动态重构[13]。动态重构的需求自然且频繁地出现，这可能是由于面向对象建模和编程[14]的广泛接受，其中动态重构是直接支持的。几种体系结构描述语言（ADL）通过定义重构操作来支持动态然而，那些支持重构和形式语义的ADL通常只允许操作性（而不是声明性）描述。考虑到这一限制，我们提出了一种基于时态逻辑的声明式形式主义，用于描述可重构软件架构[1]。通过使用声明式框架获得的抽象使我们能够研究描述软件体系结构的可能的更复杂的抽象方法。 这种形式主义的主要特征是：（i）由于其逻辑性质，它直接支持推理，（ii）它具有足够的表达能力，允许以面向属性的方式描述组件，（iii）组件和配置由逻辑理论统一表示，这使我们能够建立系统的层次组织[2]。组件的配置被封装到子系统中，这些子系统可以通过子系统操作进行动态重构。在[2]中，我们已经证明了按照子系统和组件分层组织可重构系统的技术可能性。然而，这样做的确切困难和好处仍有待研究。 本文利用子系统的概念讨论了基于构件的系统的层次组织的一些重要优点，并提出了一种扩展到以前介绍的原型规范语言，以处理层次子系统。2时态规范语言在这一节中，我们描述了一种语言，层次子系统的研究是基于这种语言。这种语言是典型的，不应被视为真正的日常生活语言。它的目的只是为了研究更抽象的东西和说明性的方式来描述软件体系结构，并探讨我们提出的形式主义的能力。N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）6971UⓍADTADTADT语言是时态逻辑的一个简单前端。这种逻辑的主要特征是：（i）它是一阶的，（ii）时间是线性的，离散的，有一个初始时刻（即，时间的模型是N），（iii）除了通常的连接词和数量词外，逻辑还具有时间操作符（“ 下 一 个 “ ） ， Q （ “ 总 是 在 未 来 “ ） ， Q （ “ 最 终 在 未 来 “ ）和 （ “ 强 直 到 “ ） ， （ iv ） 一 些 函 数 和 谓 词 符 号 （ 称 为 可 伸 缩 ） 以状 态 依 赖 的 方 式 解 释 ， 尽 管 也 存 在 函数和具有状态独立解释的谓词（称为刚性）。这种逻辑是Manna-Pnueli逻辑的一种变体[12]，其中，那些解释依赖于国家的，已经被一般化。遗憾的是，由于篇幅所限，我们无法讨论有关这一逻辑的更多细节。我们请感兴趣的读者参考[12]以了解原始Manna-Pnueli逻辑的细节，并参考[2]以详细描述我们的逻辑变体。逻辑，加上某种语言翻译，构成了一个π-机构[6，10]。 这意味着一个有用的结构属性，使我们能够将属性从系统的较低层提升到它们所包含的子系统[2]。我们在下面总结了语言的主要结构及其特性。规范的风格受到[5]和相关工作的启发。特别是，我们遵循Community设计语言提出的几个想法[15]。2.1描述组件语言的最低层是由数 据 库 的规范组成的。它仅仅是一个理论表示在一个字母表没有可伸缩的符号（相当于一个一阶逻辑表征的数据表）。设SADT是数据类型规范ADT的排序集合;我们可以通过提供以下内容来定义组件签名：（i）一组SADT-索引读变量，（ii）一组SADT索引的属性，以及（iii）一组SADT索引的属性。行动 组件的状态由其属性确定，这些属性是就像命令式编程语言中的变量读变量只是一种特殊的属性，不受组件的控制，用作动作表示组件的参数化瞬时操作。组件的预期行为由时间公理描述，采用：（i）中指定的数据集，（ii）读取变量和属性作为可伸缩的0元函数符号，（iii）动作作为可伸缩的谓词符号，以及（iv）一个特殊的0元可伸缩谓词，它表示组件的活动性。组件的签名与用于验证组件的公理的组合实际上是对72N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）69→∈组件类型，我们称之为类定义。类定义被赋予一个名称，它也被用作特殊的0元可伸缩谓词，表示组件一些ADL中类定义的可能对应物是Darwin中的组件类型[11]，Acme [8]和Wright（在样式内）[3]中的组件定义，以及Community中的程序[15]。例2.1让我们举一个类定义的例子。假设我们想指定一个可以交换消息的“单元”网络我们把这些单位称为细胞。单元格与一个地址相关联，该地址是一个整数，并且对于一个单元格应该是唯一的消息中包含目的地小区我们可以将消息和地址建模为基本数据库。因此，让我们假设我们的数据类型规范ADT除了包含诸如布尔、字符串、整数等常见数据类型的规范之外，还包含特殊数据类型消息的规范。还有一个（静态）函数dest：message integer，它挑出嵌入在消息中的目的地址。有一个特殊的null的目的地址是unfined。我们可以通过定义一个类来指定细胞成分，如图1所示。Cell类有两个布尔读变量，in和out，分别表示单元格是否有传入消息，或者“环境”是否准备好接收来自单元格的传出消息。它还有一个整型属性，用来 保 存 单 元 格 的 地 址 ， 还 有 两 个 属 性 curr-in 和 curr-out 类 型 的message，分别用于存储刚收到的消息（准备被如前所述，组件的活动性由以类名命名的可伸缩谓词表示，即，谓词Cell。直觉上，谓词Cell在某个时刻的真值应该被解释为该组件在该时刻是活动的或“活的”。相比之下，如果谓词Cell在某个时刻不为真，则组件在该时刻不活动或类单元格包含六个（瞬时）动作。 操作c-init（整数）是一个初始化操作，它设置地址属性（见公理1）。 如公理2所表达的，c-init可以在单元组件的每个生命周期内被调用一次。公理2的直观解读是：“在所有状态下，对于所有xinteger的情况下，如果实例是活动的并且发生了c-init（x），那么在实例”2“的当前生命周期内它将不会再次发生公理2公理2使用了一个派生的时态算子，即W算子（“弱直到”）。N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）6973Ⓧ类单元格读取变量in，out：boolean属性address：integer;curr-in，curr-out：message操作c-init（integer），prod（message），send（message），get（message），cons（message），rem（）公理1. Q[x∈integer：Cellc-init（x）→（address=x）]3. Q[单元格n（地址/=n地址）→ nx∈integer：c-init（x）]2. Q[<$x∈integer：Cell<$c-init（x）→<$$>（<$$>y∈integer：c-init（y）W <$Cell）]5. Q[m∈message：Cellget（m）→（curr-in=m）]4. Q[m∈message：Cellget（m）→（（in=T）（curr-in=null））]（（curr-in/=null）（curr-in=m）（dest（m）=address））]6. Q[m∈message：Cellcons（m）→7. Q[m∈message：Cellcons（m）→（curr-in=null）]9. Q[单元格currem（）→ curr（curr-in=null）]8. Q[CelII]m（）→（（CelIn=1）nu ll）n（dest（curr-in）/=address））]11. Q[m∈message：Cellsend（m）→（（out=T）（curr-out=m））]10. Q[Celll（curr-in/=cur-in）→（m∈message：get（m）<$cons（m））<$rem（）]14. Q[m∈message：Cellprod（m）→（curr-out=m）]13. Q[m∈message：Cellprod（m）→（curr-out=null）]12. Q[m∈message：Cellsend（m）→（curr-out=null）]EndOfClass15. Q[Ce]l=（curr-out=/curr-out）→Fig. 1. 类单元：一个基本的类定义3 表示当组件处于活动状态时，属性地址只能由操作c-init修改。动作get从环境中获取传入的消息。 它有一个先决条件，即in必须为true（有一条消息等待获取），curr-in必须为null（在消费之前没有传入的消息被覆盖）（参见公理4）。在get（m）发生之后，curr-in在下一个状态中变成m（见公理5）。动作cons消耗先前获得的如果先前获得的消息不是针对组件的，则可以使用rem（）操作将其删除（参见公理8-9）。动作prod和send分别用于生成和发送消息它们的特征是公理11-14。从前面的例子中，读者可能会对一些时态操作符用于指定动作意图的方式有一个概念。特别地，该示例说明了时态算子Q（总是在未来）的使用，以表示组件的不变属性（如在所有公理中使用的），以及（下一个）指定动作的后置条件，如在公理1，5，7中。在公理中使用谓词Cell（根据类名命名的可伸缩谓词）乍一看似乎有点不自然。它74N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）69ADT有必要理解组件公理是绝对的，在这个意义上，它们谈论的是组件所参与的系统的所有可能状态，包括组件不存在的状态。 此外，组件语言中这些谓词的可用性允许规范执行某些约束。例如，约束一个类的具体化C被解释为一个时间理论的表示。表示的公理是通过将以下公理放在一起获得的：（i）作为类定义C的一部分明确提供的公理，（ii）为数据类型指定而给出的公理，以及（iii）一个特殊的隐式这个理论的定理，通过在[2]中提出的证明演算获得，表示C的所有“实例”的性质逻辑的单调性和类理论中ADT公理的包含允许我们在ADT中推理数据类型属性，然后对于我们的细胞类，相应理论的一个示例定理如下：还押和监禁不能同时发生”。这个性质，可以很容易地证明使用上述证明演算，在逻辑表示的公式：Q [Cell→ <$（rem（）（m∈message：cons（m）]。2.2描述相互作用我们选择将类定义定义为封闭的独立单元。也就是说，我们不允许类在它们的定义中引用其他类。这一点很重要，因为从逻辑的角度来看，它允许我们独立于系统的其他部分来推理组件属性。 但是，当然，我们需要使组件交互的方法。我们通过使用有用的协调概念来实现组件之间的通信。在这方面，我们的沟通手段非常接近社区[15]，尽管我们允许更多的灵活性。为了使组件相互作用，我们定义了关联。关联由一组参与者和一些公式组成，这些公式描述了交互。考虑图2中的关联定义。 这种关联定义了一种使细胞通信的它有两个细胞类型的参与者，s和tN. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）6975关联链接参与者s，t：单元连接1. （s. in=T）Participate（t. curr-out =/nu ll）3. （t. in= T）Participates（s.curr-out/=null）2. （s. out= T）Participate（t.curr-in=null）6. m∈ message：（t. send（m）→ s. get（m））5. m∈ message：（s. send（m）→ t. get（m））4. （t. out= T）Participants（s.curr-in=null）EndOfAssociation（来源和目标）。连接表明，如果两个单元格通过Link连接，则：（i）如果第二个单元格的curr-out属性不为空，则第一个单元格的in read变量为true，反之亦然;（ii）如果第二个单元格的curr-in属性为空，则第一个单元格的out read变量为true，反之亦然;（iii）第一个单元格的sendaction“调用”第二个单元格的get action，反之亦然。图二.关联链接：简单的关联。请注意，定义Link连接的公式将参与者作为自由变量。这些公式将被系统地转换，并将形成表征组件动态配置的理论的一部分。3子系统的一种表示法在上一节中，我们展示了如何分别通过类和关联来声明性地定义组件和连接器类型。 我们现在需要组合这些规范，以便构建交互组件的架构。我们建议通过定义我们所谓的子系统来做到这一点[1]。子系统是一个新的模块化单元，它包含一组动态可重构的交互组件。类是组件的模板，其内部结构是基本的，仅由其属性组成;另一方面，子系统，或者更准确地说，子系统实例，可以具有复杂的内部结构，由其内部活动组件及其互连组成。此外，子系统承认重构操作的定义，这可以动态地改变它们的内部结构。在以前的工作中，我们将子系统定义为复杂的组件，其内部状态是动态的，并且是由类的实例构建的（即，组件）通过关联的实例来关联（即，连接器）[1]。我们现在要扩展它，使子系统不仅可以由类的实例组成，而且还可以由更简单的子系统的子实例组成，76N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）69ADT允许系统的分级组织因此，我们将有两种类型的组件定义：类，定义简单的非结构化组件（即，定义聚合过程的基本情况）和子系统，子系统定义复杂组件，其结构是由简单组件的实例构建这是可行的，因为基本成分和聚合的语义是通过时间理论以类似的方式定义的，因此迭代定义聚合的过程没有技术限制[2]。然后，让我们提出一个子系统的扩展符号。 让ADT名称是一个保守的扩展，有一个额外的排序NAME和一个足够大的这个排序的常量集。排序常量NAME用于表示下层组件的标识符子系统签名由以下组成：（i）名称，（ii）基本属性和基本读取变量的有限集合，由一种ADT名称类型化，（iii）操作的有限集合，其参数由各种ADT 名称类型化。属性是子系统内部状态的一部分。读变量将用于允许子系统与其他子系统通信的目的。这些操作允许子系统进化。与在基本组件中使用操作相反，子系统中的操作可以通过创建或删除组件的实例以及创建或删除它们之间的连接来因此，我们可以将子系统的操作视为重构操作，这将在运行时改变子系统的结构方面。为了在逻辑上证明这一点，子系统Sub配备了一组有限的公理，这些公理是字母表ASub上的公式，由以下组成（i）扩展的数据类型规范ADTNAME，（ii）由类定义和其他更基本的子系统产生的可伸缩函数和谓词符号，向它们添加一个额外的排序参数NAME，（iii）灵活的谓词符号R：NAME，. ，每个关联定义的名称`ktimesxR与k个参与者，和（iv）一个可伸缩的谓词符号a：S1，.，S k为类型a（x1：S1，.，xk：Sk）。我们要求源于类定义的符号集合是不相交的，以便明确地确定一个符号所属的类。这只是为了使演示更简单。例3.1在定义了Cell和Link之后，我们可以考虑一个基本的子系统SubNet来表示Cell的动态聚合。更准确地说，子网是一个动态的单元集合，其中存在一个特殊的单元称为网关。子网内的所有其他单元都连接到网关，呈可以通过以下方式创建新单元格和删除现有单元格：N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）6977ADT子系统子网属性网关：NAME操作s-init（integer），add-cell（NAME），rem-cell（NAME）公理2. Q[n]：Su b Nett i il（n）n（n=/gateway）→Link（gateway，n）]1. Q[n，m：子网链路（n，m）→（n=网关）]4. Q[子网→小区（网关）]3. Q[子网→子网n：<$Link（n，n）]6. Q[n，m]：子网单元格（n）子网单元格（m）子网单元格（n5. Q[n：SubNet（gateway = n）→（（gateway = n）W<$SubNet）]/m）→（n. 地址/= m。地址）]9. Q[n：x∈integer：SubNetadd-cell（n，x）→ <$Cell（n）]8. Q[<$x∈integer：Sub Net<$s-init（x）→<$（<$n：Cell（n）→（n=gatewayy））]7. Q[x] ∈ integer：子网初始化（x）→网关。c-init（x）]10. Q[n]：n ∈x ∈ integer：SubNet n= add-cell（n，x）→ n（Cell（n）n.c-init（x））]11. Q[n：SubNet<$Cell（n）（Cell（n））→x∈integer：add-cell（n，x）]12. Q[n =n：子网中的rem-cell（n）→Cell（n）]13. Q[n：子网中的单元格（n）→子网中的单元格（<$Cell（n））]14. Q[n：子网子网信元（n）<$（<$Cell（n））→rem-cell（n）]子系统结束相应的操作。图3的子系统是一种可能的规范。公理1-3规定，当子系统处于活动状态时，单元以网关为中心排列成星形拓扑。 AX- IOMS 4-5表示网关是一个在子网的生命周期中不会改变的单元。 公理6对应于非正式的要求，即地址对于单元3必须是唯一的。公理7-8涉及初始化操作子系统，即s-init，以创建和初始化的网关。 最后，公理9-11和12-14解释了这些运算add-cell和rem-cell，用于在子网内创建和删除小区。图三. 子系统子网：基本子系统规范子系统被解释为时态理论，就像类一样。子系统Sub的时态理论由以下部分构成：（i）作为Sub规范的一部分明确提供的公理，（ii）NAME中的公理，以及（iii）较低层的类或子系统的公理，通过普遍量化添加到读取变量，属性和动作的额外参数NAME来相对化。 事 实上，请注意，子网子系统的公理使用类的语言（即，下层的组分）。例如，公理6和10使用[3]请注意，我们不能在细胞78N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）69关联S-Link参与者s，t：子网连接1. （s. gateway. in= T）Participate（t. gateway.curr-out/=null）3. （t. gateway. in= T）Participates（s. gateway.curr-out/=null）2. （s. gateway. out= T）Participate（t. gateway.curr-in=null）5. m∈ message：（s. gateway. send（m）→ t. gateway.get（m））4. （t. gateway. out= T）Participants（s.gateway. curr-in=null）EndOfAssociation6. m∈ message：（t. gateway. send（m）→ s. gateway.get（m））n.公理6中的地址）。这些前缀实际上是一种方便的方法，可以用来消除底层的类和子系统定义中的读变量、属性和操作中包含的额外NAME类型参数。也就是说，像n.address和n.c-init（x）这样的表达式实际上分别对应于address（n）和c-init（x，n）[1]。相对化过程有一个很好的性质：如果α是一组公式Γ的结果，那么α的相对化αJ是Γ [2]的相对化ΓJ这个性质的一个重要结果是，由于我们包含了较低层公理的相对化，定义到包含子系统中，所有定理（即，属性）被提升到包含子系统中。为了澄清这种情况，考虑例如以下公式：Q[m∈message：Cellcons（m）→（curr-in=null）]这是Cell中的一个平凡定理（实际上，它是一个公理），其直观的解读是：此属性作为公式提升到子网n：Q[他的直觉解读是： 并且对于某个消息m出现n.cons（m），则在系统的下一个状态中n的属性curr-in被设置为空4复杂子系统见图4。 关联S-Link：子系统之间的关联。在上一节中，我们允许子系统以更简单的子系统来定义。一个重要的限制是子系统的定义不能是循环的。这是由于子系统的语义是基于以下事实的：N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）6979子系统网络属性router，sn1，sn2：NAME操作conn（NAME），disconn（NAME）公理2. Q[网络→sn 1/=sn 2]1. Q[Network→（Cell（router）SubNet（sn1）SubNet（sn2））]3. Q[网络→S-Link（sn 1，sn 2）]4. Q[s]：网络连接→（（）链路（路由器，s。gateway）gateway））]6. Q[s1，s2，n，m]：网络子网（s1）子网（s2）子网（（Link（router，s. gateway））网关（路由器）gateway））]5. Q[s]：网络连接中断→子系统结束Cell（n，s1）<$Cell（m，s2）<$（s1=/s2）→（n. 加上ress/=m。（address）]较低层的类和子系统，如果子系统依赖性是循环的，这当然是不可能的为了说明如何定义更复杂的子系统，让我们进一步扩展前面的例子。现在我们有了细胞、链接和节点，我们可以定义一个由两个节点组成的网络为了允许这些子网进行通信，我们定义了一个（更高级别的）关联，如图4所示。这种关联通过连接相应的网关来连接两个网关，与Link连接小区的方式相同。这是对[1]中定义的关联的概括，因为我们现在允许子系统成为参与者，而不仅仅是基本组件。还要注意，多个网络现在可以很容易地定义为一个更高级别的子系统，如图5所示。前四个公理对应于结构约束。例如，公理3指示当网络处于活动状态时，网络sn 1和sn 2通过S-Link连接。网络可以与外部世界通信（例如，其它网络）通过路由器单元。操作conn和disconn管理网络中路由器的访问（参见公理4-5）。最后，公理6指出，两个不同的单元格不能有相同的地址。图五. 子系统网络：更高级别的子系统规范从这个例子中可以清楚地看出，更基本的子系统和组件的语言是如何在更高级别的子系统中合并和使用的。同样，逻辑的结构性属性允许我们将定理从规范的下层提升到上层。例如，子网属性Q[n：SubNetCell（n）（<$Cell（n））→rem-cell（n）]可以被提升到网络中：s：Q[80N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）69然后，我们可以在层次规范的不同层次上组合推理，以证明整个系统的属性。不幸的是，由于空间限制，我们无法在这里复制一个结合层次规范的所有层次的推理的证明。5结论我们已经提出了一个扩展的原型时间规格化语言，用于指定动态软件架构。扩展的目标是允许系统规范的分层组织，在可重构的子系统方面。我们已经概括了关联和子系统的概念，并给出了一个示例来说明表达能力的扩展。形式主义的一个主要特征是可以声明性地描述可重构系统，这也是我们工作的部分声明性规范往往比操作性规范更长;因此，模块化声明性规范的机制至关重要。子系统的概念补充了基本组件的概念，并允许我们进一步模块化规范。由于组件是分层描述的，使用类和子系统，作为封闭的独立单元，证明可以本地化到规范的相关子部分。我们已经展示了一些证据，证明这种逻辑对于指定动态软件体系结构来说是足够有表现力的。 我们相信，然后，逻辑是适合作为一个“推理框架”的正式ADL。此外，该逻辑可以用于向一些ADL提供声明性语义。ADL中的规范可以解释为逻辑，然后可以使用它的证明能力来推理规范的属性。我们目前正在探索这条工作线，将Community [15]规范映射到逻辑中，以便推理规范的属性即使对于简单的系统，规格往往是大而复杂的。尽管模块化机制有助于减轻证明工作，但软件工具的支持是必要的。目前，我们正在尝试使用斯坦福时间证明器（Stanford Temporal Prover，STeP）[4]来帮助我们的逻辑证明。引用[1] N. Aguirre和T.Maibaum，A Logical Basis for the Specification of ReconfigurableComponent- Based Systems，Proc.FASE 2003，华沙，波兰，LNCS 2621，Springer，2003。[2] N. Aguirre和T. 关于时间推理的一些制度要求N. Aguirre，T.Maibaum/Electronic Notes in Theoretical Computer Science 108（2004）6981Dynamic Reconfiguration，to appear in Proc. of Symposium on Verification：Theory andPractice，Taormina，Italy，LNCS，Springer，2003.[3] R. 艾伦河Douence和D.林文龙，《动态软件体系结构分析》，第二届中国软件工程学术研讨会论文集，北京，1998。[4] N. Bjorner，A. Browne，M.科隆湾Finkbeiner，Z. Manna，H. Sipma和T.陈晓，“反应式系统的时间特性：一种STeP方法”，系统设计中的形式化方法，第16卷，2000年。[5] J. Fiadeiro 和 T. Maibaum ， Temporal Theories as Modularisation Units for ConcurrentSystem Specification。计算的形式方面，卷。号43，Springer，1992.[6] J. Fiadeiro和A. Sernadas，Structuring Theories on Consequence，in D. Sannella和A. Tarlecki（eds），Recent Trends in Data Type Specification，LNCS 332，Springer，1988。[7] D. Garlan，软件架构：一个路线图，在软件工程的未来，A。Filkenstein（ed），ACM Press，2000.[8] D. 加兰河Monroe和D.王文，《一种结构描述交换语言》，中国计算机科学院学报[9] D. Garlan和D. Perry，软件架构。小组介绍。In Proc. of ICSE[10] Goguen 和 R. Burstall ， Institutions ： Abstract Model Theory for Specification andProgramming，Journal of the ACM 39（1）：95-146，ACM Press，1992.[11] J. Magee，N.Dulay，S.Eisenbach和J.Kramer，《分布式软件体系结构》，载于Proc. of ESEC[12] Z. Manna和A. Pnueli，反应和并发系统的时态逻辑，Springer，1991。[13] N. Medvidovic，ADL和动态架构变化，在Proc. of ISAW 96，1996。[14] B. 面向对象软件结构，第二版，北京，2000。[15] M. Wermelinger和J. Fiadeiro，A Graph Transformation Approach to Software ArchitectureReconfiguration，载于Science of Computer Programming 44，Elsevier，2002。