没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子札记239(2009)85-103www.elsevier.com/locate/entcs具有秩函数的计数器系统的自动验证艾曼纽·恩克雷纳兹·阿兰·芬克尔LSV,ENS-Cachan CNRSCachan,法国{encrenaz,finkel}@ lsv.ens-cachan.fr摘要计数器系统的最终终止验证是不可判定的。对于不可验证的计数器系统,这种类型的属性的验证通常基于排名函数的展示。 证明一般计数器系统的排序函数的存在也是不可判定的。我们提供了一个框架,在该框架中,验证给定函数是否是排名函数是可判定的。这个框架是适用于凸计数器系统,承认Presburger或LPDS排名功能。 这推广了[6]的结果。从这个框架中,我们得到了一个模型检查算法来验证是否满足最终终止属性。 这种方法已成功地应用于ZCSP协议的参数版本。关键词:最终终止性,秩函数,凸计数器系统,自动验证,参数协议ZCSP。1介绍在使用FAST [2]验证参数协议(ZCSP)时,我们遇到了一个有趣的问题。我们必须验证一个最终终止性质,表示系统将以不可避免的方式在给定的状态集合中结束不幸的是,对协议进行建模的计数器系统的类别不符合FAST可以自动解决它的假设:我们的ZSCP模型既不是可验证的,也不是可跟踪的。事实上,最终终止属性在一般情况下是不可判定的,人们必须考虑一些强假设来自动验证它。这个终结问题是经典的解决展示排名功能,它一直在积极研究,在过去的三年中,在代码分析的背景下,命令式程序包含循环与整数变量。在这种情况下,[15]提出了一个完整的方法,用于在限制类的单路循环上合成线性秩函数这一结果最近在[7]中扩展到(单路径)嵌套循环,并在专用于分析的工具EQUATOR [8]中实现1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2009.05.03286E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)85硬件设备驱动程序的C代码分析。在[14]中提出了一种补充方法本文提出了一种基于区域图的半算法,它适用于互斥多路循环,并在专门用于Java程序验证的PONES工具中实现。[6]为更大类的系统合成线性排序函数:具有非排他性保护的多路径整数变量循环。该合成基于所有线性函数的枚举(表示为Presburger公式)。该方法是完整的(如果存在这样的线性函数,程序最终将显示它),然而,这项工作没有考虑参数。我们的贡献。我们重新审视排名功能合成问题的背景下(可能是非确定性的)计数器系统。我们区分排序函数的存在性问题和验证给定类中的函数是否是排序函数的问题。我们首先回顾一下,递归排序函数的存在性是不可判定的,但当考虑迹可判定的计数器系统时,它就变得可判定了。类似地,验证递归函数是否是排名函数是不可判定的,尽管验证Presburger可定义的排名函数是可判定的。不幸的是,ZCSP不允许任何Presburger可定义的排名函数,但它允许在Presburger扩展中定义一个排名函数,允许与唯一参数相乘M.博兹加河Iosif和Y. Lakhnech在[5]中证明了线性参数Dio- phantine系统(LPDS)是有效可解的。LPDS严格地扩展了Presburger算术的基本部分,允许变量与唯一参数p相乘。我们证明了验证计数器系统(使用Presb可定义线性函数并具有Presb可定义可达集)是否满足LPDS可定义排序函数是可判定的。从这个结果中,我们得到一个自动合成Presburger定义的排名函数或LPDS定义的排名函数的过程。该过程将枚举潜在的排名功能并检查它们。当且仅当存在Presburger可定义或LPDS可定义的排名函数时,该过程终止。所提出的方法被用来验证协议ZCSP的最终终止属性。由于我们的假设和[6]一样一般(比[14]和[7]大),并且我们合成的排序函数的类比[6]大所展示的排序函数不可能用所引用的方法或工具找到,因为它需要最宽松的假设(具有非排他性保护的多路径循环),并且不允许任何Presburger线性排序函数。特别是,在分析多线程程序时,EQUIPATOR关注的是文件的组织。一个初步的部分收集了一些有用的概念,关于可验证和可验证计数器系统。 第3节和第4节将ZCSP协议抽象为计数器系统,并验证FAST实现的安全属性。第5节定义了一种方法来证明计数器系统的最终终止与排名功能的自动合成在第6节中,该方法在ZCSP模型上进行了说明附录给出了E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)8587−→详细介绍了ZCSP协议,并给出了派生的计数器系统。ZCSP协议的描述和第4、5和6节中命题的完整证明在作者网页上的论文长版本的附录中给出。2预赛2.1计数器系统我们记得Presburger算法是结构的一阶理论N,+,=给定一个Presburger公式φ,其自由变量属于计数器集合C,且a∈NC,我们写一个|= φ,如果φ对于估值a为真。一个集合X <$Nn称为Presburger可定义 的 , 当 且 仅 当 存 在 一 个 Presburger 公 式 <$N ( x ) , 其 中 有 自 由 变 量x=<$x1,.,xn≠,使得X ={a∈Nn:a| {\displaystyle {\frac {x}这可以毫无问题地扩展到Zn。普雷斯堡算法是已知的可判定的,因此,在接下来的章节中,所有可以归结为普雷斯堡算法的问题都是可判定的。 我们记得多面体凸集的集合正好等于Presb可定义集的集合,其中Presb可定义集是Presburger存在片段(没有模)。Presburger函数是一个可由Presburger公式定义的部分一个Presburger线性函数f是一个可以用元组(A,b,φ)表示的Presburger函数,其中A是NC ×C中的方阵,b∈ZC,φ是一个Presburger公式,使得f(a)= A。a+ b对于每个a |= φ(φ是表示f的定义域的公式,也用dom(f)表示)。我们将这类函数的集合表示为Czc。定义2.1计数器系统是一个图,它的边被标记为Pres-burger线性函数,即元组CS=<$Q,E<$,其中E<$Q×<$C×Q。带有计数器系统CS =<$Q,E<$,我们将跃迁系统TS(CS)=<$Q×NC,→定义为(q,a)→(qJ,aJ),如果存在跃迁qfqJ在E中,使得aJ=f(a)。图G= Q,E中的一个简单圈是一条没有重复边的闭路(其中初始顶点和最终顶点重合)。 称G是单圈的,如果每个q∈Q至多属于一个单圈。计数器系统CS被称为具有有限幺半群性质,如果在其标签中使用的矩阵生成的乘法幺半群是有限的。注意,对于计数器系统CS=<$Q,E<$,控制状态可以被编码为正整数(即Q<$N),然后配置集由N表示|C|+1。定理2.2[11]设CS是一个具有有限幺半群性质的随机计数系统<$Q,E<$Q,TS(CS)=<$N|C|+1,→那么可达关系的自反和传递闭包→闭 包是有效的Presburger可定义的。在下文中,我们将假设状态集在Nn中。在文献[9]中,引入了计数器系统的时序逻辑具有有限么半群性质和FOPCTL中公式的计数器系统的模型检验是可判定的.88E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)852.2可重构系统的模型检验平板计数器系统具有许多理想的特性,然而,现实的系统很少被验证。有趣的是考虑更大类的系统定义2.3设CS=<$Q,E_j和CS_J=<$Q_J,E_J_j是两个具有有限幺半群性质的同维反系统,h是函数h:Q_J→Q,q∈Q,q_J∈Q_J. <$CSJ,qJ<$$>是<$CS,q<$$>的h -扩张当且仅当h(qJ)= q,CSJ是h,且当<$s,f,sJ<$$> ∈EJ时,有<$h(s),f,h(sJ)<$∈ E.当CSJ,qj是CSj,qj的h-抽象时,CS可以看作是CSJ的抽象.工具FAST [2]通过穷举搜索算法生成搜索注意定义了几个非线性项,并为每一个非线性项建立了FOPCTLPr(Pr)公式的保留子类CS和CSJ之间最常见的关系是可达集的相等性(导致后可达性的概念)。设CS= Q,E是一个计数器系统.来自配置和来自Presburger可定义配置集合的可达性集合定义如下:• 邮政编码def(q,a <${<$qJ,aJ<$$> ∈Q×NC:<$q,a<$→<$ $>qJ,aJ<$}.TS( CS)• 邮政编码)=的def邮政编码(q,a).TS(CS)(q,n(x))=一|= x(x)TS(CS)定义2.4(来自[9])CS,qJ 是一个h-后-后衰减(后-后衰减 为短)的,q相对于)当且仅当后(q,q)=h(后qJ(qJ,q))和TS( CS)TS( CS)CSJ是CS的一个h-可加性(h自然地扩展到TS(CS)的态);我们说CS,q是后可加性的。[9]第九节:如何正确地理解和运用直观地说,系统CSJ是一个跟踪跟踪(参见如果CSJ是CS的一个h-分支,并且如果CS的迹集等于CSJ的迹集的h的像,则为系统CS的一个特征。痕量标记保留了可用于痕量标记计数器系统的FOPCTL_(Pr)的LTL片段。因此,最终终止问题可以表示为LTL公式,因此它对于可跟踪计数器系统是可判定的。例2.5图1中描述的系统CS1不是可编程的,但它是从初始配置Init0=N4后可编程的。从Init0设置的可达性由迹线t1.t<$.t<$.t 4处的加速度获得,迹线t 1. t <$.t4可由加速度计算[11]。2 3此外,CS1是不可追踪的[9]。该系统产生了一个非无限的工会的union(union的大小取决于参数p2,它是无界的)。在实践中,后可验证框架对于验证安全属性非常有效(参见例如[11],[3],[2])。但是,现实的系统很少是可跟踪的。因此,最终终止的证明一般必须依靠另一种方法。E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)8589t1=[TRU E]→{xJ:=p1,yJ:=p2}t2=[x>0]→{xJ:=x−1,yJ:=y}t3=[ x= 0<$ y=0]→{xJ:= p1,yJ:=y−1}t4=[x= 0<$y=0]→ { xJ:= x,yJ:= y}Fig. 1. 一个后可验证但不可跟踪的系统3ZCSP协议的计数抽象3.1ZCSP协议介绍ZCSP协议(Zero-Copy Secure Protocol)是MPC并行计算机中实现的一个通信协议。从本质上讲,ZCSP协议是BRP协议的一个变体,已经被广泛研究(例如,参见[1])。在ZCSP中,在接收到相应的确认之前,可能会发出几个消息;这些确认可能会被无序地接收;发出的消息必须被存储,直到接收到它们自己的确认和它们的前任的确认。这种存储导致比BRP更大的复杂性3.2期望的性质P1. 表 条 目 的数量是恒定的(并且等于TMAX)。P2. 在给定的时间,在重新发射下永远不会有多于一条消息。P3. 如果没有再发射,则再发射计数器被设置为0。P4. 每个丢失的消息将重新发出。P5。 某些消息重新发射将达到最大重传界限。P6。没有重新发出的消息超过最大重传界限。P7。 如果该表包含任意数量的要发出的消息,并且最终没有插入新消息,则该表和通道将不可避免地变为空。3.3ZCSP的计数抽象我们提出了ZCSP的计数器系统抽象。该系统被抽象为两个方向:消息是原子的,并且它们的身份不被表示。计数器系统包含14个计数器。通过这种抽象,表中的消息不是由它们的条目索引标识的,而是由它们的状态标识的。存储表的内容被建模为一组五个计数器c1、c2、c3、c4、c5,指示每个相应类别中的消息信道StoR将消息从发送方传输到接收方,它被建模为两个计数器c6和c7,用于区分消息的第一次发射和再次发射。以相同的方式,从接收器向发射器发送分段的信道RtoS,由两个计数器c8和c9建模。超时发生被建模为两个计数器c10和c11。再发射的当前数量被建模为计数器c12。计数器c13和c14分别包含最大重传次数和存储表中的条目数T2T1T4123T390E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)85TS( CS)我们将Z表示为计数器系统,它由一个唯一的局部状态和16个自循环跃迁组成。Z 的 每个状态s都 是一个元组(s1,s2,. s14)∈ N14;命题3.1对于所有1 ≤i≤ 7,如果则证据(草图)抽象表示ZCSP的被处理器集合的过度近似:文件被表示为计数器,并且文件上的边界被放松。此外,消息现在是原子的。这种粗糙的表示不会错过任何交织,因为在ZCSP中,给定消息的分组是原子地发送Q4使用FAST计数器系统Z未校准。Init是初始状态,定义如下:Init ={s∈N14|s1+ s2+ s3+ s4+ s6+ s7+ s8+ s9+ s10+ s11+ s12= 0s5= s13s13> 0 s14>0}。Init表示当挂起消息表为空(所有条目都是空闲的)、通道StoR和RtoS为空、没有挂起超时且重新发射计数器设置为0时的配置集。命题4.1(Z,Init)是后可验证的。因此,可达性属性可以自动检查。属性P1至P3、P4我们现在集中在属性P7上:“如果表包含任何数量的要发出的消息,并且最终没有插入新消息,那么表和通道将不可避免地变为空”。此属性表示最终终止,它不能还原为可达性属性,但可以用LTL或CTL表示。不幸的是,(Z,Init)的语言包含一个形式为(abpc)n的序列,因此:命题4.2(Z,Init)是不可跟踪的.因此,最终终止属性不能通过(Z,Init)的自动跟踪来检查。排名功能的自动合成是一种替代方法。5用排序函数的5.1终止排序功能让我们注意到CS是计数器系统CS的类,使得关系→实际上是Presburger定义的。我们将CS表示为后CS(相应地,CS跟踪)计数器系统CS的集合,具有初始Presburger集合Init,使得它是后可验证的(相应地,跟踪-可识别的)。让我们注意到:CS跟踪CS后,CSpresb。定义5.1设TS是一个变迁系统,且有两个集合Init和是无死锁的,如果TS∈post(Init)\final,postTS(s)TSE. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)8591TS( CS)TS( CS)命题5.2给定一个计数系统CS∈Cpresb和两个Presburger集初始化和最终化,的无死锁性是可判定的.当CS与有限么半群相交时,(Init)是一个有效的Presburger可定义集,因此:推论5.3给定一个具有有限幺半群和两个Presburger集的可积CS,和Final,则的无死锁性是可判定的.排序函数通常用于证明终止性。一般的排序函数f是从状态集合S到有序集合(N,n)的函数,使得在N中不存在有限个严格递减序列。对于n维计数器系统CS,我们将研究从Nn+1到N的递归函数.这不是限制,因为对于每个排序函数f:Nn+1→Nk,k≥ 1,可以关联另一个排序函数f J:Nn+1→ N,使得f J(x)= y1+ y2+.+ yk,其中f(x)=(y1,y2,., yk)。定义5.4让我们考虑一个转移系统TS(CS)=,它有两组构形Init,FinalS和一个函数f:S→N。我们说递归函数f是(TS(CS),Init,Final)的排序函数,如果<$x,xJ∈ post<$x(Init)\F inal,x→xJ蕴涵f(xJ),配备有两个集合Init,Final,使得(TS(CS),Init,Final)是无死锁的,我们有|= AF Final i如果存在用于的排名函数。5.2排序函数性质给定一个转移系统类C(以S为状态集),一个递归集类X和一个从S到N的递归函数类F,我们区分与每个三元组(C,X,F)相关的两个问题:(i) 存在性排序问题ERP(C,X,F)。输入:给定C中的转移系统TS=,两组配置Init,Final∈X。输出量:判断是否存在排序函数f∈F,?(ii) 验证排序问题VRP(C,X,F)输入:给定C中的转移系统TS=,两组配置Init,Final∈X和函数f∈F。输出:f是的排名函数吗?我 们 表 示 Xpresb ( resp.Xconv ) Presburger 可 定 义 集 合 的 集 合 ( 分 别 ) 。Presburger多面体凸集的集合)和Frec(分别Fpresb和Fpresblin)递归函数的集合(分别为Presburger函数和Presburger线性函数)。92E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)85TS( CS)从活性属性对于后可验证CS是不可判定的这一事实出发,利用有限幺半群,我们可以推导出:命题5.6存在性排序问题ERP(CSpostranking,Xpresb,Frec)是不可判定的。从具有有限幺半群的迹可判定CS的LTL模型检验是可判定的这一事实,我们可以推导出:命题5.7存在性排序问题ERP(CStrace,Xpresb,Frec)是可判定的.有一个减少的问题,测试是否递归函数是减少到VRP(CS后,Xpresb,Frec)。我们建立一个n维的CS,初始状态为Init= 0;CS有一个唯一的局部状态,对于每个计数器ci,都存在一个转换ti:ci:=ci+ 1。 该计数器系统不是可编程的,它是后可达,且其可达性集合等于后可达=NC。 现在一个从N到N的递归函数f是秩函数的条件,仍然可以说f是严格递减的。最后一个问题是不可判定的[12]。因此,我们得到:命题5.8验证排序问题VRP(CSpostRanking,Xpresb,Frec)是不可判定的。虽然这最后一个问题是不可判定的,但对于任何计数器系统CS和任何Presburger函数f,都存在可判定的充分条件;事实上,人们总是可以判定下面的Presburger公式的满足性:(nx,xJ∈NC+1,x→xJ蕴涵f(xJ)f(x))。的排名函数,则返回TRUE,否则转到5(a)6.否则,对每个参数p∈P,枚举所有LPDS函数f(a) 如果CS是凸计数器系统,则a.1.如果f是TS(CS),Init,Final >的排名函数,则返回TRUE0≤s14> 0}。我们将FinalJ表示为ZJ中来自InitJ的不可避免的状态集。finalJ表示一个所有条目都空闲且通道为空的表。它对应于状态集Init。属性P7现在可以表示为: |= 最终J。这可以在ZJ中重新表述:。为了证明这个性质,我们应用了在Sec. 5.3.注:我们可以看到,初始值J,最终值J和ZJ的每个转移的域都是凸的。即使我们可以在理论上决定ZJ是否是凸的,我们也不能自动测试它;一旦实现了[13]的结果,它就会完成。以下是模型检查(Z J,InitJ,FinalJ)的后续步骤:E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)8595ZZJZ步骤1. 计算后初始化J(初始化J)步骤2.计算死锁=<$2 ≤i≤16<$dom(ti)步骤3. post_name(Init_J)\F_inal_JDeadlock=死锁步骤4. 通过对Zj跃迁的静态分析,确定了参数集P={c13,c14}.步骤5. 作为P,我们直接跳到第6步。步骤6. 考虑P中的参数c14,并枚举关于参数c14的LPDS函数f。步骤6.a. 我们post_req_J(Init_J)是凸的;这是可判定的,但尚未自动化。步骤6.b.对于每一个f,判断f是否是绝对排序函数。设f是从N14到N的以下LPDS函数:f(s)=(3.s14+5)(3.s6+2.s8+s10)+(3.s14+4).s4+(3.s7+2.s9+s11+3.s12)+ 2.s2+(s13−s5)命题6.1 f是一个LPDS绝对排序函数,用于。我们还证明:命题6.2 不允许线性排序函数。7结论和展望我们的特点的系统,所提出的分析是feeficiary类。本文提出了一种模型检验算法来分析计数器系统的最终终止性我们的过程是完整的:如果给定类的排名函数存在,则过程终止我们的研究结果扩展了布拉德利的排名功能类为了使模型检验过程自动化,必须解决几个问题。- 有一个有效的解决LPDS的程序。据我们所知,不存在这样的专用工具。- 有一个有效的枚举方案的潜在排名功能(无论是Presburger或LPDS定义)。可以遵循Bradley- 以确定PostInit(Init)是否为多面体凸集。一种进行的方法是将Post_Init(初始化)的符号表示转换为Presburger公式,然后检查这个公式是否是凸的。引用[1] P. Abdulla,A.Annichini和A.布阿贾尼有损信道系统的符号验证:应用于有界重传协议。用于构造和分析的96E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)85系统(TACAS),计算机科学讲义第1579卷,第208-223页。Springer,1999年。[2] S. Bardin,A.Finkel,J.Leroux和L.彼得鲁奇快速:符号转换系统的快速加速在CAV 2003,第15届计算机辅助验证国际会议,美国科罗拉多州博尔德,计算机科学讲义第2725卷,页短文。Springer,2003年。[3] S. Bardin和L. 彼得鲁奇从pnml到用fast加速petri网的计数器系统。在Petri网交换格式研讨会,博洛尼亚,意大利,2004年,第26-40页[4] V. Beaudenon,E. Encrenaz和J. - L.德巴比厄带自旋的零电流源的设计验证。 在IEEE第三届国际并发系统设计应用会议(ACSD)上,第102-110页IEEE Computer Society Press,2003.[5] M. 博兹加河Iosif和Y.Lakhnech 平参数计数器自动机。在自动机,语言和编程,第33届国际学术讨论会,ICALP 2006,意大利威尼斯,会议录,第二部分,计算机科学讲义第4052卷,第577-588页。Springer,2006.[6] A. Bradley,Z. Manna和B.西普玛 整数线性回路的终止性分析。 2005年CONCUR- 并发理论,第16届国际会议,CONCUR 2005,旧金山,加利福尼亚州,美国,计算机科学讲义第3653卷,第488-502页Springer,2005.[7] B. 库克A.Podelski和A.雷巴琴科系统代码的终止性证明在PLDI,Proceedings of the ACM SIGPLAN2006 Conference on Programming Language Design and Implementation , Ottawa , Ontario ,Canada,June 11-14,2006,pages 415[8] B. 库克A.Podelski和A.雷巴琴科终结者:超越安全。计算机辅助验证,第18届国际会议,CAV 2006,西雅图,华盛顿州,美国,第415-418页,2006年[9] S. Demri,A.芬克尔河谷Goranko和G.范·德里默伦。面向计数器系统的模型检查器在ATVA 2006第四届自动化技术验证与分析国际研讨会上,北京,中国. 计算机科学讲义第4218卷,第493-507页。Springer,2006.[10] J. - L. 德巴尔比厄岛Glck,A Zerrouki,A.Fenyo,A Greiner,F.瓦伊斯布尔特角Spasevski,F.席尔瓦,E.德雷福斯mpc并行计算机的协议与性能分析。在第15届国际并行与分布式处理研讨会上,第52页. ACM,2001年。[11] A. Finkel和J. Leroux。如何合成Presburger加速度:广播协议.在第22届软件技术和理论计算机科学基础会议(FSTTCS)中,印度坎普尔,计算机科学讲义第2556卷,第145- 149156. Springer,2002年。[12] 阿兰·芬克尔,皮埃尔·麦肯齐,还有克劳丁·皮卡罗尼。一个结构良好的分析Petri网扩展的框架。信息与计算,195(1-2):1[13] J. 勒鲁数判定图的多项式时间presburger准则与综合在20IEEE Symp. 计算机科学中的逻辑(LICS),第147-156页。IEEE Computer Society Press,2005.[14] S. Leue和W.伟.基于区域图的终止性证明方法。在TACAS,Tools and Algorithms for the Constructionand Analysis of Systems,第12届国际会议,TACAS 2006,作为欧洲软件理论与实践联合会议的一部分举行,ETAPS 2006,奥地利维也纳,2006年3月25日至4月2日,第318[15] A. Podelski,A.and Rybalchenko.线性秩函数综合的一个完整方法在验证,模型检查,和抽象解释,第五届国际会议,VMCAI2004,,卷2937计算机科学讲义,2004年。附录A-痕量的设CS= Q,E是一个计数器系统.一条迹,一条迹是一个(可能是无限的)序列,其形式为一条迹0,一条迹0,一条迹1,一条迹2,一条迹2.。 使得,对于对Q × NC中的任意i,<$qi,ai <$i→ <$qi+1,ai +1<$i. 在C中的一个图,表示为def由迹CS(λq,λ q)表示。 通过扩展,迹CS(q,n)=n q,an|=10迹CS(10迹,a迹)。定义7.1CSJ,qj是h-跟踪-衰减(简称跟踪-衰减),迹CS,q关于迹CS(q,q)的k ≠ 0当且仅当CS(q,q)=h(迹CSJ(qJ,q))且CSJ是CS的h-可迹化,我们称迹CS,q是可迹化的.E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)8597图二. ZCSP的一个场景附录B7.1协议的总体架构已经开发了第一个模型,并使用模型检查器SPIN([4])实现了有限实例的验证。该模型非常接近协议的实际实现,特别是对未决消息的管理得到了忠实的体现。该方案的总体架构见附录中的图3它由一个发射器和一个接收器组成,通过两个单向有界通道连接,以FIFO顺序存储和检索数据。过程的详细信息见[4]。发射器由一个待处理消息表(详见附录)和两个修改其内容的异步进程sender和update接收器由唯一的进程接收器组成。它检查接收到的数据包是否是等待的数据包,如果接收到的数据包是消息的最后一个,则发送确认。通道StoR存储从发射器到接收器的消息分组,通道RtoS存储从接收器到发射器的确认分组。7.2一种可能的场景图2呈现了一种可能的场景。消息A被发送,并且其内容丢失。同时,消息B被正确地发送。 然后消息A被完全重新发出。但这并不意味着它是一个(第一次)发布消息的顺序。7.3协议架构图3呈现了协议的总体架构。98E. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)85图三. ZCSP的架构7.4表格的结构挂起消息表是TMAX槽的数组,其中包含有关消息的信息• 已发送,但尚未确认,• 已经确认,但是前面有一个未确认的消息(在重新发射下)。一个时隙可以是空闲的,也可以包含有关未决消息的信息。这涉及:消息的第一个序列号,消息的分组数,确认位,重传位。对表的访问以循环方式执行。表中的“空闲”由三个指针指出:FF(表示进程sender和update读取和修改挂起条目表的内容。当一个新的消息必须被发送时,进程发送者将消息标识符放在第一个自由条目表中(修改FF指针),并将消息发送当接收到确认或超时时,进程更新修改表条目指针,或者在超时的情况下修改FT,或者在确认的情况下修改eldP和FTE. Encrenaz,A.Finkel/Electronic Notes in Theoretical Computer Science 239(2009)859923Eld_P FT FF免费已发送,未确认,也未超时发送,超时,当前重新发射已发送,已确认sent,timeout(to be re-emitted)见图4。 桌子的配置7.5表的计数抽象在消息挂起表中的消息被分类为五个集合。• 集合1:消息已发送,未发生超时,未收到确认(FT、FF[和ack= 0]中的消息条目)• 集合2:消息已发送,确认已接收,但先前消息接收超时(因此,还不能离开表)(FT,FF[和ack= 1中的消息条目• 集合3:当前正在重新发射的消息(字段P,FT中的消息条目),ack= 0,且eldP =FT− 1)• 集合4:要重新发出的消息(字段P,FT中的消息条目并且ack= 0)= 1且eldP
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 京瓷TASKalfa系列维修手册:安全与操作指南
- 小波变换在视频压缩中的应用
- Microsoft OfficeXP详解:WordXP、ExcelXP和PowerPointXP
- 雀巢在线媒介投放策划:门户网站与广告效果分析
- 用友NC-V56供应链功能升级详解(84页)
- 计算机病毒与防御策略探索
- 企业网NAT技术实践:2022年部署互联网出口策略
- 软件测试面试必备:概念、原则与常见问题解析
- 2022年Windows IIS服务器内外网配置详解与Serv-U FTP服务器安装
- 中国联通:企业级ICT转型与创新实践
- C#图形图像编程深入解析:GDI+与多媒体应用
- Xilinx AXI Interconnect v2.1用户指南
- DIY编程电缆全攻略:接口类型与自制指南
- 电脑维护与硬盘数据恢复指南
- 计算机网络技术专业剖析:人才培养与改革
- 量化多因子指数增强策略:微观视角的实证分析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功