视觉协调网络中的体系结构互操作性检查

理论计算机科学电子笔记181（2007）81-96www.elsevier.com/locate/entcs视觉协调网络中的体系结构互操作性检查1DavidSafra'nek2捷克布尔诺马萨里克大学信息学院计算机科学系摘要在本文中，体系结构互操作性检查的方法[1]被重新审视，并被用于体系结构的互操作性检查，其中连接器和组件被视为体系结构描述的行为上和表达上不同的元素。在此基础上，建立了图形化语言Visual CoordinationNetworks的体系结构互操作性检查框架。关键词：可视化协调网络，体系结构互操作性检查，可视化规范，并发系统，外生协调模型1介绍分层的基于组件的系统设计可以以精确的操作语义为基础，其允许将传统的软件和硬件设计方法与从进程代数理论已知的形式化方法（例如，精化、等价或模型检查）。此外，在体系结构描述中，协调（交互）方面的建模与实体（计算）方面的建模在语法和在这样的环境中，可以通过架构描述来确保指定的系统通过关于组件协作的互操作性正确性的设计是正确的。在本文中，我们提出了一个形式化的体系结构互操作性检查方法的视觉形式化视觉协调网络（VCN）。这种语言是基于我们以前的工作[12]。1这项工作得到了捷克共和国资助机构资助号201/06/1338，捷克科学院资助号1 ET 408050503，以及理论计算机科学研究所（ITI）研究中心项目号1 ET 408050503的支持。1M0021620808。2电子邮件地址：xsafran1@fi.muni.cz1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.05582D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81VCN采用外生协调模型[3]。在这样的模型中，协调方面在语义上与计算方面分离。VCN可以被看作是静态的体系结构图，指定组件之间的连接。为了捕获协调方面，引入了连接器-所谓的VCN总线。通过特定的VCN总线，某些协调模型的行为被指定。1.1相关工作通信系统的图演算[6]和体系结构交互图[9]代表了以前在这个主题上的工作。据我们所知，这些语言的互操作性方面都没有研究。在协调语言的社区中，有一个大的语言组这个领域最新的语言是Reo[4]。Reo支持控制驱动的外生协调，并且与面向设计的VCN相比是面向执行的。在硬件和软件设计的过程中，将设计中的系统的行为方面与体系结构方面分开处理似乎是有用的。这种方面分离的思想已经在大多数关于架构描述语言的工作中得到了解决[7]。这些原则也在UML语言的最新版本中使用。1.1.1我们的贡献有一个详尽的作品贝尔纳多等人。讨论了在传统过程代数框架中形式化的体系结构描述的互操作性检查问题文[5]证明了，对于非循环部件拓扑的检验，必须检验所有相互连接部件对的交互相容性。这种相容性的概念是基于一对中两个分量的弱双相似性。这两个组件的抽象被认为只包括相互作用的动作，而所有其他动作都是隐藏的。在[1]中，这种兼容性检查的方法已被扩展到任意网络拓扑结构，其中可以包括组件之间的循环关系。我们表明，类似的方法可以扩展到VCN的行为模型。与[1，5]相反，VCN中架构的依赖图是双部件的，因为VCN将连接器和组件区分为架构的两个语义 换句话说，这样的扩展必须定义任何两个相邻节点之间的架构兼容性的概念，这两个相邻节点被赋予一对连接器和一个组件。 此外，VCN引入了一个集合标记的转换操作语义来捕获连接器的行为模型。这个扩展增加了所支持的协调模型的表达能力。在本文中，架构互操作性的概念被重新审视和扩展，以捕捉这样的设置的需求。特别是，在VCN中没有并行复合算子的传统概念，因此文[1，5]中的一般同余结果不能直接应用于此。本文的主要结果表明文[1]的思想是如何推广到VCN环境的。D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81832视觉协调网络2.1概述在最抽象的视图层，VCN引入了两个独立层的层次结构-计算层 和协调层。 计算层关注设计中系统的计算方面，而协调层处理交互方面。这种分层结构的原理反映了基于组件的系统设计的本质，并受到软件体系结构描述工作的启发（即，Wright [2]）。在我们的设置中，计算层被视为系统规范的低级层，协调层依赖于此。因此，从设计者的角度来看，自顶向下和自底向上的设计方法都可以应用在使用VCN的系统设计中。一方面，VCN允许计算层被认为是一个补充层，可以添加到建模的系统层次结构在特定的设计过程中（自顶向下的方法）。另一方面，可以首先指定组件的计算，而协调层可以稍后添加（自底向上方法）。2.1.1协调层VCN协调层修改了Wright [2]中引入的概念，其主要思想这种静态结构的概念涉及由特定连接器永久协调的并发运行组件的拓扑。此拓扑由将组件接口端口连接到特定连接器的点对点链路确定。表示组件和连接器的这种拓扑的相应VCN构造被称为网络。图1中描绘了网络的示例。get1显示复位get2Fig. 1.由一条总线与Wright类似，连接器被视为一等公民（与组件处于相同的规范级别在VCN设置中，连接器称为总线。总线代表控制组件交互的协调机制由总线表示的协调模型的特征在于称为协作的原子动作，其具有特定网络中的一组某些组件的原子多同步的含义。INI1tempCOORD忽米ini2触摸开关联系我们联系我们84D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）812.1.2计算层组件计算由VCN叶子描述。VCN叶子是计算层的基石在我们的设置中，叶子被假定为系统组件的抽象计算模型更具体地说，叶子是VCN结构中的原子元素，可以在任意形式主义中指定，用于反应式计算的正式据推测，这种形式主义，可用于此目的是兼容的语义模型中采用的VCN。一般来说，这种兼容的形式主义的潜在集合包括任何可以被编码到标记转换系统中的反应式计算描述语言。2.1.3网络层次计算层是VCN层次结构的最底层。它由在特定系统设计中使用的所有叶子的集合如前所述，叶子直接表示组件的计算，并通过总线互连以产生网络拓扑。在自然意义上，这种由叶子和总线组成的网络拓扑可以抽象地看作是一个隐藏着复杂行为的黑盒子（通过总线协调的叶子计算来定义）。更具体地说，计算不仅由叶子表示，而且由整个网络拓扑表示。这个想法使我们认为组件的概念比叶子的概念更抽象。特别是，叶子或网络都可以被认为是VCN思维方式的一个组成部分将网络作为一个组件的可能性允许协调层具有更多层次结构。3VCN结构及其行为模型在本节中，我们将介绍VCN语言的简化版本。所考虑的简化集中在VCN网络上，以开发架构互操作性检查的框架。3.1结构术语类似于类似于状态图的形式主义[8]，VCN的语义是由文本术语定义的。在VCN中，我们区分了形式化系统架构的结构术语和形式化行为模型（组件和网络计算）的行为术语。VCN的关键元素是形成组件接口的端口。每个端口由一个标签标识，该标签在特定层次结构级别的范围内是明确的。一个端口可以被感应到作为在特定组件计算期间观察到的事件发生的位置。我们区分两种端口定义3.1将L固定为可数标签集，并假设τ∈/L。Def neportsD. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8185=={nw，in nw∈ W，i∈ N}，且R={R，i∈ N}.作为集合P的成员DFDF=L × {in，out}。进一步定义P输出端口的集合W={p∈ P <$p=l，输出端口，l∈L}和输入端口DFR={p∈ P <$p=<$l，in<$l，l∈ L}.为了确保每个端口标签在特定的网络范围内是唯一的，我们用一个索引来注释每个端口，该索引表示它所属的组件特别是，我们假设网络中的每个组件都由唯一的自然数标识定义3.2定义带注释的端口集合Pdf{p，ip∈ P，i∈ N}。进一步将相应的投影定义为带注释的输出端口和带注释的输入端口的集合，WDFDF注3.3对于某些i∈ N，我们将由i标注的端口集合表示为DF={p，ip∈ P}。 此外，集合P的成员通常表示为用符号p，p1，p2，.. .，W的成员由w，w1，w2，. . .，最后，由r，r1，r2，.. .请注意，WR=。对于某个i∈ N，记为pi，我们的意思是np，in ∈ P。因此，由i∈ N标注的输入端口r∈ R记为ri。带注释的输出端口以相同的方式表示。每当注释编号i在注释端口pi的特定上下文中不重要时，我们省略上面的索引对于一个特定的（未注释的）端口集合P∈ P，包含这些端口的集合都由i∈ N注释，表示为Pi。对于所有注释索引的端口集，DF使用符号P，P=i∈NPi。现在我们介绍总线概念的一个基本概念-合作的概念。协作可以被感测为一组端口，当协作发生时，相应的计算事件在该组端口上原子地同步。定义3.4设W中国RR有限的港口。 定义合作作为一对R_W，R_R，表示为R_W/R_R，满足：(1) 其中，j ∈ N，w1，w2∈ W，r1，r2∈ R. （w1i，w2j ∈ W <$i/= j）n（r1i，r2j∈Rni j）我们说一个端口p包含在一个合作 c：=中，并写p∈c，如果p∈W或p∈R。所有合作的集合表示为Coops。条件（1）确保了每个组件的最多一个输入端口或一个输出端口可以参与协作的自然要求定义3.5将总线B定义为一组有限的协作B_Coops，使得B.对于特定总线B，相应的协作集合被表示为coop（B）。所有总线的可数集合记为总线。总线成员通常表示为B，B1，B2，... .DF总线B的输入 记为In（B），定义为集合In（B）={Wǁ ⟨W/R ⟩ ∈B}. 类似地，总线B的输出表示为Out（B），DF定义为集合Out（B）={RW/R∈B}。Pi86D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81定义3.6将链路关系L定义为关系L∈ P×Buses，对于每个B∈Buses，满足以下所有条件：（2）n ∈i，j ∈ N，p1i，p2j ∈ P，n ∈p1i，B∈ L. B∈ L<$p1/= p2<$ijp ∈ P。B∈ L，b ∈ c。 p ∈ c（3）n∈ W，w∈In（B）n ∈W，B∈Lr∈ R.r∈Out（B）r∈R，B∈LDF将总线B的所有链路的集合表示为链路（B，L），并定义链路（B，L）={l <$p ∈ P.l=<$p，B <$∈ L}.上述定义中的条件（2）确保最多一个链路可以为特定组件接口端口定义。条件集合（3）保证特定总线嵌入到特定链路关系中的一致性。更确切地说，链接到特定总线的所有端口必须通过某种协作来反映，并且对于特定总线的任何协作的每个端口，必须存在将总线与相应端口连接的链路注3.7对于某个链路关系L的特定链路l∈L，我们将其端口表示为DF如port（l）= p，其中l <$p，B<$p。定义3.8将结构项的集合（记为Tst）定义为满足以下条件的最小集合：(i) A∈Tst是一片叶子DF(ii) N∈Tst，如果N是一个k可定义的，则N=kC<$，B<$，L，其中• C =C1，.，C n nn for some n > 0是分量项的元组，对于每个i∈ {1，.，n}，C i={S i，I i，G i}是满足以下条件的分量：(a) Ii端口的有限集合是一个接口，记为I（Ci）(b) Si∈Tst(c) Gi是一个门，它将组件体Si映射到接口Ii• B<$=B1， .. . ，Bm≥0表示总线已关闭• L是满足以下条件的链接关系：Li∈{1，.，n}I ii × {B ii ∈ {1，.，{\fnSimHei\bord1\shad1\pos（200，288）}此外，我们说端口p是网络N中的自由端口，如果它没有连接到链路。我们在这里不定义门的概念，因为我们只关注架构的内部级别（hor-izhetry）方面。然而，门是VCN关于层间（垂直）方面的重要元素[12]。为了本文的目的，我们把一个门作为一个内射映射门G，它将一个组件体的端口映射到相应接口的端口。D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8187同步广播DF3.2行为模型3.2.1叶每个叶子的特征在于在其计算期间可能发生的事件集。叶的行为模型由传统的转移系统S=S × S，T，s0∈S确定，其中转移关系的形式为T= S×P×S.表示为Φ（S）的叶S的行为模型由初始状态s0确定，Φ（S）=s0. τ-事件代表无声事件（环境无法观察到）。3.2.2巴士总线的特定行为模型表示协调机制。总线行为的示例如图2所示。该模型反映了协调触摸/−1触摸/ini 1，ini 2，2一位缓冲（humi-bubble'同步通道（temp−>get1）−/get2temp，3一位缓冲区触摸/−图二、COORD总线（协作机）的行为模型在图1的网络中，特别地，它处理组件Temp传感器、代表天气条件传感器的Humi传感器、代表报告当前剧院信息的LCD面板的显示组件、以及启动整个系统计算的Switch组件。这些组件的协调模型由总线COORD确定。这种总线的含义是协调行为，它结合了原子广播，同步通道，抑制器和一个地方的缓冲器。在该特定示例中由总线COORD确定的协调模型的总体原理可以概括为以下阶段：(i) 在初始阶段，按下触摸触发器会导致通过ini1、ini 2和复位端口向相应组件广播初始化信号。这种广播是在不可分割的时刻以原子方式执行的，以确保系统对启动信号的即时和不间断的反应。(ii) 在启动之后，协调模型等待在生产者（T emp传感器和Humi传感器）输出端口上发信号通知信息。在该阶段，它还能够接收触摸信号，以保持启动开关的阻塞。88D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81BBJ当温度和湿度信息出现在相应的端口上时，协调模型的作用就像同步通道（将温度信息中继到get1端口）和一个位置缓冲器（将湿度信息存储到内部存储器-状态（3））。(iii) 在填充缓冲器之后，存储在缓冲器中的信息被发送到get2端口。它确保get1和get2端口以给定顺序的序列填充有适当的信息（即，当前天气状况的信息可以总是以预定顺序出现在显示面板上）。(iv) 协调模型返回到初始阶段（i）。上面描述的协调行为可以被正式地捕获为一个带有合作标签的transi- tion系统 我们把这种变迁系统的变体称为合作机。合作机器通过以下定义正式声明：定义3.9假设B是一辆公共汽车。 B的合作机，记为cm（B），DF元组cm（B）=<$Q，T，q0<$，其中• Q是状态的有限集合，•q0∈Q是一个初始状态，• T<$Q×coop（B）×Q是一个有限跃迁关系。注3.10对于给定的总线B，协作机cm（B）的所有状态的集合记为Q（B）。此外，合作机cm（B）的初始状态表示为ΦB（B）。对于某些q，q j ∈ Q（ B ） 和d <$W/R<$∈ B ， <$q ， <$W/R<$ ， q j <$∈T 的 事 实 证 明 了dq→W/RqJ. 除此之外，所有的数据库都位于可以从一个状态q∈Q（B）。 q→W/RqJ}。DFQ（B）记为en（q），en（q）={q∈3.2.3组件和网络定义3.11对于每个组件C=S，I，G，和每个网络或叶配置S，定义组件配置S，I，G，。组件C的行为模型表示为ΦC（C），并由S的初始状态确定。从形式上讲，DFΦ C（S，I，G）= Φ（S），I，G.定义3.12将网络配置的集合定义为{1，..， cn，q1，..， q m<$n，m ∈ N，c1，.， cn. . . 组件配置，q1∈Q（B1），.，q m∈Q（B m）.总线状态}网络的行为模型N= NC1，..，C n，B1，.，B m，L记为DFΦ（N）和定义的Φ（N）= ΦC（C1），.， Φ C（C n）n，ΦB（B1），.， Φ B（B m）设N = N =1，..， cn，q1，.， q m表示网络配置。通过符号N[ci：=cJ]，我们表示仅在第i个组件配置中与N不同的网络配置，前提是组件配置ci被替换为cJi。D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8189→NN⎥我我类似地，通过N[qj：=qJ]的旋转，如果总线状态qj被替换，则在仅在第j个总线状态中与N不同的情况下，不需要工作k个常数在QJ。对于某个θ∈ {1，.，n}表示N [i∈θci ：=cJi]网络配置，在θ中包含的所有元件位置上与N有偏差，条件是对于某些i∈θ，每个元件配置ci都用配置cJi替换。此外，在θ中包括的所有组件位置以及另外在已经移动到状态qJ的总线Bj的第j个状态中与N不同的网络配置是J J表示为N[i∈θ c i：= c i，q j：= q].对于任意类型的任意配置t，记en（t）为所有事件的集合dfJeJ它可以从t演化而来，en（t）={e∈t .t→t}，其中相关的过渡关系。注意，内部τ事件也可以包括在en（t）.现在，我们提出结构操作语义规则，从基本实体（总线和叶子）的行为模型导出组件和网络的抽象模型。第一条规则定义了最底层组件的操作语义。设C=S，I，G是一个分量，S是一片叶子。C的操作语义由推理规则给出的相关组件配置上的转换关系s→es ssj（一）埃斯岛gateG−→（五）CsJ，I，Ge∈en（s）设C =<$N，I，G是一个分量，N =<$<$C1，C2，.，C n，B1，.，B m，La网络。C的操作语义由相关组件配置上的转换关系' → C '定义（二）NEIJ科隆，I，G门G（e）NJ，I，G⎡ ⎤i ∈ {1，.，n}n∈ en（N）− →C网络N的操作模型由网络配置上的转移关系“→ N”确定下面的规则捕获组件在空闲端口上执行操作⎡ ⎤c→eCJN =ci，..，cn，q（三）我N→eiCN[c⎢⎢：=cJ]e∈en（c）⎦N iei是一个自由港最后，我们提出了负责网络协调的规则。在每个网络配置中，从所有启用的合作中选择要执行的最大合作。在我们陈述同步规则本身之前，我们定义了实现这种选择的最大启用合作的概念。定 义 3.13 设 N=N =1 ， ... ， cn ， q1， . ， q m 表 示 网 络 配 置 。 进 一 步 设 <$W/R<$∈Coops是满足<$W/R <$∈en（q j）的合作，其中j∈ {1，.，m}。我们说，在配置N中启用了写W/R，并且启用了写（写W/R，N），如果并且90D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81⎢J⎥只有当存在满足以下条件的端口集合P_p_P时• 如果对于某个i∈ {1，.，n}则e i∈ en（ci）.• e∈P惠e∈W或e∈R。我们说W/R是N的q j中的最大使能合作，写maxenabled（W/R，N，q j）当且 仅 当 enabled （ W/R ， N ） 和 WJ/RJ∈en （ qj ） 。 （ WJ<$W<$RJ<$R ）<$（WJ<$W =<$RJ<$R=<$）。以下规则负责网络协调：W/RJ⎡ej⎤N= 1，.. ，cn，q1，.. ，qj，.. ，qm⎥（四）qj→Bjτqj <$e i ∈ MBj. ci→C] cimaxenabled（⎢ ⎥dfN→N[C：=cJ，q：=qJ]MBj=WRNi∈θii jjDFIθ={i∈MBj}4网络互操作性正确性本文提出的VCN 虚拟模型互操作性正确性检验的形式化解决方案是对Bernardo等人在文献[1]中提出并证明的方法的一种改进和扩展。受此启发，我们建立了检查VCN项的弱双模拟等价所由于弱互模拟等价保持了所有具有弱菱形和盒子算子的μ演算公式的有效性，因此互操作性检查方法包括一组详尽的有趣性质，包括死锁自由度。互操作性检查的原理依赖于在特定的网络层次结构中搜索这样一种情况的思想，即被检查的属性的有效性被某些组件和总线的交互所违反，而这些组件关于VCN图的归纳定义，互操作性检查遍历从叶子到更高网络级别的层次结构。请注意，Bernardo等人的方法处理的是由统一组件组成的体系结构，这些组件通过链路连接，可以具有一对多的特性。无论如何，这些链接都是静态（无状态）连接器。 没有像Wright或我们的方法中那样明确的连接器概念。然而，连接器仍然可以显式地建模为逻辑上与普通组件不同的组件。什么是不可能的，有原子多对多合作的连接器动态建模，因为我们的方法允许通过总线的行为模型。这就是为什么[1]的结果不能直接应用于开发VCN行为模型我们遵循利用和推广这些结果以适应公共汽车的行为模型的特点4.我的世界1对于Ci和B j的组合，如果C<$，B<$，L<$∈Tst，表示Llinks（Ci，Bj），Ci和Bj之间的所有链路的集合：DFLlinks（C i，B j）={l ∈ links（B j，L）p ∈ I i. port（l）= p i}D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8191γ⇔ ⟨γ定义4.2设N= N，C1，...，C n，B1，.，B m，La网络。定义de-DFN的悬挂图，记为G（N），作为二部图G（N）= n {C1，...，C n}{B1，...，其中，E以如下方式定义：DFE={<$Ci，Bj<$$>Llinks（Ci，Bj）<$}在接下来的部分中，我们将假设一个模态μ演算的公式来表示一些互操作性安全性质。这种性质的一个例子可以是死锁自由度，用公式νZ表示. [[−]]Z.这个公式的一个重要特点 独立于行为模型字母表。在前一节中，合作机已经作为特殊的变迁系统被引入，合作出现在变迁标签中。因此，我们首先利用传统的（弱）互模拟等价，以建立所谓的合作标记弱互模拟的概念。4.我的世界3L etγ∈C oops表示Coperations的等式。确定以下合作顺序DF• γ=π，ifγ=π/π;•东风J吉吉γ=γ，ifγ=γ/γγ表示·γWheereγ/=0。γDF公司简介公司简介连续跃迁的顺序为：<$B=（→B）→B（→B）。定义4.4设B1和B2总线.进一步设q∈Q（B1），b∈Q（B2）各合作机的状态.我们说q和b是（弱）双相似的，并且写q<$clb当且仅当对于每个γ∈B1<$B2，以下两个条件都成立：(i) 如果qJ JγγJJclJ→B1q 然后，∈Q（B2）.b<$B2b而qB.(ii) 如果bJ JγγJJclJ→B2b 然后，∈Q（B1）.q<$B1qB.Q.互操作性检查的基本思想是基于所谓的兼容性的概念，这是基于对网络中组件和总线的行为进行成对比较。更具体地，考虑在组件和总线之间的链路上观察到的行为。 为了实现这种比较，我们定义了总线行为到特定链接子集的投影。定义4.5设N= N，C1，...，C n，B1，.，B m∈，L∈ a网络，设B j∈ {1，.， m}为总线，cm（Bj）=<$Q，T，q0为协作机，Lj<$L为链路关系。定义LJ -Bj的投影，表示为π（Bj，LJ），作为总线BJ，JdfJ由协作机确定的语义cm（B）= Q，T，q0TJ的定义如下<$q，<$WJ/RJ<$，qJ<$∈TJdfq，<$W/R<$，qJ <$∈T日本民主力量党J JdfJ其中W=W端口（Bj，L）和R=R个端口（Bj，L）。总线BJ被定义为出现在TJ的标签中的所有合作的集合。92D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81→J⎢J⎥⎣⎦注意，合作标记的合作机器的转移关系可以被正式理解为用于确定VCN术语的操作语义这种经典的转移关系可以提升为合作标记转移关系的形式。更确切地说，我们可以考虑VCN项的行为模型，其形式为所谓的饱和合作机器（定义如下）。这样就实现了对VCN术语行为分析的统一框架在这样一种情况下，我们将内部τ事件表示为空的合作/。定义4.6合作机cm（B）被称为饱和的，如果cm（B）的每个转移具有满足以下可能性之一的形式：• b对某个w∈ W，b {w}/;• b∈R，对于s ∈R，b∈R/{r}∈R;• b不稳定/不稳定。为了分析网络中总线和特定组件的互操作性，我们需要研究网络的内部行为。更具体地说，合作不能隐藏在这样的分析中。特别是，我们需要观察网络链接关系或其特定子集上发生的合作。为了捕捉关于某种链接关系L的网络行为的这种观察，我们定义了网络的L-可观察模型该操作模型是基于合作标记的转移关系。在下面的定义中，给出了L-可观测模型的概念，并因此用于形式化相容性的概念。定义4.7设N= N，C1，.，C n，B1，.，B m∈ T，L∈T是一个网络。定义网络N的L，通过以下规则在网络配置上定义的过渡关系→L，这些规则是规则（3，4）的修改：c →ecJ⎡ ⎤N= 1，..，ci，..，cn，q⎢ ⎥阿吉 什（3J）iC⎢γje是自由港⎧⎥⎨我的N→LN[ci：=c]df如果e∈ W，γ=⎦当e ∈ R时，⎡ ⎤（4J）W/RjBjJ∈i∈ MB.Ci→eC cJiN=1，.. ，cn，q1，.. ，qj，.. ，qm⎢ ⎥maxenabled（⎢ ⎥W/RjjdfN→LN[i∈θ ci：=ci，qj：=qj]MBj=WRDF我θ={i∈ ∈MBj}网络N的 L-观测值，记为ΦL（N），与普通行为模型的情况一样，由初始网络配置Φ（N）确定，但采用→L而不是→N。定义4.8设N= N，C1，...，C n，B1，.，B m，La网络，设C i=i ∈S，I，G∈ S和B j（对于i ∈ {1，.， n}，j ∈ {1，.， m}）G（N）的相邻节点。进一步令LjJdf{l∈links（B，L）p∈I. pi= port（l）}。L定义为链接关系L=jQQJD. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8193我们说Ci在N中与Bj相容，并且写Ci0NBj，当且仅当ΦB（BJ）S，IJ，Gj，，LJ），其中•日本民主力量党DFJII=I<$P其中P={p∈I<$l∈L，i∈ N.p=port（l）}，• GJ定义为G限制在IJ的端口。非循环网络拓扑的一个重要子部分是所谓的星型拓扑。直观地说，星型拓扑是一组连接到特定非循环网络中同一总线的所有组件。这种结构的重要性依赖于这样一个事实，即为了检查互操作性，它需要检查中央总线与特定星形拓扑中包含的每个组件的兼容性。这个结果包含在一般定理4.11中。为了使星形拓扑的概念更加精确，我们首先正式地引入了子网的概念。定义4.9Let N=⟨⟨C1, ..., C n，B1，.，B m，L∈ Tsta network.对于某些nJ≤n和mJ≤m，将N的子网NJ定义为网络NJ=⟨⟨CJ，..., CJj，BJ，.， BJj，LJ∈ Tst满足：1n1m• {CJ，....， CJJ}{C1，.， Cn}和{BJ，....， BJJ}{B1，.，{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}1N•日本民主力量党1mJ J J JL ={l∈L<$l∈Llinks（C，B）<$C∈ {C1，.，CnJ}<$B ∈ {B1，，BmJ}}• 每个B ∈ {BJ，....， BJJ}定义为π（B j，LJ），其中j ∈ {1，.， m}。1m对某些j ∈的进一步定义 {1，.，m}是N中B j的星形拓扑，J JdfJJ J J子网NN的形式为 N=C1，.，Cnj，B，L，其中每个CJ∈ {CJ，.， CJJ}满足Llinks（CJ，B j）<$.i1ni在检查网络互操作性时，需要特别注意循环组件关系的存在图3中描述了循环拓扑中互操作性正确性违反的示例。如果我们把星型拓扑⟨⟨CJ,CJ⟩,⟨π(B, L)⟩, L⟩df{in1，B，out1，B，in2，B，out2，B}1 21，L=1111其中分量CJ、CJ是投影到L中的链路的C1、C2，则这样的子网-1 2工作没有死锁。类似地，这同样适用于总线B2的星形拓扑。然而，如果我们考虑整个循环拓扑，可能会出现死锁情况，如图中过渡系统的暗态所示为了解决上述问题，我们提出了本文的主要结果，声明了一组必要和充分的条件，以确保任意网络拓扑满足某些性质。在下面的定理中，最大圈是指网络依赖图中不严格包含在图的某个较大圈中的每个子图此外，对于网络依赖图的每个最大圈Ω，我们考虑相应的子网络，即所谓的Ω-子网络，它包含圈的所有总线和组件以及限制于它们的链接关系。此外，我们定义一个循环的边界来表示这些组件和总线的集合，每个组件和总线都由以下语句之一标识：• 至少有一个自由端口的循环部件。94D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81阿库阿库阿肯阿肯B2B1出来在出来在C2C1第一条：B1、B2：第二条：在吗？ackin？in/out输出/输入滚出去！ackout！在吗？ackin？滚出去！ackout！图3.第三章。死锁违反网络互操作性的正确性• 自行车的一个部件，与自行车外部的总线相连。• 循环中的总线，它与循环外的部件相连。定义4.10设N= N，C1，.，C n，B1，.，B m网，L_a网和G（N）的Ω某（极大）圈.定义Ω的边界，记为β（Ω），作为集合DFβ（Ω）={C∈Ω<$P∈P ts（I（C）），<$B∈Ω. p∈/ports（Llinks（B，C））}<${B∈Ω <$Nγ∈B，p∈γ，<$C∈Ω. p∈/ports（Llinks（B，C））}定理4.11设N= N ∈C1，...，C n，B1，.，B m∈ N，L∈ N是一个网络，G（N）是一个任意形状的连通图. 当且仅当以下条件成立时，N满足：(i) 每个总线Bj∈ {B1，.，B m}满意。(ii) 每个分量Ci ∈ {Ci，.，C n}满意度(iii) 不包括在G（N）的任何循环中的每个总线B对于每个C满足C 0 B，使得Llinks（C，B）/= 0。(iv) G（N）的每个极大圈Ω的每个母线B∈β（Ω）满足C0B，对于每个C使得Llinks（C，B）/= Ω且C不包含在Ω中。(v) 对于G（N）的每个极大圈Ω，N的Ω-子网络满足为了实现任意网络拓扑的互操作性检查，并以这种方式建设性地证明上述定理，我们应用逐步减少整个潜在的循环拓扑的思想，一个较小的非循环拓扑，其行为模型观测等价于原始拓扑。关于这样一个保持循环拓扑到非循环拓扑的还原的观察行为的直觉如下。整个网络中的每一个循环都被替换为一个星型拓扑，该星型拓扑具有与原始循环拓扑等价的行为模型这种星形拓扑D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8195的定义方式是，所有相关链接96D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）81从该循环的组件和总线到该循环外部的总线和组件的引导被重新映射到从该星形拓扑的组件和总线引导的等效链路这种替换必须满足的重要特性是这些组件和总线的相互兼容性此外，星型拓扑本身必须满足其组件与形成其中心的总线的兼容性。然后通过用这种兼容的星形拓扑替换所有的循环子网络，实现了整个网络的非循环性，并且互操作性检查依赖于检查总线和组件的相互兼容性该定理的形式证明是基于本段中描述的直觉，并在本文的完整版本中精确给出[11]。5结论与未来工作本文提出了一种简化的VCN语言，用于基于构件的并发系统的层次规范化。该语言的关键概念是总线，总线代表系统体系结构中使用的协调模型。我们已经利用了[5]的过程代数方法，并证明了它的扩展，由于VCN的特定特征，它没有直接包含在传统的过程代数方法中用于体系结构描述。我们目前正在实现一个图形工具[10]，它允许简单地创建和修改VCN图在我们以后的工作中，我们将按照[1]的方式讨论VCN模型的内生和外生扩展。我们还旨在将架构互操作性检查扩展到允许总线广义定义的VCN总线类[12]。引用[1] Alessandro Aldini和Marco Bernardo 进程代数的可用性Theor. Comput. Sci. ，335（2-3）：281[2] R. Allen和D.加兰架构连接的正式基础。ACM Trans. Softw.工程师，Methodol。，6（3）：213[3] F.阿巴布协调是什么意思？荷兰理论计算机科学协会（NVTI），1998年。[4] 法哈德·阿巴布Reo：一个基于通道的组件组合协调模型。数学。Comp. Sci. ，14（3）：329[5] 马可·贝尔纳多，保罗·钱卡里尼和洛伦佐·多纳蒂洛。用进程代数构建软件系统族。ACM Trans. Softw.工程师，Methodol。，11（4）：386[6] R. Cleaveland，X. Du和S. A.斯莫尔卡GCCS：一种用于系统规范的图形协调语言。在COORD'00的会议记录中LNCS，Springer Verlag，2000年。[7] Paul C.克莱门茨体系结构描述语言综述。IWSSD'96：Proceedings of the 8th International Workshop onSoftware Specification and Design，第16页，华盛顿特区，美国，1996年IEEE计算机协会。[8] D.哈雷尔Statecharts：A Visual Formalism for Complex Systems.技术报告，魏茨曼研究所，1987年。[9] A. Ray和R.克里夫兰架构交互图：系统建模的辅助工具。2003年ICSE会议记录。IEEE，2003年。D. Šafránek/Electronic Notes in Theoretical Computer Science 181（2007）8197[10] Z. 瑞哈克VCNE项目主页。ParaDiSe实验室，Masaryk University Brno，2006年。http://www.fi.muni.cz/www.example.com[11]D. 我的天啊。在Vi s ualCor di na ti nnntwor ks中，一个特定的结构性整数可恢复性C h e k i n g。TechnicalReport FIMU-RS-2006，Faculty of Informatics，Masaryk University Brno，2006.[12] D.这是 一 个 很 好 的 例 子 。 是的 。VCD ： AVi s ualFormali s morSpeionorH erogeneousSoftar eArchitectures.计算机科学的理论与实践：第31届计算机科学理论与实践当前趋势会议，LNCS第3381卷。施普林格，2005年。