基于图的分布式系统组合规格说明方法

网址：http://www.elsevier.nl/locate/entcs/volume51.html10页一种基于图的分布式系统组合规格说明方法曼努埃尔·科赫1PSI AG德克森海峡第四十二至四十四条10178 Berlin，Germany摘要分布式图变换是分布式系统的组合形式化规范技术。分布式图变换是一种直观的、图形化的、基于规则的分布式系统拓扑、局部数据和动态建模方法该方法是组合的意义上说，本地组件指定本地和组成的同步约束。分布式系统的操作语义由其组件的操作语义组成1引言分布式图变换[Tae96，TFKV99，Koc99]是一种基于图的分布式系统规范化技术。分布式图用于指定分布式系统状态的拓扑结构和局部状态。分布式产生式指定了对分布式图的操作，包括拓扑以及局部状态转换。而[Tae96，TFKV99] 通过一组全局分布式产生式来指定分布式系统，[Koc99]中的规范由局部规范组成，每个局部规范由一组进程产生式组成。在分布式系统中，过程产生式服从可见性，在这个意义上，只有一个局部组件（称为过程）的局部视图是应用产生式所必需的，而不需要全局信息。一个局部组件的行为。某种类型的过程是特殊的，由包含每个动作的过程产生的过程语法来定义，过程可以执行。分布式系统的可能进程类型在网络类型图中指定，并且分布式语法具有用于出现在网络类型图中的每个进程类型1电子邮件地址：mkoch@psi.dec2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2过程端它的目的是与同步的分布式系统的行为建模过程产生式的同步约束由一个同步关系给出。这种关系限制了进程的行为，因为一个进程的移动需要其他进程的同时移动分布式系统规范结合了所有规范部分：工作类型图、分布式文法和同步关系。2分布式图转换分布式系统的拓扑结构由图1所示的分布式系统的图DS中类型化的图指定。 类型图DS表示Fig. 1.分布式系统的类型图DS由通过共享端口通信的并发进程组成的分布式系统的视图类型图DS提供两种类型的节点，即进程和端口。边缘从端口指向进程，因此进程之间的连接只能通过端口。 此分布式系统视图遵循[MPR99]中的分布式系统视图。如果存在分布式系统的另一视图，则类型图DS可以被改变。为了区分不同类型的进程和端口，分别， 网 络 类 型 图（NTG）的介绍。网络类型图是在DS中键入的，用于标识进程和端口类型。在网络类型图上类型化的图被称为关于网络类型图的网络图。通过传递性，网络图也在DS中类型化。图2显示了一个例子。定义2.1 [网络类型图，网络图]网络类型图由类型图t NTG：NT G给出！ DS. t NT G的进程类型集合由PT type（NT G）= f x 2 NT GVj t NTG（x）=进程g定义。网络图w.r.t. t NTG是类型图t G：G！NT G在NT G中。在本文的其余部分，我们给出了一个网络型图tNTG，并将tNTG简称为NT G。每个进程和端口都有一个内部状态。分布式图通过为网络图中的每个进程和每个端口分配其局部状态以及为每个边分配端口的局部状态与进程的局部状态之间的关系，将进程和端口的局部状态集成到拓扑结构中。 例如，该关系可以指定哪些元素 一个端口的哪些元素由一个进程导出，或者哪些元素由多个进程共享。局部状态由一个范畴和关系3由范畴态射定义。用于局部状态的指定的示例类别可以是图、属性图、部分代数等。定义2.2[分布图]G上的分布图是一对G^=ht G; Gi，其中t G：G！ NTG是一个网络图，G：G！ GC是从G到范畴C的底层图GC的全图态射。两个分布图之间的态射由两个网络图之间的部分图态射和一族C-态射组成，一族C-态射包含网络图之间的部分态射域中的每个节点的C部分图态射与网络图有关，C-态射族与局部状态有关.定义2.3[分布态射]G iventwo分布图G^=h t G;Gi和Hi=h t H;Hi分别超过G。 H，一个分布态射f^：G^！H^是由一个保持类型的部分图态射f：G * H给出的（即对所有x2dom（f），t G（x）=t H<$f（x））和一族C-态射f=ff（i）：G（i）！H（f（i））j i 2 dom（f）Vg，使得对所有边e：i！j在dom（f）E中，H（f（e））<$f（i）= f（j）<$G（e）.如果图态射f是全的，则分布态射f^是全的给定一个范畴C，所有分布图和分布态射形成一个范畴DGrC[Koc99]。3过程语法与分布式语法分布式图的操作是通过过程生产来实现的。一个过程产生式由一个产生式名和一个分布态射给出.生产态射的左手边包含一个分布式图，其中它的网络图有一个且只有一个过程节点，可能还有端口。该单个过程节点的类型决定了过程生产的类型。流程生产不能创建新的流程节点，但可以删除单个流程节点以指定流程终止。定义3.1[过程生产]过程生产p：（L）！R^R^），typex由一个预减名p和一个预减态射r^组成，因此，网络图L包含一个且仅一个过程节点，即，有且仅有一个v2LVtNTG（tL（v））=过程，过程节点v是类型 x，即 tL（ v）= x，并且r不创建新的过程节点，即，如果存在v 002 R V，其中tNTG（tR（v0 0））=p r过程，则v00=r（v）。一种工艺生产的应用：（L^！r^R^）到一个分布图如果存在全分布态射m^，则G^是p可能的：L^ ！ G^. 的应用是通过推出的生产态射和4范畴DGrC中的分布态射 分布式图形。的在[Koc 99]中给出了推出的存在性证明和构造将流程生产的左侧限制为一个流程节点是由分布式系统中流程的局部视图激发的。进程可以看到自己的本地状态，端口的本地状态，但不能看到远程进程的本地状态。产生式的左手边是其应用的先决条件，表示必须在分布式图。 要应用左手边包含多个进程的产生式，需要分布式系统的全局视图，因为必须为左手边的每个进程在分布式图中找到一个进程。由于分布式系统中不存在这样的全局视图，因此过程产生式受到限制。例3.2[流程产生式]为了简单起见，本例中流程和端口的局部状态都是用集合来建模的。运行示例的网络类型图有两个进程类型A和B以及一个端口类型（见图10）。2 ）的情况。ABA1 B1网络型图NTGB2B4B3A2图二、网络类型图（左）和可能的网络图（右）。分布式图htG; Gi由网络图G表示，其中过程和端口节点x2GV的局部状态G（x）直接集成到网络节点中。类似地，边的局部态射被直接积分。例如，图3中流程生产p的左侧表示分布式图，其中网络图由一个A型流程节点组成，局部状态由单例集指定图3显示了过程类型A的过程生产p; p0和过程类型B的一个过程生产q。过程productionp创建了一个新的port，它在本地状态中消耗了它的一个元素。进程生产p0将一个元素从进程A的局部状态复制到端口。进程B的进程生产q在进程B的本地状态和连接端口中创建一个元素一个x型过程产生式指定了一个x型过程的一个可能动作。为了指定流程的完整行为，流程语法中提供了其每个操作的流程产生式。的过程语法5工艺生产p一工艺生产qB B工艺生产pAA图3.第三章。 为A和B加工产品。类型x包含一组类型x的过程产生式和类型x的开始产生式。启动生产创建一个新的流程实例。startproduction的左侧包含启动流程所需的端口，右侧包含连接的x类型的新流程实例（可能是新创建的）端口。创建的进程的本地状态表示x类型进程的初始状态。请注意，开始生产不是流程生产，因为在其左侧没有流程节点。定义3.3[开始生产，过程语法] A开始生产st（ x）：（L^！r^R^）包含一个分布态射r^，其中L^R^包含仅端口节点和R1包含类型pex的另外一个处理节点以及可能的一些新端口。typex的一个概率g rr r ammar由一对GG（ x）=hst（ x）;（p：r^）p2Pxi组成，其中Px是一组产品名称，（p：r^）p2Px 是一个Px索引的类型x的过程产生式和st（x）是类型x的开始产生式。例3.4[start production and process grammar]进程A的start production创建了一个进程A，该进程最初在其本地状态中包含两个元素。B类型进程的初始局部状态是空的。进程B直接连接到一个端口。进程类型A的进程文法由GG（A）=（st（A）;fp; p0 g）给出，类型B的进程文法由GG（B）=（st（B）;fq g）给出。这里，p、p 0和q是实施例3.2的工艺产物 。开始生产st（A）一开始生产st（B）B图四、 开始生产A和B。关于网络类型图NT G的分布式文法具有进程文法和NT G中的每个进程类型的一组索引。流程类型的索引集表示此流程类型的流程实例的实例空间已经指定流程实例的必要性一6在分布式语法中，进程的同步是有动机的：这种同步是基于进程实例的级别，而不是进程规范的级别。这允许相同流程类型的流程实例有不同的同步约束。原则上，任何集合，也是可数的集合，都可以被选择作为索引集合，这样就不存在对过程实例数量的限制。定义3.5[分布式文法]给定网络类型图NT G，关于 NT G的分布式文法GG=（GG（ x）; Ind（ x））x2 PType由过程文法GG（ x）和每个x2的索引集 Ind（ x）组成。PT型（NT G）。例3.6 [分布式文法]图2中网络类型图的分布式文法GG =（GG（A）;Ind（A）; GG（B）; Ind（B））包含例3.4中给出的过程文法GG（A）和GG（B）。类型A的进程实例的索引集由Ind（A）= f A 1g给出，而进程B的索引集由Ind（B）= f B 1g给出。也就是说，分布式系统可以由两个过程实例组成：一个是类型A，一个是类型B。为了简单起见，选择单例索引集以更清晰地表示以下概念4分布式系统规范进程之间的同步通信通过公共端口进行对于流程生产的同步应用，同步移动中涉及的每个流程生产必须在相应的公共端口上执行相同的操作。这种要求的特点是存在一个共同的港口生产。流程生产或起始生产的端口生产是通过从其左侧和右侧删除流程而获得的子生产，而所有端口都被保留。如果生产具有相同的端口生产，我们称之为可同步的定义4.1[portgraph，portproduction]设= G; G是一个非-G上的一个分配图，它的端口图是G上的最大子图Port（G）=htPort（G）;Port（G）i over Port（G），其中网络图Port（G）是G中只包含端口节点的最大子图，即. 对于每个节点x在P ort（G）中，V保持t NTG（t Port（G）（x））= port和P ort（G）= GjPort（G）是G对P ort（G）的限制.一个过程生产p的生产：（L^）！R^R1）由Y给出^r^jP orrt（L^）^port（p）：（port（L） ！ Port（R））。示例4.2 [港口生产]图5显示了示例3.2的过程生产和示例3.4的起始生产的港口生产。生产p和st（B）以及生产p0和q具有相同的端口生产，即它们是可同步的。进程生产是可同步的，如果它们具有相同的端口亲，7XXXPGGPGG，其中PGG=fpA1;p0A1;st（A）A1;qB1;st（B）B1gS端口（st（A））端口（p）端口（p '）端口（st（B））端口（q）图五. GG（A）和GG（B）的港口生产duction.然而，并不是所有的流程生产都必须同步。为了指示必须同步的过程产生，同步关系被引入。分布式文法GG的同步关系是关于产品名称pi的关系，其中p是GG的过程文法GG（x）中的过程产品的产品名称，i是索引集Ind（x）的索引。同步关系只涉及具有相同港口生产的生产，也就是说，它们是可同步的。同步生产必须同时应用。同步化行为可以通过将同步化的流程生产通过在公共端口生产上将它们粘合在一起而建立的全局生产来模拟（参见示例4.4）。定义 4.3 [同步关系] 给定一个分布式文法GG = （ GG （ x） ;Ind（ x ） ） x2PT ype ， 其中 GG （ x ） =hst （ x ） ;（ p ： r^） p2Pxifor ea chx2PType。设Pi= fsti（ x）g[（ pi）p2 P是进程的进程生产名称的集合实例i2 Ind（ x）对于每个 x2 PT类型且PGG=Sx2 PType;i2 Ind（ x）我是分布式语法中所有流程实例的生产名称集然后，同步关系SP GGP GG是P GG上的关系，使得p iSp j意味着port（p i）= port（p j）。例4.4[同步关系]同步关系S例3.6中的语法可以如下：st（B）B1和p0A1qB1.由于每个进程类型只有一个实例，因此我们在下面跳过实例名称的索引生产p和st（B）的同步约束的预期含义是，如果A1创建端口，则流程实例A1创建流程实例B1在图6中，通过将p和st（B）合并到公共端口生产上构建的全局生产，可以看到这一效果。全局产生式p+st（B）表明A1创建端口会导致创建流程实例B1。生产p和q的同步约束的预期含义是，流程实例A1的元素应该是8A1通过端口同步复制到流程实例B1。全球生产使这一意图再次可见。生产 p + st（B）A1 B1生产 pA1B1 A1B1见图6。 由同步关系总之，分布式系统由描述可能的进程和端口类型的网络类型图、网络类型图中给出的每个进程类型的进程语法、每个进程类型的实例的索引集以及用于指示对进程实例的移动的同步约束的同步关系来指定。定义4.5[分布式系统规范]分布式系统规范阳离子DSP =（NT G; GG;（D）由(i) -如定义2.1中所定义的网络类型图NT G，(ii) 如定义3.3中所定义的关于NT G的分布式语法GG =（GG（x）; Ind（ x））x2 PType，以及(iii) 如定义4.3中所定义的同步关系。5分布式操作语义本节简要概述分布式系统规范的组合操作分布式系统规范的操作语义由其过程实例的操作过程语义组成。成分受同步关系控制。操作过程语义及其组成的基础是转换系统。Gro e-Rhode在[GR 98，GR 99]中引入了转换系统作为一个通用的语义框架，在这个框架中可以解释用不同语言编写的规范转换系统是两层结构，由对动作的时间顺序进行建模的控制流图给出，以及由分别与控制流图的状态和转换相关联的数据状态和数据转换给出的数据级别通过这种分离，控制流图定义了原子数据转换如何组合到流程中。 控制流图中的路径模拟了动作的顺序执行，分支表示非确定性选择。在[Koc99]中，9分布式图转换也可以在这个框架中解释。用于过程实例的操作过程语义的转换系统考虑了可以通过应用过程实例的过程产生式和通过分布式语法的任意过程产生式的端口产生式生成的所有分布式图。流程实例的开始生产应用一次以启动流程实例。用于过程实例的操作过程语义的转换系统指定了过程实例在完整环境中的行为，因为远程过程的端口上的可能影响也被合并在本地语义中。由于这些端口效果不能由流程实例本身实现，因此这种语义被称为开放流程语义。分布式语义是由转换系统范畴中的一个上极限在一个辅助转换系统上对过程的转换系统进行组合而构造的[GR99]。辅助转换系统由分布式系统规范中所有进程产生式的端口产生式生成。辅助变换系统代表分布式系统规范所规定的分布式系统中可能的端口上的完整行为。辅助转换系统可以嵌入到进程的开放进程语义的每个转换系统中，从而定义了共极限所需的转换系统态射。6结论介绍了一种基于分布式图变换的分布式系统组合规约技术。它是用来指定一个分布式系统的静态和动态方面的分布图和过程产生式，分别。该技术是组合的，在这个意义上，本地组件指定本地的进程语法和它们的连接是由一个同步关系。操作分布语义由分布系统中过程实例的开放过程语义组成在[Koc99]中，分布式图变换和命题时态逻辑被集成到图解释的时态公式中。图形解释公式提供了一种以图形方式指定时态属性的方法。分布式图变换与时态逻辑的结合，可以利用时态逻辑中的各种验证概念来检验图解释的时态公式。组合方法允许组合推理，在这个意义上，局部满足的局部公式在分布式系统的子系统中，可以用来证明全局公式在完整的分布式系统中的10引用[EKMR99] H. Ehrig，H.- J. Kreowski，U. Montanari和G. 罗森伯格，编辑。图文法与图变换计算手册。卷第三章：并发、并行和分发。World Scienti c，1999.[GR98] I'm sorry.代数变换系统及其组成。在大肠Astesiano ，编辑，Proc.Fundamental Approaches to Software Engineering（FASE'98），LNCS中的第1382号，第107页。122. Springer，1998年4月[GR99] I'm sorry. 基于代数变换系统的CCS和UNITY中交替位协议规范的合成比较。第一届综合形式方法国际研讨会（IFM'99），约克，英国，1999年6月。出现在Springer LNCS上。[Koc99] Manuel Koch.图变换与时态逻辑的集成用于分布式系统的规范化。博士论文，柏林工业大学，1999年。[MPR99] U.蒙塔纳里湾Pistore和F. 罗西 [EKMR99]，通过图变换建模并发，移动和协调系统一章。 World Scienti c，1999.[96] I'm sorry.并行和分布式图变换：形式化描述及其在基于通信系统中的应用。博士论文，柏林工业大学，1996年。沙克尔出版社[TFKV99] G.坦策岛菲舍尔，M。Koch和V. Volle。分布式图形转换及其在分 布 式 系 统 可 视 化 设 计 中 的 应 用 In G.Rozenberg ， 编 辑 ，HandbookofGraphGrammarsandComputingbyGraphtransformation，第3卷：并发和分布。World Scienti c，1999.