没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记139(2005)3-23www.elsevier.com/locate/entcsSPIN-to-GRAPE :一种分析Promela模型Alastair Donaldson,Alice Miller,Mu Zhao Calder苏格兰格拉斯哥大学计算机科学系{ally,alice,muffy}@ dcs.gla.ac.uk摘要我们提供了两个例子,Promela模型的并发,分布式系统,其相关的Kripke结构有更复杂的对称群比文献中常见的模型。我们提出了一个工具,SPIN到GRAPE,它允许使用群论软件包GAP和它的图论插件GRAPE来操纵Promela模型的状态图。通过研究这些例子,我们显示了一个系统的通道图的对称群和与该系统相关联的Kripke结构的对称群之间的对应关系。然后,我们确定了一些一般类的系统,并描述了相关模型的对称群。最后,我们讨论的方式,对称性降低技术纳入SPIN,例如。SymmSpin软件包可以扩展到利用这种模型中的对称性关键词:反应式系统;并发性;形式化建模与验证;对称约简;分布式系统; Promela/SPIN; GAP/GRAPE;nauty1引言模型检测是一种技术,通过建立系统的抽象模型,并通过探索所有可能的执行路径,检查模型是否满足属性,可以检查系统的属性。模型通常具有高度的对称性,这一点可以用来降低搜索成本。SPIN模型检查器[12]是一个显式状态,基于模型检查器,主要用于验证通信协议。SPIN使用的验证模型使用规范语言Promela(过程语言)编写。最近,人们尝试将对称性简化技术纳入SPIN模型检查器[2]。特别是SymmSpin1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2005.09.0074A. Donaldson等人/理论计算机科学电子笔记139(2005)3包已被证明给非常大的因素时,减少应用到模型与许多复制的组件是完全对称的。SymmSpin采用的对称性约简技术基于Ip和Dill的方法,使用标量集[14]的概念-一种具有限制性的特殊数据类型,保留操作。除了SPIN 之 外,标量集也被用于向其他验证系统添加对称性约简,例如UPPAAL [11]和MurPRAAL [6]。标量集是一种理想的手段,利用对称性的模型与许多复制的组件,如果有这些组件之间的完全对称。例如,当验证具有完整拓扑结构的相同过程的网络模型时,标量集可以有效地用于获得对称性约简。Ip和Dill还指出,标量集类型可以修改为适用于其他类型的对称,例如。具有环形拓扑结构的系统中的旋转对称性然而,尽管对称性约化是当前的热门话题,但很少有实例可用于(a)说明基本概念和(b)将结果推广到更现实的系统。在本文中,我们提供了一些具体的例子模型,有更复杂的对称群比那些通常在文献中引用的例子,对称性不能利用目前的标量集方法。我们的模型是分布式系统,表现出并发性和非确定性。我们发现,我们的模型的对称群是同构的通道图与模型的对称群,并描述这些群体的结构的基本置换群。通过这些例子,我们确定了一些更一般的系统类别,并预测了相关模型中存在的对称性。我们描述了一种技术,通过该技术,群论软件包GAP [9]被用于研究Promela模型的自同构群,并提出了一个软件工具SPIN-to-GRAPE,该软件工具允许Promela模型的状态图被加载到GAP中,并使用GRAPE(GAP的图论软件包)进行操作。最后,我们提出了一些扩展的scalarset数据类型,可用于应用对称性约简技术的一个更大的类Promela模型比目前可能与SymmSpin。2预赛在第2.1节中,我们给出了一些数学定义,这些定义将在全文中使用。在2.2节中简要讨论了对称约化在模型检验中的应用,在2.3节中我们给出了GAP包的概述。A. Donaldson等人/理论计算机科学电子笔记139(2005)352.1基本群论与图定义2.1设G是一个非空集,并且设G:G×G→G是一个二元运算。我们说(G,n)是群,如果G在n下是闭的;n是结合的;G有一个单位元1G;对每个元素x∈G都有一个逆元x−1∈G使得x<$x−1=x−1<$x=1G。在G中,我们称这种运算为乘法。当二元运算是什么很清楚时,我们简单地把一个群称为G而不是(G,n)。设H是群G的非空子集。如果H在G的二元运算下是一个独立的群,即它满足定义2.1,那么我们称H为G的子群,记为H≤G。设G是一个群,g1,g2,.,gn∈G. G的元素集通过将任何(以任何顺序并允许重复)元素g1,g2,.,gn,g−1,g−1,.,g−1被表示 由g1,g2,.,gn.1 2N这个集合是G的一个子群,称为由g1,g2,.生成的子群。 ,gn.考虑集合[n] ={1,2,...,n}。[n]的置换是从[n]到[n]的双射。我们使用不相交的循环形式[19]来表示[n]的排列。 [n]的所有置换的集合在映射的合成下形成群。这个群称为n点上的对称群,记为Sn。定义2.2设(G,G)和(H,G)是群,θ:G→H是映射。我们说θ是从G到H的同构,如果它是双射的并且满足以下条件:g,h ∈ G. θ(g <$h)= θ(g)<$θ(h)。在这种情况下,逆映射θ−1也是从H到G的同构,并且假设G和H是同构的,只要G≠H。群的等价性定理[19]中,若群G与H同构,则它们在群论上等价.事实上,它们在代数上是不可区分的。因此同构群通常被认为是相等的,因为它们具有完全相同的结构。如果一个群H同构于一个群G的一个子群,我们就说H是G的一个子群。为了简洁,以及比较不同群的结构性质的能力,我们经常将群G标识为同构于置换群H和K的乘积。 例如直积(记为H×K)、半直积(记为H.K)或圈积(记为H\K)。我们在这里不提供这些产品的定义,详细信息请参见[19]。6A. Donaldson等人/理论计算机科学电子笔记139(2005)3定义2.3设Γ =(V,E)是一个有向无色图,其中V是一个非空顶点集,E∈V×V是一个边集Γ的自同构是从V到V的双射α,它满足以下条件:x,y∈V。(x,y)∈E惠(α(x),α(y))∈ E.如果Γ是一个着色C的着色图(C将V的每个元素映射到从某个非空集合中选取的一种颜色),则Γ的自同构必须满足附加条件:x∈V。C(x)= C(α(x))。对于有向图Γ(着色或未着色),设Aut(Γ)表示Γ的所有自同构的集合.可以证明Aut(Γ)在映射的合成下形成群。我们称Aut(Γ)为Γ的自同构群2.2对称性与模型检验在 本 节 中 , 设 P = p1<$p2<$··<$pn 是 一 个 并 发 程 序 , 其 中 p1 ,p2,... ,pn是n ≥ 1时并行运行的进程,AP是程序P的一组原子命题.与P相关联的通信信道的集合由{Cn+1,Cn+2,. ,Cn+k},其中k ≥ 0.定义2.4与P相关的AP上的Kripke结构M是四元组M=(S,R,L,s0),其中:(i) S是一个非空的有限状态(ii) R<$S×S是一个全转移关系,即对每个s ∈S <$t∈S使得(s,t)∈R(iii) L:S→2AP是一个映射,它用在S中为真的原子命题集合来(iv)s0∈S是一个初始状态。Kripke结构M给出了程序P的形式语义。Kripke结构M的自同构是具有顶点集S和边集R的无色有向图的自同构(参见定义2.3)。Kripke结构M的自同构群记为Aut(M)。Aut(M)的子群G通过规则s<$Gt惠s=α(t)在M的态上导出等价关系<$G,其中α∈G.等价类记为[s]的状态s在G作用下的轨道称为s在G作用下的轨道。轨道可以用于如下构造商Kripke结构MGA. Donaldson等人/理论计算机科学电子笔记139(2005)37定义2.5M关于G的商Kripke结构MG是四元组MG=(SG,RG,LG,[s0]),其中:(i) SG={[s]:s∈S}(S在G作用下的轨道集)(ii)RG={([s],[t]):(s,t)∈R}(iii) LG([s])=L(rep([s]))(其中rep([s])是[s]的唯一表示(iv) [s0]∈SG(初始状态s0∈S的轨道)。一般来说,MG是一个比M小的结构,但MG和M是等价的,因为它们满足相同的一组逻辑性质,这些性质在群G下是不变的(即,关于G“对称”的性质因此,通过选择一个合适的对称群G,模型检查可以在MG上而不是M上执行,通常会节省大量的内存和验证时间。有关商结构和对称性简化模型检查的更多详细信息,请参见示例[5]。原则上可以通过构造原始结构,找到它的自同构群,并确定结构在这个群下的轨道来构造商克里普克结构。然而,寻找图的自同构是一个困难的问题,没有多项式时间算法已知[18]。此外,商Kripke结构不能找到使用这种方法,如果原始结构是棘手的。因此,任何有用的对称约化方法都必须允许我们找到Kripke结构的自同构,而不需要显式地构建结构。众所周知,Kripke结构的自同构通常是由于被建模的并发系统的架构或网络拓扑中的对称性而出现的[4]。我们在本文中表明,在某些情况下,这种对称性可以通过观察系统的通道图[20]来检测。定义2.6对应于并发程序P的通道图是有向着色图C(P)=(V,E,C),其中:V = VP<$VC且VP={1,...,n},VC={n + 1,.,n + k}分别是系统中进程和通道的索引集;对于i,j∈V,(i,j)∈E当且仅当i∈VP,j∈VC且进程pi可以在通道c j上发送消息,或i∈VC,j∈VP且进程pj可以在通道c i上接收消息;映射C将每个进程或通道分别分配给进程类型或通道类型(其中进程类型和通道类型是不相交的)。在图2中,我们给出了一个分布式系统的通道图的例子,其中进程用椭圆表示,通道用矩形表示,类型用文本标签表示。在每个椭圆形或矩形旁边指示索引定义2.6是特定于消息传递计算范式的。在8A. Donaldson等人/理论计算机科学电子笔记139(2005)3[4] ,对共享变量计算范例-对应于并发程序P的着色超图进行了类似的定义。在一定的限制条件下,着色超图的每个自同构对应于与系统相关联的底层Kripke结构的自同构。 超图的一个自同构α被应用到Kripke结构的一个状态,通过根据α对进程索引的置换来置换进程的共享变量和局部变量。类似的结果也适用于消息传递范例。通道图C(P)=(V,E,C)的自同构是C(P)的图自同构(见定义2.3),它被认为是一个有向着色图。Aut(C(P))的元素置换过程索引的集合VP和信道索引的集合VC两者,并且因此可以如下应用于Kripke结构的状态。让我们把定义域为过程标识符的变量集称为I-变量。Kripke结构的标记函数L用对P的局部变量和通道的一组赋值来标记每个状态s。如果vi是进程pi的局部变量,那么,由于α将进程索引i映射到与进程pi具有相同进程类型的进程的索引,因此存在进程pα(i)的对应局部变量vα(i)。状态中局部变量的标记因此,α(s)由以下规则定义:(vi=x)∈L(s)<$(vα(i)=x)∈L(α(s))如果vi不是I-变量和(vi=x)∈L(s)<$(vα(i)=α(x))∈L(α(s))如果vi是I-变量自同构α以类似的方式排列P中通道的内容。在某些限制下,自同构α∈Aut(C(P))对应于自同构αJ∈Aut(M),我们有:引理2.7如果P是满足一组限制R的并发程序,M是与P相关联的Kripke结 构 , C( P ) 是 与 P相 对 应 的 通 道图 , 则 Aut ( C( P ) )≤Aut(M)。限制R的集合与第7节中描述的标量集方法相关联的那些限制类似,因为它们适用于与P相关联的变量的子集,这些变量是I-变量。 在这种情况下,P中涉及I变量x的陈述被限制为xΔy形式的陈述,其中Δ是x(从名称为chan的通道中读取x);或chan!x(将x写入到名称为chan的通道)。虽然很简单,但由于空间的原因,我们在这里不提供引理2.7的证明。然而,我们证明了具体的例子的结果A. Donaldson等人/理论计算机科学电子笔记139(2005)39在第4和第5节。引理2.7使我们能够通过分析系统的通道图(通常是一个小图)来找到一个难以处理的大Kripke结构的自同构。2.3GAP和 GRAPEGAP(Ggroups,Altax ms andP programming)[9],是一个计算群论软件包,它包括一个命令式编程语言,一个用于处理代数结构的类型系统,以及一个用于使用这些结构进行计算的广泛函数库。GAP为群计算提供了丰富的函数集,但它本身对图论计算提供的支持很少GRAPE(使用PE突变组的GRaphA出租[23]由一组可以导入GAP的函数组成。在GRAPE提供的函数中,有一个函数用于计算有向着色图的自同构群。该函数与nauty(noaut morphisms,yes)程序[17]接口,该程序使用目前已知的最有效的算法来查找图的自同构群[18]。关于GAP和GRAPE的详细信息可以在GAP网站上找到[9]。在本文中,我们使用以下两个函数:• AutGroupGraph(Γ[,C])-返回有向图Γ的自同构群。可选参数C允许指定Γ的顶点上的着色,并且只有保持这种着色的自同构才会被返回。• IsomorphismGroups(G,H)-计算群G和H之间的同构,如果它们是同构的(见定义2.2),否则返回失败。3SPIN转GRAPE工具SPIN为在Promela模型上运行验证提供的选项之一是-DVERBOSE编译时指令。此选项将记录验证的每一运行验证以在无死锁模型上搜索无效的结束状态,-DVERBOSE选项,并且没有偏序约简(一种确保从一组等价路径中仅搜索一个代表的算法),从而有效地使得整个对应的Kripke结构被输出。为了使用GAP和GRAPE来操纵与模型相关联的Kripke结构的状态和转换,我们设计了一个工具SPIN到GRAPE,该工具获取相关的详细输出并产生可以输入到GAP的图。10A. Donaldson等人/理论计算机科学电子笔记139(2005)3SPIN到GRAPE工具由基于下面的算法1的PERL程序组成,其重新跟踪SPIN在执行状态空间搜索时所采取的步骤。该算法为模型中的每个进程使用单独的堆栈。每当输入文件中的一行指示进程执行了一条语句时,当前状态号就被添加到该进程的堆栈中。当一行输入指示某个进程已反转时,将从该进程的堆栈中弹出一个值,并将当前状态号设置为该值。这就是算法在处理输入文件时跟踪当前状态编号的方式。每当发现一行输入,指定已经找到新的或旧的状态时,算法将一行GRAPE代码写入输出文件,指定应该向状态图添加转换。从SPIN到GRAPE的输出文件可以加载到GAP中,并且可以调用GRAPE的AutGroupGraph()函数来使用nauty算法找到状态图的自同构群。PERL代码列表可以在我们的网站上找到[3]。算法1SPIN到GRAPE用于构造状态空间的从SPIN输出文件打开输入和输出文件当前状态的模型:= 1求出模型的状态数n输出GAP线以创建具有n个顶点的空图K对于输入文件中的每一行l,如果l表示一个新的状态s,则输出行,用于将从当前状态到s的边沿添加到K当前状态:=s否则,如果l表示旧状态s,则输出行,用于将从当前状态到s的边沿添加到K否则,如果l指示进程p执行,则将当前状态推到进程p的进程堆栈上否则,如果l表示过程p反转,则从进程p的堆栈中弹出状态s当前状态:=s如果结束,则结束关闭输入和输出文件虽然SPIN到GRAPE工具对于处理简单的Promela模型非常有用,但它有局限性。使用-DVERBOSE选项会大大增加完整状态空间搜索所需的时间,因为SPIN会在屏幕上显示所涉及的每一步。最好将该工具纳入A. Donaldson等人/理论计算机科学电子笔记139(2005)311到SPIN中,因此当探索模型的状态空间时,SPIN可以输出包含构建状态图所需的GAP和GRAPE命令的文件,而不是整个冗长的输出。该工具的另一个问题是,由于GAP(版本4.3)中的一个bug,GAP可以接受的输入文件的大小受到限制。输入文件的我们已经报告了这个错误,它将在下一个版本的GAP中得到修复。目前,可以修改和重新编译GAP来解决这个问题,或者将一个大的输入拆分成几个较小的文件。此外该nauty算法只适用于大小≤215− 3的图(尽管理论上这个界限可以通过重新编译来提高)。更重要的是,Nauty算法的复杂性意味着它在大型图上的性能很差,并且它的使用通常不适用于超过15,000个顶点的图为 了 配 合 SPIN 到 GRAPE 工 具 , 我 们 编 写 了 一 个 GAP 函 数QuotientKripke()。该函数将Kripke结构M(作为有向图)的状态和转换与Aut(M)的子群G一起,并返回由商Kripke结构MG的状态和转换组成的有向图。该函数允许我们通过使用小模型的对称性来确定潜在的减少因子QuotientKripke()函数的代码也可以在我们的网站上找到[3]。在下面的部分中,我们描述了两个Promela模型,并展示了SPIN到GRAPE工具如何允许我们分析这些模型的状态图和通道图4三层架构模型分布式系统的一个常见的软件工程设计模式是三层架构。这种架构中的组件分为三层,一层客户端,一层服务器和一层数据存储系统。这种系统的典型消息流程如图1所示(改编自[24])。这种模式在电子商务领域很常见,客户通过Internet购买产品或进行预订。位于不同地理位置的一组服务器我们的第一个模型是一个简单的三层系统,由三种进程类型组成:客户端、服务器和数据库。每个客户端进程由其id和与服务器进程关联的通道名称参数化。服务器进程由两个通道名称参数化。这些渠道中的第一个是使用12A. Donaldson等人/理论计算机科学电子笔记139(2005)3第一个用于接收来自客户端进程的请求,第二个用于向数据库发送查询。客户端进程不断循环,向它所连接的服务器发送请求消息,并等待,直到在其传入通道上接收到结果消息。类似地,每个服务器进程不断重复接收来自客户端的请求,向数据库发送查询并接收数据,然后将结果发送回客户端的操作。数据库进程不断接收来自服务器的查询并返回数据。对于每个服务器进程,都有一个通道数组-每个与该服务器关联的客户端对应一个通道。数据库还使用一组通道,每个通道对应一台服务器。模型中的所有通道都是同步的。图2显示了一个系统的通道图,该系统包含一个数据库、三个服务器和八个客户端。每个通道都用它接受的消息类型进行注释。消息类型由一个或多个用花括号括起来的字段类型组成。这里使用的字段类型是byte和mtype,mtype是用于表示控制指令的枚举类型。通道的类型还取决于通道的长度,即它可以容纳的消息数量。由于模型中的所有通道都是同步的(因此长度为0),因此图中没有显示长度。这种三层模型的配置代码可在我们的网站上找到[3]三层模型中的对称性分析为了分析三层架构模型中的对称性,我们使用图2所示的配置作为案例研究。设P表示具有这种配置的系统,具有通道图C(P)和相关的Kripke结构M。这种配置是合适的,因为它有多个服务器和多个客户端,并且进程树不是完全平衡的,我们希望在Kripke结构中存在的对称性中反映出这一特征。由此产生的配置状态空间足够小,可以使用我们的自动设置进行全面的对称性分析。用户界面(演示)应用服务器数据库服务器等待结果时间Fig. 1.三层体系结构系统请求操作返回结果等待数据请求数据返回数据A. Donaldson等人/理论计算机科学电子笔记139(2005)31312图二.具有一个数据库(Db)、三个服务器(Se)和八个客户端(Cl)的三层架构模型的通道图。将图2的通道图输入到GAP(根据过程类型指定着色),并调用GRAPE函数AutGroupGraph()来查找通道图自同构组,这表明:Aut(C(P))=(5 6)(20 21),(6 7)(21 22),(8 9)(23 24),(9 10)(24 25),(5 8)(6 9)(7 10)(20 23)(21 24)(22 25)(2 3)(1718)(14 15),(11 12)(26 27)从图2中我们可以看到,这个组的第一个生成器,置换(5 6)(20 21)是通道图的自同构,因为很明显,交换客户端5和6,同时交换通道20和21,使通道图的结构保持不变。 由于客户5和6具有相同的过程类型,并且通道20和21具有相同的通道类型,则该置换保留了通道图的着色。其他生成器在通道图上的作用类似。Aut(C(P))的元素作用于Kripke结构M的状态,如我们在第2.2节中的引理2.7之前的讨论中所描述的。由于模型中的通道是同步的,因此在这种情况下不需要交换通道内容。三层模型关注的是控制流而不是数据流,因此我们可以预期克里普克结构M的所有对称性都是结构诱导的。我们证明了Kripke结构和通道图的自同构群是同构的,并证明了它们是依次同构的对称群的乘积:引理4.1对于上述三层模型的构造,Aut(M)=Aut(C(P))=(S3\S2)×S2我们已经使用了我们的SPIN组合,SPIN到GRAPE,GAP和GRAPEDB113141516Se2Se3Se417{mtype,byte}{mtype,byte}1819联系我们20联系我们21联系我们22联系我们23联系我们24联系我们25联系我们26联系我们27CL5CL6CL7CL8CL9CL10CL11CL{mtype,byte}联系我们联系我们联系我们{mtype,byte}14A. Donaldson等人/理论计算机科学电子笔记139(2005)3来证明这个引理。使用SPIN到GRAPE工具将Kripke结构M的状态图输入到GAP。然后使用AutGroupGraph()函数找到这个状态图的自同构群。利用GAP构造了一个群G=(S3\S2)×S2(GAP提供了计算两个群的直积和圈积的函数 利用同构Groups()函数证明了Aut(C(P))<$=Aut(M),又证明了Aut(M)<$=G.最初的克里普克结构有4,393个州。我们使用Quo- tientKripke()函数计算了关于群Aut(M)的商结构,发现它有281个状态。这是一个重要的减少因素,对于实际尺寸的模型,可以证明在对抗状态空间爆炸问题方面非常推广:直观地说,群Aut(C(P))同构于群(S3\S2)×S2,因为有两个三个客户进程的块(产生子群 S3\S2),和一个两个客户进程的块(产生子群S2)。考虑三层模型的任意配置P。 设M是与P相关联的Kripke结构,并且设K是配置中的任何服务器连接到的最大客户端数量设mi表示对于每个i,连接到i个客户端的服务器的数量,1≤i≤K。上述讨论和结果清楚地概括为:Aut(M)=Aut(C(P))=1≤i≤Kmi/=0(Si\Smi),哪里表示对i的直积。在[15]中,Jha展示了自动驾驶汽车是如何运行的可以找到任意根树的态射群。他的方法可以用于将上述论点推广到具有三层以上的系统。5超立方体中的消息路由模型在基于交换机的多计算机的实现中使用的流行拓扑是超立方体[24]。以下定义改编自[25]:定义5.1n维超立方体是一个图G=(V,E),其中V ={(b1,.,bn):bi= 0,1}和E={((b1,. ,bn),(c1,. ,cn)):b和c在一位中的差异}A. Donaldson等人/理论计算机科学电子笔记139(2005)315(0,(0,(0,(0,1,1,1)(1,(0,(0,(1,(1,(1,0,(1,0,1,0)(1,0,1,1)算法2超立方体网络中消息路由的基本算法whiletruedo接收发往节点x的如果id=x,则选择一个新的目的地xend if确定比当前节点更接近节点x的邻居将消息转发到其中一个邻居end while4维超立方体可以用两个立方体在3维中表示,如图3所示。在使用超立方体拓扑的基于交换机的多计算机中,消息在处理器之间路由。作为我们的第二个例子,我们使用算法2(下面)对超立方体网络中的消息路由进行建模,这是[8]中描述的算法的简化版本。我们的模型定义了一个参数化的节点过程。为了确保模型的状态空间足够小以便于分析,我们一次只考虑一条消息通过网络。全局变量记录消息的目的地和当前位置。通信是通过一个通道数组实现的,超立方体中的每个节点都有一个通道,init进程(设置数组、通道等初始值的进程)将第一条消息发送到非确定性选择的节点。为了决定哪些邻居适合转发给定的消息,节点进程首先计算其自身位置和消息目的地的逐位异或。然后考虑该结果的每一位。 如果在结果的位置m中存在1,则当前节点的仅在位置m中坐标不同的邻居比当前节点。节点进程非确定性地选择一个这样的合适的邻居。同样,该模型的Promela代码可在我们的网站上找到[3]。(0,1,0,0)(0,1,0,1)图三. 四维超立方体16A. Donaldson等人/理论计算机科学电子笔记139(2005)3超立方体模型n维超立方体的自同构群是很好理解的,并在[10]中得到超立方体的节点可以由形式为(x1,x2,. ,xn)。 对于Sn中的任意置换α,定义α对(x1,.,xn)乘以α((xi,.,xn))=(xα(1),.,xα(n))。 对于每个i,定义第i个互补置换ciby ci((x1,.,xi.,xn))=(xi,...,<$xi,.,xn)。设Kn= Kc1,.,Cn,由c i的所有组合生成的群。n维超立方体的自同构群是Sn和Kn的半直积,记为Sn.Kn。在分析超立方体模型中对称性的本质时,我们希望使用至少四维的构型作为案例研究。然而,即使是4维配置的状态空间也被证明太大,无法使用我们的setup-1进行分析。6× 107个状态--所以我们把自己限制在三维构型(立方体)。这个问题证明了状态空间的快速爆炸,因此需要对称性约简等技术。设P表示超立方体消息路由系统的三维结构,具有通道图C(P)和相应的Kripke结构M.系统的拓扑是立方体,所以我们有Aut(C(P))=S3.K3.由于P中的节点进程都是相同的,我们期望立方体拓扑的任何自同构都对应于底层Kripke结构同样,所有的对称性都可能是由结构引起的。引理5.2对于上面描述的超立方体模型的三维构造,Aut(M)= Aut(C(P))=S3. K3我们已经证明了这个引理使用SPIN到GRAPE,GAP和GRAPE,因为我们做了引理4.1。最初的Kripke结构有15,409个州。使用我们的QuotientKripke()函数作为三层模型,我们发现所得的商结构有411个状态。所取得的减少因素也是令人鼓舞的。引理5.2是有趣的,因为我们的超立方体中的消息路由模型不满足我们在引理2.7之后讨论的限制:进程id被用作逐位异或操作中的操作数,以确定分组应该如何路由。这表明与引理2.7相关的限制是足够的,但不是引理成立所必需的。尝试识别进程id可以用作算术表达式的操作数而不破坏对称性的一般情况将是有趣的。A. Donaldson等人/理论计算机科学电子笔记139(2005)317推广:设P是n维超立方体模型的一个构形,其中n≥1。设M是与P相关联的Kripke结构,并且设C(P)是对应于P的信道图。根据前面的讨论,上述结果似乎可以概括为:A ut(M)= A ut(C(P))= Sn.Kn我们会直观地期望这一推广的结果,以保持任何模型的分布式算法的n维超立方体的相同的进程。6将SPIN-to-GRAPE应用于不太对称的模型到目前为止,在我们的分析中,我们使用了SPIN-to-GRAPE,以及GAP和GRAPE,来证明对于某些模型配置,与模型相关的Kripke结构的自同构群与对应于模型的通道图的自同构群同构。在本节中,我们对每个模型进行轻微的修改,使它们不那么对称,并使用SPIN到GRAPE来检测这些修改引起的对称性变化。6.1三层模式在图2所示的三层体系结构模型中,所有通信都使用同步通道进行建模,因此消息通过发送方和接收方之间的握手传递,而没有缓冲。我们修改了我们的模型,使其中一个通道成为一个位置缓冲器(即长度为1的异步通道)-进程ID为5,6和7的客户端使用该通道向进程ID为2的服务器发送请求。 模型的其余部分保持不变。对于原始模型的Kripk结构M,具有Aut(M)=(S3\S2)×S2。设MJ为修改后模型的Kripke结构。用SPIN-to-GRAPE分析表明,Aut(MJ)=S3×S3×S2,它比(S3\S2)×S2小.显然,这是因为更改的通信信道意味着不再可能使用进程来置换服务器ID 2和3。这表明,影响模型结构对称性的不仅是进程的行为和进程之间的连接我们通过观察系统的通道图来发现对称性的方法很好地处理了这种不对称性,因为改变通道的长度会改变该通道的类型。这反映在对称的18A. Donaldson等人/理论计算机科学电子笔记139(2005)3通道图,并且因此也检测到Kripke结构的对称性的相应变化。Kripke结构MJ有14,995个状态,使用QuotientKripke()函数,我们发现所得的商结构有1115个状态。折减系数小于模型修改前的折减系数。这显然是由于模型对称性的改变。6.2具有固定发起者在第5节描述的超立方体模型中,数据包首先由init进程在系统中的一个通道上非确定性地发送。模型中的这种非确定性通常会导致状态的爆炸,当试图编写一个有效的验证模型时,一个常见的方法是删除这种非确定性。我们改变模型,使数据包总是首先在与id为0的节点相关联的信道上发送。使用SPIN的状态空间搜索显示,改变后的模型有8,866个状态,而原始模型有15,409个状态SPIN-to-GRAPE 证明了改变模型的自同构群同构于立方体的自同构群的一个子群设G=S3,K3是立方体的自同构群,MJ是立方体的为一个线性模型建立一个结构。nwehaveAut(MJ)n=stabG(0)={α∈G:α(0)= 0},G中固定节点0的子群(G中节点0的稳定子)。这表明,对于由连接为给定拓扑的相同过程组成的模型,底层Kripke结构的对称性如果init进程不相对于所有进程对称地工作,则对应于拓扑对称的对称性将不一定同样,我们的方法会检测到对称性的这种变化:在原始模型中,从init进程到系统中的每个在修改后的模型中,从init进程到与节点0关联的通道只有一条边。这将导致通道图中对称性的变化,并且将检测到潜在的克里普克结构的对称性有趣的是,QuotientKripke()函数显示,对应于修改后的模型的商结构的大小为1,669。对应于没有改变的模型的商结构具有大小411。在这种情况下,尽管从模型中去除非确定性导致Kripke结构的尺寸减小,但对称性的相应减小意味着改变的模型的商结构实际上大于没有改变的模型的商结构。A. Donaldson等人/理论计算机科学电子笔记139(2005)3197SPIN中对称约化的扩展在[14]中,Ip和Dill提出了一种特殊的标量集数据类型,可以将其添加到系统描述语言中,以便于检测和利用系统的对称性。标量集是具有限制操作的整数子范围,其确保在Kripke结构的所有状态中标量集值的一致置换导致Kripke结构的自同构。这些限制防止标量集值通过排序关系相互比较,或用作算术表达式中的操作数。系统中等价过程的id可以用标量集建模,这表明在整个Kripke结构中应用id的置换将导致结构的有效自同构虽然在许多情况下它被证明是有效的[2,6,11],但一般来说,使用标量集的对称性约简是有限的,因为它只允许指定和利用总对称性。 它肯定不能应用于 我们的例子。我们对三层模型的分析表明,Kripke结构的自同构可能并不总是对应于一种进程类型的id的排列:在具有树状结构的模型中,它们可能是由于组合了许多进程类型的id的排列。同样,我们对超立方体模型的分析表明,在相同过程的网络中,对称性的存在取决于网络拓扑。标量集的应用目前仅限于非常简单的拓扑,如星和团。我们提出了两种方法,可以将标量集数据类型扩展到我们所描述的各种模型。我们扩展了[14]中使用的符号,其中标量集是这样声明的类型名称 :Scalarset[size]7.1相伴标量集一个相关的标量集将允许在模型规范中描述树结构的对称性。一个相关联的标量集通常被声明为具有指定的大小N。声明还要求指定N个标量集类型该列表将相关标量集的N个元素中的每一个与另一个标量集相如果与i和j相关联的标量集类型相同(并且被置换),则置换相关联的标量集类型的进程idi和j是安全的。举例来说typeserver id:AssocScalarset(3, [Scalarset(3),Scalarset(3),Scalarset(2)]);指定一个大小为3的相关标量集类型,其中元素1和2与20A. Donaldson等人/理论计算机科学电子笔记139(2005)3一个这个相关的标量集类型可以应用于图2所示的三层系统的配置,假设客户端进程使用适当的标量集id声明。关联的思想可以递归地应用于更深入地描述树结构7.2基于拓扑的标量集当指定相同进程的网络时,如果网络拓扑已知,则可以利用进程之间的对称性。一个基于拓扑的标量集被定义为一个给定的大小,一个指定的拓扑也必须以某种标准化的方式描述。举例来说:typenode id:TopologyScalarset(8,cube)其中cube:=1→ { 2, 3, 5}, 2→ { 1, 4, 6}, 3→ { 1, 4, 7}, 4→ { 2,3, 8},5→ { 1, 6, 7}, 6→ { 2, 5, 8}, 7→ { 3, 5, 8}, 8→ { 4,6, 7};为立方体网络中的节点指定了基于拓扑的标量集类型,例如我们在第5节中考虑的节点。立方体拓扑的定义指出,对于每个节点,该节点连接到其他节点。指定拓扑的任何自同构都可以安全地应用于基于拓扑的标量集,并且GRAPE可以用来找到所有这样的自同构的群。通过扩展SymmSpin包以支持这些新类型,可以增强使用SPIN的对称性约简模型检查的应用为了做到这一点,有必要在这些类型的元素上定义保持对称性的操作这也将是必要的,设计算法,使有效地利用新的标量集类型的对称性在模型检查。在这些扩展的开发过程中,SPIN-to-GRAPE工具和这里介绍的自动设置将被证明是有用的,可以测试特定模型上对称性约简的有效性。8相关工作SymmSpin软件包[2]已被证明,当应用于具有许多完全对称的复制组件的模型时,可以提供非常大的缩减因子。SymmSpin使用由Ip和Dill在[14]中引入的标量集类型;标量集最近也被用于将对称约简技术添加到实时模型检查工具UPPAAL[11]中。A. Donaldson等人/理论计算机科学电子笔记139(2005)321Emerson等人研究了对称性简化在部分对称系统中的作用,包括涉及在其他相同过程之间变化的优先级的系统[7]。SMC工具[22]是一种基于对称性的模型检查器,可以验证安全性和活性属性,旨在处理公平性约束,这无法通过标准对称性约简技术来处理。Sistla和Gyuris [21]关于部分对称性的结果也已在SMC工具中实现在[16]中,考虑了GAP在识别数字电路对称性问题中的应用。没有其他关于对称性和模型检验的论文试图利用GAP,或者任何计算代数包。Aloul等人。[1]使用GAP,特别是Nauty算法[17],实现有效的对称破缺技术以实现布尔可满足性。在[15]中,讨论了各种常见体系结构的对称性,包括超立方体和有根树然而,没有提供使用这些架构的模型的具体例子,也没有研究自动找到这些自同构的问题。9结论和进一步的工作我们给出了一个结果,表明与并发系统P相关联的Kripke结构的自同构可以通过找到相关联的通道图C(P)的自同构来确定. 此外,我们已经提出了一个软件工具,SPIN到GRAPE,它允许我们分析的对称性,目前在简单的Promela模型的并发,分布式系统使用群论包GAP和它的图论插件,GRAPE。我们已经描述了两
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功