IEEE-1394根竞争协议的概率属性自动验证

104《理论计算机科学电子札记》66卷第2期（2002）网址：http://www.elsevier.nl/locate/entcs/volume66.html16页IEEE-1394根竞争协议与KRONOS和PRISM合作*Conrado Dawsa，1，Marta Kwiatkowskab，Gethin NormanbaCWI，P.O.Box 94079，NL-1090 GB阿姆斯特丹，荷兰Conrado. cwi.nlb伯明翰大学，伯明翰B15 2TT，英国{M.Z.Kwiatkowska，G.Norman}@ cs.bham.ac.uk摘要我们报告了IEEE 1394根竞争协议的定时概率属性的自动验证，该协议结合了两个现有的工具：实时模型检查器KRONOS和概率模型检查器PRISM。该系统被建模为概率时间自动机。我们首先使用KRONOS来执行符号前向可达性分析，以生成从初始状态到最后期限到期之前以非零概率可达的状态集。 然后，我们将这些信息编码为马尔可夫决策过程，用棱镜进行分析。我们应用这种技术来计算一个领导者在截止日期前当选的最小概率，对于不同的截止日期，并研究使用有偏见的硬币对这个最小概率的影响。关键词：模型检测，软截止期，概率时间自动机，IEEE 1394，根竞争协议1介绍许多硬件和软件系统的设计和分析，如嵌入式系统和监控设备，除了功能要求外，还需要详细了解其实时方面。通常，这是用硬实时约束来表示的;例如， 在安全关键系统的情况下，必须确保这些约束永远不会失效。*部分由EPSRC赠款GR/N22960支持。1 由ERCIM奖学金支持。2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。DAWS，KWIATKOWSKA，NORMAN105然而，在其他情况下，如在有损介质的存在下执行的多媒体协议，这样的硬期限可能过于限制。在这些情况下，软截止日期是一个可行的选择。例如，多媒体系统的软截止时间可以是软截止期限还可以指定容错和可靠性属性，例如最近的研究[16，17]为时间概率系统的规范和验证建立了一个理论框架。受实时模型检查器（如Kronos [7]和Uppaal [18]）的成功启发，所采取的方向是通过模型检查进行自动验证，将用于定时系统模型检查的形式主义和算法[1]适应于定时概率系统的情况。在该方法2中， 定时概率系统被建模为概率时间自动机[16]，即时间自动机与边相关的离散概率分布和属性在逻辑PTCTL中指定，该逻辑PTCTL用概率算子扩展了定量分支时态逻辑TCTL。由于时间的密集性，模型检查算法依赖于系统状态空间的有限商的构造，即区域图[16]或前向可达图[17]。通过将相应的概率分布添加到图的转移中，我们得到马尔可夫决策过程（MDP）。这个MDP的一个状态满足一个性质的概率可以通过求解一个适当的线性规划问题来计算[6，5]。在这项工作中，我们展示了如何基于这些想法，实时模型检查器KRONOS[7，12]和概率模型检查器PRISM[13，19]可以结合起来自动验证IEEE 1394的根竞争协议，这是一种定时和概率协议，用于解决领导者选举过程中竞争的两个节点之间的冲突。 感兴趣属性是在截止日期前选出领导者的最小概率。 我们首先使用KRONOS3执行符号前向可达性分析，以生成从初始状态到最后期限到期之前以非零概率可达的状态集。 然后我们将这些信息编码为一个马尔可夫决策过程在棱镜输入语言。最后，我们用棱镜计算了不同截止日期下，在截止日期前选出领导者的最小概率，并研究了使用有偏见的硬币对这个最小概率的影响。这篇文章如下。第2节介绍了概率时间自动机和定义概率可达性。在第3节中，我们描述了在我们的验证方法中使用的KRONOS和PRISM的特征。在第4节中解释了棱镜输入语言中的可达性图的编码。第5节通过验证根争用来说明这种方法[2]在这项工作中，我们考虑只有离散概率出现的系统3使用了一个尚未分发的实验版本，该版本已被适配为处理概率时间自动机并生成所需的输出DAWS，KWIATKOWSKA，NORMAN106∧≤≥∈∈ X发送x ≤5x：=0x= 3x ≥40的情况。99x：= 0等x ≤30的情况。01x：=0误差Fig. 1. 概率时间自动机PTA1的一个例子。IEEE 1394标准。 我们以第6节结束。2概率时间自动机时间自动机[2]是一种扩展了时钟的自动机，具有正实值的变量随时间均匀增加。时钟可以与正整数时间界限一致，以形成时钟约束，例如（x2）（x5）。有两种类型的时钟约束：标记节点的不变量和标记边的守卫。如果时钟满足不变量，自动机只能停留在一个节点上，让时间流逝。当一个守卫被满足时，可以采取相应的边缘。转换是瞬时的，并且可以用形式为x：= 0的时钟重置来标记，这意味着在进入目标节点时，时钟x的值被设置为0。概率自动机将概率分布添加到边缘，模拟动作发生的可能性。例2.1图1的概率定时自动机PTA1模拟了一个过程，该过程在4到5ms之间尝试发送一个数据包，如果成功，则在尝试发送另一个数据包之前等待3 ms。 数据包以概率0发送。因为一个错误，以0.01的概率输了。请注意，属于同一分布的边必须使用相同的保护标记。2.1语法时钟和估值。设时钟的集合X是从时域R +取值的变量的集合。 一个闭赋值是 一 个 点 v∈R|+X|.clock 值 0∈R|+X| 将 0 赋 值 给 X 中 的 所 有 clocks 。 设v∈R|+X|beaclock估值R+是持续时间，X是时钟的子集。 则v+t表示v和t的时间增量，并且v[X：=0]表示从v获得的时钟值R|+X|通过将X中的所有时钟复位到0，并保持所有其他时钟的值不变。区界限设Z是X上的区域集，它们是形式为x<$c和x−y<$c的原子约束的合取，其中x，y∈ X，<$∈ {<，≤，≥，>}，c∈N。一个时钟估值v满足了区域V，写为v|，当且仅当DAWS，KWIATKOWSKA，NORMAN107→→⊆ × × ××→X−→∈X∈如果在将每个时钟x∈ X替换为相应的时钟值v（x）之后，设X是一个区域，X是一个时钟子集然后是表示时钟估值集合v + t的区域，使得v| = 0且t≥ 0，并且t [X：= 0]是表示时钟估值v [X：= 0]的集合的区域，使得v| = 0。概率分布。有限域上的光盘再现性分布集合Q是函数μ：Q[0， 1]，Q的子集上的分布集。q∈Qµ（q）= 1。设Dist（Q）为定义2.2（概率时间自动机）概率时间自动机是一个元组PTA=（L，，L，I， P），其中：L是位置4的有限集合;L是标签的有限集合;函数I：LZ是不变条件;和有限集合P LZΣ距离（2XL）是概率边关系。 边采用元组（l，g，X，lJ）的形式，其中l是其源位置，g是其使能条件，X是重置时钟的集合，并且lJ是目的地位置，使得（l，g，σ，p）∈ P并且p（X，lJ）> 0。2.2语义概率时间自动机PTA的状态是一对（l，v），其中l∈L且v∈R|+X|苏志辉|=I（l）. 如果当前状态是（l，v），则存在在满足不变量的同时让时间流逝条件I（l），或根据P中具有源位置l且其使能条件g满足的任何概率边进行离散转移。 如果选择概率边缘（l，g，σ，p），则移动到位置lJ并将X中的所有时钟重置为0的概率由p（X，lJ）给出概率时间自动机的语义是根据transi定义的，同时表现出非确定性和概率性选择的系统称为概率系统，它本质上等价于马尔可夫决策过程。2.2.1概率系统。概率系统PS=（S，Act，Steps）由状态集合S、动作集合Act和概率转移关系StepsS×Act ×组成。距离（S）一个概率转换a，µsJ由状态s∈S通过首先，非确定性地选择一个动作分布对（a，μ），使得（s，a，μ）步，然后通过对目标状态sJ进行概率选择”（《易经》卷一）：“，。定义2.3（概率时间自动机的给定一个概率时间自动机PTA=（L，，Act，I，P），PTA的语义是概率系统[[PTA]]=（S，Act，Steps），定义如下。（美国）LetSL×R|+X|使得（l，v）∈S当且仅当v|=I（l）.4有时，我们会将初始位置L以图形方式表示为传入的箭头。 在这种情况下，模型从l开始，所有的clock都设置为0。DAWS，KWIATKOWSKA，NORMAN108−−−→−−−→fulfulfuldefdef（行动）设行动= R+ R。（概率转移）设步长是概率转移的最小集合，对于每个状态（l，v）∈S：时间转换。 F或每个区间t∈R+，let（（l，v），t，μ）∈Steps当且仅当（1）μ（l，v+ t）=1，且（2）v+tJ|=I（l），对于所有0 ≤tJ≤t。离散过渡。 对于每个概率边（l，g，σ，p）∈ P，令（（l，v），σ，μ）∈步骤当且仅当（1）v |= g，以及（2）对于每个状态（lJ，vJ）∈ S：Σμ（lJ，vJ）=p（X，lJ）.X<$XvJ=v[X：=0]&2.3概率可达性一个概率时间自动机的行为是描述其语义的行为，也就是说，一个概率系统的行为道路。 概率系统PS的一条路是一个非空的有限或无限长跃迁序列ω=s0a0，µ0a1，µ11···对于路径ω和i∈N，我们用ω（i）表示ω的第（i+ 1）个状态，用last（ω）表示ω的最后一个状态，如果ω是有限的。对手。 一个对手是一个函数A，它将每个有限路径ω映射到一对（a，µ）∈Act×Dist（S），使得（last（ω），a，µ）∈Steps[22]。让AdvPS成为PS的对手。对于任何A∈AdvPS，设路径A表示集合与A相关的无限路径。 路径A上的概率测度ProbA可以这样定义[11]。定义2.4设PS =（S，Act，Steps）是一个概率系统。 然后，对于对手A ∈AdvPS，从状态s ∈ S可以到达目标状态集合F ∈ S的可达性概率为：P rob Reac hA（s，F）d=efP ro bA{ω∈Pat hA|ω（0）=s&<$i∈N. ω（i）∈F}。此外，最大和最小可达性概率分别定义为MaxProbReachPS（s，F）=sup ProbReachA（s，F）A∈AdvPSMinProbReachPS（s，F）= infProbReachA（s，F）A∈AdvPS3KRONOS和PRISM由于时间的密集性，（概率）时间自动机的底层语义模型是有限的，因此有效的决策过程依赖于建立状态空间的有限商，例如区域图或前向可达性图。本节描述基于使用KRONOS生成前向可达图的验证技术，以及SDAWS，KWIATKOWSKA，NORMAN109|∈ ∈⊆⟨⟩对编码为马尔可夫决策过程的所获得的图进行模型检查，棱镜。3.1KRONOS的前向可达性KRONOS的前向可达性算法通过使用状态集的符号表示（称为符号状态）对可达状态空间进行图论遍历来进行 符号状态是一对形式为l，，其中lL和Z，这样，I（l）;它表示所有状态（l，v），所以v=？遍历是基于迭代的后继算子在两个交替的步骤：首先计算的边缘后继，然后计算的时间后继的符号状态。3.1.1边缘继承者。关于边e=（l，g，X，lJ）的l，j的边后继是edge succ（nl，nn l，e）=nlJ，（nng）[X：= 0]nl（lJ）n3.1.2时间的继承者时间继承者的时间继承者的时间继承者被定义为time succ（n，n）=n→I（l）图2示出了针对15 ms的最后期限针对概率定时自动机PTA1所获得的可达性图，该可达性图利用额外的时钟y来测量。 由于y永远不会重置，它的值将无限地增加。为了获得有限可达图，我们需要应用[8]的外推抽象，当y >15时，它抽象出y注意，这个抽象对于可达性属性是精确的。3.2基于PRISM的PRISM[19]是一个模型检查器，旨在验证不同类型的概率模型：离散时间马尔可夫链（DTMC），马尔可夫决策过程（MDP）和连续时间马尔可夫链（CTMC）。要检查的属性在概率时态逻辑中指定，即如果模型是DTMC或MDP，则为PCTL [6，5]，如果模型是CTMC，则为CSL [4]。我们专注于MDP上的可达性的模型检验，因为（非确定性）概率可达图属于这类模型，并且截止日期属性被指定为时间有界的可达性属性。3.2.1模型检查MDP。马尔可夫决策过程的模型检验是基于计算状态s满足可达性公式φ的最小概率p（s，φ）或最大概率P（s，φ）。一个国家的幸福l，DAWS，KWIATKOWSKA，NORMAN110等y−x∈[4，5]0的情况。99等x≤3y−x∈[11，13]0的情况。99等x≤3y−x>150的情况。99x≤3发送0发送4发送x≤5y−x ≥140的情况。0170的情况。99派遣10名x≤5y−x= 00的情况。01x≤5y−x ∈[7，8]0的情况。01x≤5y−x>150的情况。01误差x= 0时y >15前误x=y错误11x=y39851P ≤ P≥误差2x= 0时y∈[4，5]误差6x= 0时y≤15图二. PTA 1的可达性图PTCL公式≤λ（<$φ）i <$P（s，<$φ）λ，≥λ（<$φ）i <$p（s，<$φ）λ。最大和最小概率通过求解线性规划问题来计算[6，9]。在PRISM中实现的迭代算法可以将不同的数值计算方法与不同的计算方法结合起来，数据结构[13，14]。3.2.2模型检查PTA。我们使用以下结果[17]通过模型检查其概率可达性图来验证PTA：在可达性图上计算的最大概率是概率时间自动机的语义模型上定义的最大概率的上限也就是说，MaxProbReachPS（s，F）≤P（s，φF），其中φF是表征状态集合F的公式。4PRISM中可达图的编码用KRONOS得到的可达图是一个符号状态和它们之间的为了对概率特性进行我们必须使用棱镜的描述将其编码为马尔可夫决策过程语言，一种简单的、基于状态的语言，类似于Reactive Modules [3]。系统的行为由一组形式为[] -> command>的保护命令描述。 守卫是系统变量的谓词。一个命令描述了一个转换，如果守卫为真，系统可以通过给一个新的值作为一个函数， 未初始化变量的旧值。我们考虑两种类型的编码的可达图在这种语言。DAWS，KWIATKOWSKA，NORMAN1114.1显式编码第一种解决方案是使用单个变量s对可达图进行直接显式编码，该变量s的值是可达图的状态的索引。系统的变迁由保护命令编码，使得保护测试s的值，并且命令根据可达性图的变迁关系来更新s的值。例如，对应于图2的可达性图中的位置发送，从状态0、 4和7的传出转换的编码是：[]（s=0）-> 0.99：（s '= 1）+0.01：（s'= 2）[]（s=4）-> 0.99：（s '= 5）+0.01：（s'= 6）[]（s=7）-> 0.99：（s '= 8）+0.01：（s'= 9）该编码生成可达性图的大小的描述它可以随着截止日期的值而急剧增长棱镜涉及一个模型构建阶段，在此期间解析系统描述，转换为MTBDD表示以供进一步分析。 当输入文件不符合系统的模块化和结构化描述时，此阶段可能非常耗时，例如使用显式编码。因此，需要允许更紧凑地描述系统的编码。4.2编码可达图的状态对应于生成它的时间自动机的位置的几个实例然后我们可以用两个变量对它们进行编码，一个位置变量l和一个实例变量n，描述它对应于位置的哪个实例。例 如 ，设l = 0为与send对应的location变量的值。然后，状态0、 4和7对应于该位置的三个不同实例，例如n=0、n=1和n= 1。n=2。然后，从对应于send的状态的传出转换可以通过以下方式指定：[]（l=0）（n=0）-> 0.99：（[]（l=0）（n=1）-> 0.99：（[]（l=0）（n=2）-> 0.99：（4.2.1相对压实实例变量n在命令中保持不变，这意味着转换只会删除实例0、1和2的位置变量。这相当于写nJ=n，可以省略，因为默认情况下，未更新的变量采用其旧值。因此，上述过渡可以是在一行中描述得更复杂：[]（1 =0）（0 =n =2）-> 0.99：（DAWS，KWIATKOWSKA，NORMAN112由于在可达性图中，两个给定位置之间的转换可以针对不同的实例重复多次，因此这种编码允许我们以更紧凑的方式指定它们。我们将此称为相对压缩，因为它基于指定相对于旧值n。压缩算法基于可达性图的转换集合的遍历，以便找到对应于相同更新命令的那些转换，然后在单行中将它们描述为来自多个状态的转换。此外，我们将对应于相同位置和连续实例数的不同源状态组合在一个简单的约束中，其中n在两个边界之间，如上面的示例所示4.2.2绝对压实在可达性图中，我们可以遇到作为目的地的状态许多不同的转换，如状态错误之前（1= 3，n = 0）在图2的例子。在这种情况下，如果我们用它的绝对值指定更新值nJ，则与上述算法类似的算法将允许我们描述所有传入的转换都在一条线上。例如，之前的两个错误转换可以描述为：[]（1 =2）（0 =n =1）-> 1：（1 '= 3）（n'= 0）我们将把这称为绝对压缩，因为它是基于指定nJ的绝对值。注意，这种压缩也可以应用于显式编码。然而，由于在实践中，导致更紧凑的描述，压缩算法仅在实例编码的情况下实现。绝对压实在与相对压实结合使用时特别有趣4.2.3组合实现的启发式算法包括首先应用相对压缩，然后对于那些无法压缩的转换5根竞争协议IEEE 1394高性能串行总线用于在多媒体系统和设备（如TV、PC和VCR）的网络内传输数字化视频和音频信号。它具有可扩展的体系结构，并且是热插拔的，这意味着可以随时在网络中添加或删除设备，支持异构和异步通信，并允许快速，可靠和廉价的数据传输。它是目前用于互连多媒体设备的标准协议之一。该系统针对不同的任务使用许多不同的协议，包括领导者DAWS，KWIATKOWSKA，NORMAN113111选举协议，称为树识别协议。树标识协议是在网络中总线复位之后，即当节点（设备或外围设备）被添加到网络或从网络移除时发生的领导者选举协议。在总线复位后，网络中的所有节点都具有相同的状态，并且只知道它们直接连接到哪些节点，因此必须选择领导者。该协议的目的是检查网络拓扑结构是否是树，如果是，则在网络上构造一棵生成树，其根是由协议选出的领导者为了选出一个领导者，节点与它们的邻居交换“成为我的父母”的请求。然而，当两个节点同时向彼此发送“成为我的父母”请求时，可能出现争用。标准采用的解决方案来克服这种冲突，称为根争用，是概率和定时的：每个节点将分配一个硬币，以决定是否等待短时间或长时间的请求。该协议感兴趣的属性是领导者是否在某个截止日期之前以一定的概率或更大的概率当选。5.1模型图3中的概率时间自动机Ip它是[20]的定时自动机I 1的概率扩展，其中分叉边缘的每个实例对应于被分割的硬币。例如，在初始位置start start中，存在对应于节点1的非确定性选择（分别为节点2）启动根争用协议，并对其硬币进行加密，导致慢启动和快启动中的每一个的概率分别为0.5。开始慢，开始快）。为简单起见，图中省略了概率标签，概率边由虚线箭头表示。Ip中的时序约束对应于更新标准IEEE 1394a中规定的时序约束。例如，如果节点使用长导线连接，则360 ns对应于网络中的传输延迟。 其他类型线的传输延迟不同，因此可以通过更改此值并重新运行实验来验证。当然，较低的延迟导致在截止日期之前选举领导者的概率更大或相等5.2验证我们首先生成概率时间自动机的可达图p直到超过 截止日期D。为了做到这一点，我们增加了一个额外的时钟y，它测量自执行开始以来经过的时间。在输入位置done后，我们在时间零处进行测试（时钟x在所有传入边，以及不变量x= 0迫使系统立即离开该位置），无论是否超过最后期限，都通过添加来自done的两个传出边，其中一个具有导致位置的保护y> D一个是在之后完成的，另一个是在保护y≤D的情况下完成的，从而导致在之前完成的位置。我DAWS，KWIATKOWSKA，NORMAN1141P入门开始x≤360x：=0x≥760x：=0x≥1590快速启动快速启动慢速启动x≤360x ≤ 360x≤ 360x≤ 360x：=0x：=0x：=0x：=0x：=0x：=0x：=0x：=0快速快速x≤850快慢式x≤1670慢快x≤1670慢慢x≤1670x≥400x≥1230x≥1230x≥1230x：=0做x= 0时x：=0y≤Dy>D做之前做后图三.概率时间自动机Ip建模根争用协议。然后，我们指定的根竞争协议，我们感兴趣的属性，即领导者被选为截止日期前至少有一个给定的概率。指定此属性的PCTL公式为P≥λ（λ（doneλy≤D）），无法用我们的技术验证，因为概率量化器P≥λ不是正确的形式。 但可以证明[15]它等价于公式1−λ（后完成），实际上可以在可达图上验证。5.3实验结果为了验证上述性质，我们计算了在截止日期之前选出领导者的最小概率，截止日期从4µs到100µs不等。这些实验在运行Linux的PC上进行，具有1400 MHz处理器和512 MB RAM。棱镜使用其默认选项。更多信息可参见[19]。表1示出了关于可达性图的KRONOS生成及其作为MDP的编码的结果。前两列给出了可达性图的生成信息，它的大小以状态数和生成它所需的时间（秒）表示。其余的列显示了KRONOS生成的MDP文件的大小，以行数（即转换）表示，对于我们考虑的不同编码：显式，绝对或相对压缩的实例，以及两者兼而有之。图4显示了在不同的截止日期值下生成的文件行数的变化它表明，实例编码允许压缩，这大大减少了DAWS，KWIATKOWSKA，NORMAN表115115可达图的生成与编码截止日期（µs）向前。到达。显式实例ABS实例rel实例绝对值+相对值国时间（秒）105260.03709421126392018760.0925311501368723040490.20546632407341004070340.4694995629122312650108651.23146748694184215960155112.742095212412258618680272968.94368682184144372431004240122.2957274339266797303600005000040000300002000010000020 40 60 80 100 120截止时间（微秒）见图4。 MDP的行数MDP文件，并且在考虑相对和绝对压缩的情况下，行数的增长小于截止日期值的线性增长。关于棱镜验证的实验结果见表2。最左边的一列显示了属性中使用的截止日期，最右边的一列显示了系统在截止日期之前达到选出领导者的状态的最小概率。结果反映了一个明显的事实，即增加最后期限增加了领导人当选的概率。请注意，对于超过40µs的截止日期，计算的概率相同，这意味着迭代方法已经收敛，也就是说，实际概率的差异小于10−6。剩余的列给出了关于棱镜的时间性能的信息，以秒为单位，使用显式编码和具有相对压缩（inst+rel）以及具有相对和绝对压缩（inst+rel+abs）的实例编码来构建模型（标记为model的列）和计算概率（标记为verif的列）。外显本能 腹 肌Inst. Rel.Inst.Rel.+ABS.行数DAWS，KWIATKOWSKA，NORMAN表116116模型构建和验证截止日期（µs）显式inst+relinst+rel+abs概率型号验证型号验证型号验证40.6260.0090.0610.0060.0540.0070.62561.5880.0130.1110.0070.0730.0080.85156285.6540.0180.1950.0080.1400.0080.9394531013.3380.0290.3010.0090.1960.0100.97473120190.9710.0983.0380.0251.3030.0260.999629301037.8920.30914.6720.0564.9690.0580.99999340––344.2510.13430.1470.1120.99999850––1119.0080.34950.1290.2040.99999860––3468.3100.442233.2720.3510.99999880––––814.0350.7290.999998100––––2861.8891.7440.999998350030002500200015001000500020 40 60 80 100截止时间（微秒）图五、是时候建立模型了与之前的根争验证尝试[15]相比，协议使用惠泽[10]，可达图的生成是不需要的。更长的问题，因为它只花了大约20秒来生成它的一个最后期限为100µs，而使用HYTECH生成它大约需要24小时，最后期限为6µs。此外，在最坏的情况下，概率属性的模型检查不到两秒钟。从这个结果中可以清楚地看出，这种验证方法的瓶颈现在是PRISM的模型构建阶段，我们的验证方法的实际成功取决于改进编码或模型构建算法。图5显示了使用不同编码为不同截止日期构建模型所需时间的演变。我们可以看到，尽管压缩改进了构建模型所需的时间，但后者仍然随着截止日期的值而急剧增长，即使输入文件的大小外显Inst.Rel.Inst. Rel.+ABS.时间（秒）DAWS，KWIATKOWSKA，NORMAN117表3有偏见的硬币选举领导人的概率快速慢D=6µsD=10µs.01.990.0392110.076886.10.900.3305340.551770.20.800.5545160.801000.30.700.7043520.910950.40.600.7991500.957090.45.550.8300270.968230.50.500.8515620.974731.55.450.8646160.977771.60.400.8694980.977795.65.350.8656090.974558.70.300.8508980.966919.80.200.7689420.923030.90.100.5442730.746829.99.010.0768720.130600线性增长，因为压缩后的警卫的复杂性。5.4有偏见的硬币的RCP我们现在研究使用有偏见的硬币对协议性能的影响。如[21]中所述，该协议的一个奇怪属性是，如果两个节点选择快速定时的概率增加，则在截止日期之前选举领导者的概率可以稍微增加。这是因为，虽然协议需要更多的回合来选举领导者，但当两个进程都选择快速计时时，每回合的时间较低表3给出了在6µs或10µs之前选出领导者的概率，对于两个节点选择快或慢定时的概率的不同值。给出的结果对应于模型检查，与使用优化的实例编码之前相同的属性。注意，我们不需要计算每种情况下的前向可达性。相反，由于选择快或慢定时的概率可以作为PRISM描述语言中的参数给出，因此使用相同的输入文件来执行概率模型检查，并且只有概率的实际值发生变化。6结论我们已经提出了一种方法来自动验证软截止日期的时间概率系统建模为概率时间自动机。我们使用KRONOS来生成关于最后期限，并将其编码为棱镜输入语言。然后用棱镜验证概率可达性属性。我们成功地应用了这一点，DAWS，KWIATKOWSKA，NORMAN118验证技术的时间和概率根竞争协议的IEEE 1394。我们计算了在不同的截止日期之前选出领导者的最小概率，并研究了使用有偏见的硬币对这个最小概率的影响。我们不得不面对的主要障碍是在棱镜输入语言中的可达图的编码。PRISM的模型检查算法基于（MT）BDD，因此其输入需要以紧凑和结构化的方式指定。一个显式的编码的可达性图使用一个单一的变量来编码的状态被证明是不可行的，即使是最后期限的小值。实例编码使用两个变量，一个对应于时间自动机的位置，另一个对应于可达性图中该位置的实例，允许我们应用压缩技术来帮助克服这个问题。然而，目前尚不清楚这一解决方案的普遍性。找到一个好的编码是至关重要的。当然，我们需要通过将其应用于出现时序和概率方面的其他系统或协议来验证这种方法为了做到这一点，需要更好地整合这两种工具。朝着这个方向迈出的第一步是实现概率时间自动机的并行组合，以便我们能够以组合的方式对复杂系统进行确认我们感谢Sergio Yovine为我们提供了KRONOS引用[1] R. 巴尔角Courcoubetis和D.迪尔密集实时的模型检查信息与计算，104（1）：2[2] R. Alzheimer和D. L.迪尔时间自动机理论。Theoretical Computer Science，126（2）：183[3] R. Alzheimer和T. A.亨辛格Reactive模块。系统设计中的形式化方法，15（1）：7[4] C.拜尔湾Haverkort，H. Hermanns和J. - P·加藤通过瞬态分析对连续时间马尔可夫链进行 在proc CAV'00，LNCS，2000。[5] C. Baier和M.Z. 奎亚特科夫斯卡具有公平性的概率分支时间逻辑的模型检验分布式计算，11（3）：125[6] A. Bianco 和 L. 德 · 阿 尔 法 罗 概 率 和 不 确 定 系 统 的 模 型 检 验 。 另 外 ，Thiagarajan，编辑，FSTTCS'95会议记录Springer-Verlag，1995.DAWS，KWIATKOWSKA，NORMAN119[7] C. Daws，A. Olivero，S. Tripakis和S.尤文工具克洛诺斯。In R. 但是，T. A. Henzinger和E. D. Sontag编辑，混合系统III，计算机科学讲义第1066卷，第208Springer-Verlag，1996.[8] C. Daws 和 S.Tripakis 。芽 孢 杆 菌 中 Ste Escheren ， 编 辑 ， Proc.TACASSpringer-Verlag，1998.[9] L. 德·阿 尔法 罗概 率系 统 中最 小和 最大 可 达时 间的 计算 。 Baeten 和S.Mauw，编辑，Proceedings of CONCURSpringer Verlag，1999年。[10] T. A. Henzinger，P.H. Ho和H.王台HYTECH：一个模型检查器混合系统Software Tools for Technology Transfer，1（1+2）：110[11] J. G. Kemeny，J. L. Snell和A. W.纳普可数马尔可夫链。数学研究生教材。Springer，第2版，1976年。[12] Kronos web 页.http://www-verimag.imag.fr/TEMPORISE/kronos/。[13] M.夸特科夫斯卡湾Norman和D.帕克PRISM：概率符号模型检查器。在J.B。T. Field，P. Harrison and U. Harder，编辑，Proc. TOOLS 2002，LNCS的第2324卷，第200-204页。施普林格，2002年。[14] M.夸特科夫斯卡湾Norman和D.帕克概率符号模型检验与PRISM：一种混合方法。在J. - P. Katoen和P. Stevens，编辑，Proc. TACAS 2002，LNCS第2280卷，第52-66页。施普林格，2002年。[15] M.夸特科夫斯卡湾诺曼和J·斯普罗斯顿。IEEE 1394火线根竞争协议中截止日期属性的概率模型检验。IEEE 1394标准形式化方法应用研讨会，2001年。[16] M. Z.夸特科夫斯卡湾诺曼河，巴西-地Segala和J.Sproston。具有离散概率分布的实时系统的自动验证。LNCS第1601卷，第75-95页。Springer-Verlag，1999.[17] M. Z.夸特科夫斯卡湾诺曼河，巴西-地Segala和J.Sproston。具有离散概率分布的实时系统的自动验证。理论计算机科学，286，2002。出现。[18] K. G. Larsen，P. Pettersson，and W.逸 简单地说。 软件工具技术转让，1（1+2）：134[19] 棱镜 web 页. http://www.cs.bham.ac.uk/~dxp/prism/。[20] D. Simons和 M. 斯 托 林 加 使 用 Uppaal2k 对 IEEE 1394a 根 竞 争 协 议 进 行Springer International Journal of Software Tools for Technology Transfer ，2001。出现。[21] M.斯托林加Alea jacta est：概率、实时和参数系统的验证。博士论文，奈梅亨大学，2002年。[22] M. Y.瓦迪概率并发有限状态程序的自动验证。在FOCS'85会议记录中IEEEComputer Society Press，1985.