以太网CSMA/CD协议的概率模型分析及性能定量研究

理论计算机科学电子笔记128（2005）195-214www.elsevier.com/locate/entcsCSMA/CD协议的概率模型检验使用PRISM和APMC玛丽·杜杜洛特2，1 洛朗·弗里堡2，3托马斯·埃罗4RichardLassaigne5Fr'ed'ericMagniettte7 St'ephaneMessika2，3Sylvain Peyronnet5，6 Claudine Picaronny2，3摘要载波侦听多路访问/冲突检测（CSMA/CD）是以太网中用于载波传输访问的协议（国际标准IEEE802.3）。在以太网上，任何网络接口卡（NIC）都可以随时尝试在通道中发送数据包。 如果另一个NIC试图同时发送数据包，则会发生冲突，数据包将被丢弃。CSMA/CD协议就是为了避免这个问题而设计的，更准确地说，是为了允许NIC在没有冲突的情况下发送数据包。这是通过随机化指数回溯过程来完成的。本文利用概率模型检验和近似概率模型检验技术对CSMA/CD协议的正确性进行了分析。我们使用的工具是PRISM和APMC。此外，我们提供了一些CSMA/CD性能的定量分析保留字：概率模型检验，近似验证，案例研究，IEEE802.3。1LACL，巴黎第十二大学（duflot@univ-paris12.fr）2由FrencprojtRNTL“A v e r o e s“提供资源3LSV，CNRS&ENSC ach a n（弗里堡|Messika |picaro@ls v. 恩，恩。（f、r）4巴黎大学Xi，INRIA Grand-Large（herault@lri.fr）5法国国家科学研究中心巴黎第七大学逻辑设备部（lassaign@logique.jussieu.fr）6EPITA研发实验室（LRDE）（peyronnet@lrde.epita.fr）7CNRS（magniett@lri.fr）1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.012196M. Duflot等人理论计算机科学电子笔记128（2005）1951介绍载波侦听多路访问/冲突检测（CSMA/CD）协议是一种基本的分布式网络协议。事实上，它是IEEE 802.3国际标准（以太网网络通信协议）最重要的部分之一。在以太网中，多个网络接口卡（NIC）可以通过同一通道连接。由于两个路由器可能同时发送数据包，因此可能发生冲突，从而丢弃两个数据包。这两个路由器都将检测到这种冲突，但不能立即重新发送数据包，因为这会引发新的冲突。因此，当发生冲突时，CSMA/CD协议强制每个NIC从有界间隔中随机选择整数值延迟，并在重新发送数据包之前等待与此整数值延迟成比例的时间长度。本文研究了概率模型检验技术在IEEE802.3CSMA/CD协议验证中的应用。在这里，我们感兴趣的是建立协议的定量属性，例如计算给定事件在某个截止日期之前发生的概率。还计算其他值，例如发送数据包所需的最大预期时间。在[21，23]之后，我们在概率时间自动机（PTA）的框架中对该协议进行了建模。PTA [24]是时间自动机[1]的扩展，其中包含离散转换的概率分布。由于实值时钟变量的存在，PTA具有无限数量的状态。然而，对于我们在这里考虑的一类可达性性质，人们总是可以导出一个等价的有限状态转移系统（见[23]）。我们在这里采用一种方法（在[8，23，22]中称为“整数语义”方法），其中时钟被视为存储非负整数值的计数器，其随着时间的推移而PTA对系统进行建模，然后简化为有限状态马尔可夫决策过程[10]。然后，我们使用模型检查工具PRISM [30]来分析CSMA/CD协议的马尔可夫决策过程。然而，原始常数所使用的协议，tocol导致一个模型的规模过大。因此，使用PRISM进行验证需要在执行验证之前将所有时间常数除以某个“时间单位”的长度。部分缓解这一限制的一种方法是消除不确定性的来源，用概率分布取代不确定性选择（源于系统组件的定时转换和异步乘积然后，底层的马尔可夫决策过程成为一个在两种工具中使用相同的输入格式（ReactiveModules，[2]）来处理模型M. Duflot等人理论计算机科学电子笔记128（2005）195197同时使用这些工具的好处是双重的：(i) PRISM允许验证具有非确定性选择的模型，但尺寸较小（由于状态空间爆炸现象），而APMC允许验证较大的模型（即CSMA/CD协议的实际值），但仅限于完全概率系统（在用概率分布取代非确定性选择之后）。(ii) 此外，使用基于不同方法的两种不同工具允许对协议给出不同的观点，利用两种工具的优点。本文结构在描述了相关工作（第2节）之后，本文继续介绍CSMA/CD及其在马尔可夫决策过程框架中的建模（第3节和第4节）。在本文的其余部分（第5和第6节），我们介绍了两种专用于概率系统模型检查的工具，并简要描述了它们的理论框架和几个实验的结果。我们讨论这些结果，再次验证CSMA/CD协议。这是第一次使用概率和近似模型检查技术来完成。2相关工作CSMA/CD是一种使用各种技术的广泛研究的协议。在这里，我们专注于与模型检查和近似相关的技术以前对CSMA/CD LAN的研究主要涉及使用两种方法进行性能评估：分析模型[12，26]或仿真[29]。开发了几种模型来分析吞吐量链路和分组延迟：从简单的传统模型[26]到更复杂的模型[6，18]。其他作者基于详细的模拟和测量进行性能研究，以避免分析模型采用的一些简化假设[9]。很少有论文考虑在定时模型上自动验证时间和概率规格对于一些离散时间模型，[14]给出了该协议的时间约束。在[31]中，系统的行为由乘积时间自动机描述。然后，使用时间自动机模型检查工具KRONOS来验证诸如• “无论何时两个帧同时发送都检测到冲突”，• “a198M. Duflot等人理论计算机科学电子笔记128（2005）195• “when时间自动机模型检查工具，如UPPAAL [27]和KRONOS[11]不允许验证概率规范的满足情况据我们所知，迄今为止，只有一次尝试使用概率模型检查器来验证在[17]中，工具RAPTURE已被用于计算设备具有N个连续冲突的概率的上限。该工具使用抽象和细化技术来减少执行验证之前的状态空间，从而更有效地获得近似结果。在[21]中，概率模型检查工具PRISM [30，20]用于验证IEEE 802.11协议（WLAN的CSMA/CA）的概率属性。例如，可以计算两个站最终正确地发送它们的分组的最小概率和一个站在某个截止期限内递送分组的最小概率。3CSMA/CD协议CSMA/CD协议（带冲突检测的载波侦听多路访问）是一种网络仲裁协议，它规定了通过唯一信道进行通信的多个代理之间的通信。在ieee802.3[5]标准精确地描述了协议的不同方面我们关注的是协议的半双工版本（一次只能携带一条消息）。发射所有代理在向网络发送消息的能力方面都是平等的（多路访问）。粗略地说，每个代理必须感测信道（Carrier Sense），并且在开始发射之前等待不存在信号。 由于信号需要有限的时间（这里用σ表示）来传播，两个代理可能都感测到信道是空闲的，因此开始发出（几乎）同步，这产生了随后的消息冲突。因此，碰撞检测最多需要2σ µ s（见图1）。 在这段时间之后，如果没有检测到冲突，发送方可以安全地完成发射。这里假设完全发送一条消息的时间是一个常数μs，记为λ。（例如，对于σ= 24µ s的10 Mbps以太网通信，对于大小为1024字节的消息，传输时间约为780µM. Duflot等人理论计算机科学电子笔记128（2005）195199一.B一...................... ..<............ . . . . . . . . .............. . . . . . . . . ............ . . ... . . .......a.... .. . . . . . . ....t0. .t0+σ. .. . “的意思。..A开始发送碰撞.................................................... . .. . . . ....t2t 1A......你好。. .. .....<. .. .BB开始发送t1 t0+σA和B都检测到冲突，最坏情况下 t2= t0+2σ0。一条路径代表了非决定论和概率的一个特定的分解：它是一个非空的有限元素a0，µ 0a 1，µ 1或概率跃迁的有限序列π=s0−→s1−−→· ·such0=S。我们用π（i）表示π的第（i+ 1）个状态，用last（π）表示π的最后一个状态，如果π是有限的。 一个对手只代表一个非决定论的特定解决方案。形式上，MDP的对手是一个函数A，它将每个有限路径π映射到一对（a，µ），使得（last（π），a，µ）∈Steps。根据特定对手A的MDP的演化是与A相关联的无限路径的可测量集合，其可以经典地提供概率度量。给定目标状态的集合FS，令：∗P（s-→AF）表示从初始状态开始的恢复Fs的概率在A.最大可达概率Pmax（s→F），（resp. 最小可达性概率Pmin（s→ΔF））是最大值（分别为最小的）概率在所有的对手，其中一个给定的一组状态可以达到∗初始状态：P∗Max（s→ΔF）=maxA{P（s−→A（resp. Pmin（s→s）一F）=minA{P（s−→非正式地，PmaxF）}）。（s→ΔF）（resp.Pmin（s→F））表示概率当所有非确定性选择都是有利的时，MDP达到F，（分别）尽可能的不好。要在MDP上检查的可达性属性的规范可以用PCTL表示，PCTL是流行的时序逻辑CTL的概率扩展。在[7]中，作者提供了一种算法，通过计算最大和最小概率，丰富了有限状态系统上CTL公式检验的常用算法。这可以通过求解线性规划系统在多项式时间内完成。PRISM [20]是一种概率模型检查器，它为马尔可夫决策过程的分析提供支持，并使用[7]的模型检查算法对MDP的PCTL公式进行验证。其中最昂贵的部分是可达性概率的计算。为此，有两种选择，要么是线性优化问题的解决方案或迭代数值求解技术（基于动态编程）。PRISM使用其中的第二个。每次迭代计算可达性概率的新值，趋向于精确解。当计算收敛到所需精度（用户指定的参数ε为了分析MDP，PRISM必须构造完全可达的状态空间和表示它的转移矩阵然而，该工具通常可以204M. Duflot等人理论计算机科学电子笔记128（2005）195处理非常大的模型，因为它使用符号模型检查技术。 它使用基于BDD（二元决策图）的数据结构，特别是MTBDD（多端BDD，参见例如[15]）。在本文中，我们使用了PRISM的原型扩展，它为基于成本（或相反，回报）的属性分析提供了支持[22]。模型的每个状态或转换都可以分配一个成本。PRISM允许计算，例如，在达到某组状态之前累积的预期成本量 因为我们使用MDP，我们必须计算最小或最大预期成本（在所有非确定性的解决方案上）。在PRISM中，这些属性表示为(i) Rmin[真实U目标](ii) Rmax[真实U目标]。PRISM使用[3]的算法来执行这些公式的模型检查。5.2实验所有实验均使用具有1Gb RAM的Pentium IV 2.80GHz运行。由于模型的大小（多达数千万个状态），我们有我使用了PRISM的MTBDD引擎，它通常对大型系统更有效。我们将近似参数设置为10−6。模型变得如此庞大的主要原因是计算时间（有界概率可达性）。对于期望的时间，由于成本不存储在模型的状态中，因此状态空间相当小。与APMC的主要区别（见第6节）是PRISM可以处理模型固有的不确定性通过有效地构建模型，它可以选择非确定性的“最佳”或“最差”解决方案，并给出最差和最佳情况的现实分析，例如这里具有至少N次也可以对发送或不发送消息的选择是非确定性的情况进行建模，我们稍后会看到。概率可达性的验证由于模型的大小，不可能使用常数λ和σ的实际值用PRISM进行验证。然而，我们保留了我们还将最大碰撞次数α（用于计算碰撞后发送新消息之前的随机延迟我们已验证的三个主要特性如下：M. Duflot等人理论计算机科学电子笔记128（2005）195205见图4。 PRISM测量（截止日期= 210，λ= 96，σ= 3，α= 6）• 属性1表示达到至少一个节点在截止日期d之前成功发送消息的状态的最小概率。这是写的（在PCTL）：Pmin [真实U（（s1 = 8 |s2 = 8）&y≤d）] 8• 性质2-3分别表示到达发送方1在截止日期d9之前已经发生至少N个冲突（其中1≤N≤α）的状态的最小和最大概率。这可以写为：Pmin [true U（col1 = N&y≤d）] Pmax[true U（col1 = N&y≤ d）]。图4（a）显示了对于截止日期d的不同值满足性质1的概率。有三条曲线，对应于建模系统的非确定性程度.在我们的模型中，非决定论确实有两个主要来源第一个来源来源于位置0的无限等待期（分别为当发送器在位置0时，它在每个时间单位非确定性地决定是否开始发射10。不确定性的另一个来源是由于send1和send2等send1和send2的异步操作的交错。第一条曲线对应于原始的非确定性模型。8我们关注Pmin，因为Pmax快速收敛到1[9]由于系统是对称的，因此发送者1和发送者2的概率是相同的[10]在这种情况下，我们假设至少有一个发送者尝试发送一条消息，因为如果没有人尝试发送消息，那么至少有一条消息被接收的概率总是0！206M. Duflot等人理论计算机科学电子笔记128（2005）195第二条曲线是通过将每个发送者位置0处的非确定性分支替换为均匀概率转移而获得的第三种方法是用一个统一的概率转移来代替组合系统的每个不确定性选择。(This对应于PRISM提供的完全概率选项。）请注意，后一条曲线与用APMC获得的近似曲线相同，如图5（a）所示。对于200个时间单位的最后期限以及完全概率、概率发送和非确定性发送模型，属性1的验证分别从不到1秒（对于较小的最后期限）到2小时65分钟和9分钟。性质2-3如图4（b）所示，其中常数λ= 96，α= 6，σ= 3，截止日期d=210。我们将截止日期设置为210，因为在那个时候，消息被发送的概率非常高（大于0.98）。至少发生三次碰撞的概率非常高，但之后会迅速下降，直到我们考虑的最大碰撞次数α，即6。这些曲线说明了不确定性对可能的碰撞次数的影响对属性2和3的验证（取决于N）从12分钟到78分钟，截止日期为210。性质2和性质3与[17]中研究的性质类似。在他们的模型中，由于发送者在固定的重试次数后放弃，所有的执行都是有限的，他们不需要设定最后期限。这给出了一个小得多的模型，使他们能够考虑三个方面。在这里，由于我们有一个时间计数器，我们能够计算时间限制的可达性以及预期时间，我们将在下一节中看到。预期时间使用PRISM的原型扩展，它可以计算预期成本，我们计算了（最大冲突数为6）发送消息的最大预期时间：Rmax [true U（（s1= 8）|（第2条=8））]。 概率发送模型的结果为144.4，147.0对于具有不确定性发送的一个。这两个结果之间没有多大关于期望时间，我们还考虑了到达给定发送者成功发送消息的状态的最大期望时间（因为系统是对称的，所以这个概率对于两个节点是相同的）：Rmax[true U（s1= 8）]。在这种情况下，选择非确定性或概率性发送的效果至关重要。概率发送的结果是707个时间单位，非确定性发送的结果是5750个。这表明，通过反复尝试发送消息（只要协议允许），一个发送者可以延迟另一个发送者很长一段时间。这种现象M. Duflot等人理论计算机科学电子笔记128（2005）195207这是因为如果发送者成功地发送了消息，则其冲突计数器被重置，而另一个发送者的计数器没有被重置。 因此，对于已经成功的发送者来说，再次发送更容易。最后一个结果说明了能够真正建模非决定论的重要性。 对于最后一个属性，“最坏情况”的预期时间与我们所做的概率近似的预期时间相差甚远。上述四个预期时间计算分别花费8 min、35 min、4 h和6 h。图4（a）表明，完全概率模型和非确定性模型具有相似的一般行为，并证明了第6节中遵循的方法。6使用APMC工具进行APMC是一个近似概率模型检查器，专门用于验证离散时间马尔可夫链（DTMC，即完全概率系统）上的定量属性。它使用与PRISM（反应模块）相同的输入语言。6.1APMC的理论基础APMC方法[13]使用有效的蒙特卡罗方法来近似完全概率转移系统上单调属性的满足概率。要检查的属性以LT L：线性时序逻辑表示。APMC方法6.1完全概率转移系统（PTS或DTMC）是一个元组M=（S，s，P），其中S是一组状态，s是初始状态，P是转移概率函数。我们用P ath（s）表示第一状态为s的路径集合。路径的长度π是路径中状态的数量，并表示为|π|这个长度可以是无限的。集合P ath（s）上的概率测度Prob以经典的方式定义[19]。 我们用Prob[φ]表示路径{π|π（0）= s和M，π| = φ}（参见[28]）。设P路径k（s）是PTS中从s开始的长度k >0的所有路径的集合。LT L公式φ在P路k（s）上的概率是P路k（s）中满足φ的路的测度，记为如果s是初始状态，则通过Probk[φ]定义6.2 LT L公式φ是单调的当且仅当对所有k > 0，对所有长度为k的路π，M，π |= φ = φM，π+|= φ，其中π+是任何路径208M. Duflot等人理论计算机科学电子笔记128（2005）195εδ其中π是一个前缀。单调公式的一个基本性质是：若φ是单调公式，0b≤ 1，且存在某个k∈N∞使得Probk[φ]≥b，则Prob[φ] ≥b.<为了验证一些概率规范Prob [φ] ≥b，我们选择k = O（log）的第一个值|S|），然后我们近似概率Probk [φ]并测试结果是否大于b。如果Probk[φ]≥b为真，则该性质的单调性保证Prob[φ]≥b为真。否则，我们增加k的值并再次近似Probk[φ]。 我们把这个在许多情况下，在一定范围内的过程是对数的状态数。在最坏的情况下，这个界限与底层马尔可夫链的快速混合率密切相关[25]。如果所有检验的结果Probk[k]≥b都是负的，那么我们可以得出结论：Prob[k]/≥b。如果我们只对概率时间有界性质感兴趣，在这种情况下，我们可以将k设置为指定的子公式中的最大时间界限。随机逼近方案为了用一个简单的随机算法来估计单调属性的概率，我们在深度为k的DTMC结构的概率空间中生成随机路径，并计算一个随机变量A/N估计概率k[k]。为了验证命题Probk[k]≥b，我们检验A/N是否> b−ε。我们的决定是正确的，有信心（1-δ），样本数为1和log1的多项式。的主要优点这种方法的一个优点是，我们可以用一种简洁的转换图表示法来进行处理，这是一种输入语言的简洁描述，也是PRISM [2]中使用的语言。我们的近似问题定义为输入x是MDP的简洁表示，公式和正整数K. 简洁的表示用于生成一组执行路径长度为k。随机近似方案是一种随机算法，它以高置信度计算公式φ在执行路径集合上的概率度量μ（x）的良好近似定义6.3概率问题的完全多项式随机近似方案（FPRAS）是一个随机算法A，它以x为输入，两个实数0<ε，δ 1并产生一个值A（x，ε，δ），使得：ΣΣProb|A（x，ε，δ）−µ（x）|≤ ε≥1 −δ。A的运行时间是多项式，|X|，1和log 1。ε δ概率被算法的随机选择所取代。我们称M. Duflot等人理论计算机科学电子笔记128（2005）195209ε为近似参数，δ为置信参数。算法的复杂度为O（1）。日志1）路径，验证ε2δ在每条路径上的公式φ和计算满足路径的分数。定理6.4APMC逼近算法是一个全随机逼近方案，其概率为LT L公式的概率p = Probk [k]，如果 p∈]0，1[.这个结果是通过在独立随机变量和的分布的尾部上使用Cherno-Hoe-Bounding界[16]得到的算法的复杂度取决于log（1/δ），这允许我们将δ设置为非常小的值。对ε的依赖性更重要，因为复杂度是1/ε的二次方。6.2实验我们在与PRISM实验相同的模型上使用APMC。 APMC是一个分布式近似模型检查器[13]，它使用客户端/服务器计算模型在机器集群上分发路径生成和验证。用户通过在服务器（主机）上运行的图形用户界面输入模型、公式和其他参数。 模型和公式都被翻译成C源代码，编译并在客户（工人）请求作业时发送给他们。工作者定期发送当前的验证结果，从主机接收确认，以知道他们是否必须继续或停止计算。由于工作者只需要存储生成的代码和一个路径的内存，因此验证需要很少的内存。此外，由于每条路径都是独立验证的，因此不存在负载平衡问题。实验条件所有的实验都是使用一个具有512 Mb RAM的75 Pentium IV 2GHz集群运行的。我们设定近似参数ε= 10−2，置信参数δ= 10−10。CSMA/CD模型由三个变量λ、σ和α参数化。我们做了几个实验，我们确定了这三个参数的不同值。在下面的段落中，我们介绍了我们的实验。对于每个验证的属性，我们提供了两个结果：一个与使用PRISM验证时使用的参数相同（见5.2节），另一个是CSMA/CD协议的实际值（即λ= 780，σ=24，α= 10）。210M. Duflot等人理论计算机科学电子笔记128（2005）19510.90.80.70.60.50.40.30.20.1010012014016018020010.90.80.70.60.50.40.30.20.10100012001400160018002000最后期限（步数）(a)（λ=96，σ=3，α=6）最后期限（步数）(b)（λ=780，σ=24，α=10）图五. 作为截止日期函数的排放概率。概率可达性的验证在这里，我们近似的概率发送方正确地交付其数据包在给定的最后期限（属性1节5.2）。作为近似方法的验证，我们首先计算λ= 96，σ= 3和α= 6的概率。结果见图5（a）。正如预期的那样，APMC获得的结果与图4（a）的结果完全相同。图5（b）显示了使用方案的实际值验证相同属性的结果。时间有界碰撞我们近似的概率得到至少N个冲突在协议的执行中，对于不同的N值（第5.2节的属性2和3）在给定的截止日期之前。作为近似方法的验证，我们首先计算了λ= 96，σ= 3，α= 6和N∈[1; 6]时的概率。 我们使用210作为截止日期。结果见图6（a）。作为预期，该图表明APMC计算的概率是由PRISM在属性2和3中计算的最小和最大概率的下限和上限。图6（b）显示了对实际价值的相同衡量，截止日期为2000年。我们用较小的截止日期值运行了一组实验，表明当截止日期减少时，碰撞的数量会减少。6.3分析图6（b）分析了至少发生N次碰撞的概率（1≤N≤10），对于CSMA/CD协议的实际值，具有两个发射APMCPRISM（全概率）P [（真U（（s1=8）|P [真U（（s1=8）|M. Duflot等人理论计算机科学电子笔记128（2005）195211见图6。 发生N次以上碰撞的概率，作为N的函数。在一个单一的频道。我们可以看到，当2N≤σ时，发生N次碰撞的概率几乎为1。一旦2N> σ，该概率迅速减小（这也在图4（b）中显示，σ= 3）。自从两次世界大战开始在相同的状态下，第一次碰撞的概率很大。它们有相同的col初始值，所以它们在相同的时间间隔内随机选择一个backo。对于较小的N值，间隔不足以保证两个backo之间的时间差大于σ。现在，当这个差异小于σ时，没有一个网桥检测到信道繁忙，所以它们产生新的冲突。可以观察到该协议没有引入太多的冲突：该协议被校准为处理最多10个冲突，这似乎是合理的，因为在我们的实验中，在相同的初始状态下（该测量的最坏情况），我们观察到具有10个冲突的概率非常低。图5（a）和5（b）分析了从两个中继器之一成功发送消息的概率我们可以在两个图上看到从零概率到非零概率的发射之间的差距。 第一个非零概率的时间T0由下式给出：从 建 模 中 推 导 出 的 公 式 ， 并 通 过 一 组 补 充 实 验 证 实 ： T0TBacko （ Nmin ） +3×Nmin×σ+λ，其中Nmin是不可避免的碰撞的最小数量，如图6（a）和6（b）所示，TBacko（Nmin）是相应Backo期间花费的平均时间。对于协议的实际值，我们有Nmin= 5，TBacko_n（Nmin）= 31。 请注意，这不是一个严格的等式，因为在我们的建模中，我们花费了恒定数量的时间单位等待两个变量中的一个进入212M. Duflot等人理论计算机科学电子笔记128（2005）195sending state.在这个间隙之后，发射的概率迅速增加到渐近行为，接近1。这满足了协议的目标：在短延迟之后发送消息的概率很高（例如，在其传输延迟两倍之后，消息被有效发送的概率大于0.9）。最后，可以在曲线上观察到持续的高原现象。这是由于截止日期不够大，发送方无法进入备份过程，从而成功发送数据包。这并不是一个令人惊讶的结果，因为它已经在[12，29]中使用其他技术（如模拟）显示。我们进行了一些额外的实验，这些实验表明，平台的长度是σ的线性函数，并且与λ无关。7讨论在本文中，我们应用概率和近似模型检验技术来验证CSMA/CD协议的定量属性。据我们所知，这是第一次研究这两种技术的互补性，这样一个模型。在这里，我们考虑了两个不同的框架：MDPs和DTMC。一些测量只能在DTMC模型上实现，这提供了不太准确的信息。因此，我们首先检查DTMC模型的结果与MDP模型的结果一样有意义。图4（b）表明，对于碰撞次数最少的实验，考虑完全概率模型似乎是合理的。事实上，我们可以看到，完全概率度量遵循与最小概率相同的趋势。由于这两种工具使用不同的理论，另一个问题是确保PRISM和APMC的结果是等效的。图6（a）和图5（a）显示，对于相同的完全概率模型，这两种工具获得了相同的度量（直到近似参数）。我们假设该性质对于CSMA/CD协议的参数的其他值也成立。一方面，使用PRISM，我们能够验证该协议作为一个概率系统的非确定性，从而模拟它的异步行为，但参数小于“现实生活中”的另一方面，使用APMC，我们能够用实际值来验证协议，但是用概率选择代替不确定性选择确认我们要感谢David Parker和Jeremy Sproston进行了有益的讨论。M. Duflot等人理论计算机科学电子笔记128（2005）195213引用[1] R. Alzheimer和D. L.迪尔时间自动机理论。理论计算机科学，126：2，pp。183-235，1994年。[2] R. Alzheimer和T. 亨辛格 Reactive模块。 在LICS 96，1996的程序中。[3] L.德·阿尔法罗 概率系统的形式验证。1997年获斯坦福大学博士[4] APMC网页http://apmc.berbiqui.org[5] IEEE网页http://www.ieee802.org/3[6] M.伯纳多扩展马尔可夫过程代数的理论与应用。 博洛尼亚大学博士，1999年。[7] A. Bianco和L. 德·阿尔法罗 概率和不确定系统的模型检验。在proc 第15届软件技术和理论计算机科学基础会议，第499-513页，LNCS：1026，1995年。[8] D.拜尔基于BDD的时间自动机可达性分析的改进。在Proc. FME[9] D. R.伯格斯，J.C. Mogul和C. A.肯特测量以太网的容量：神话与现实。SIGCOMM'88通信体系结构和协议会议录.[10] C.德曼 国家马尔可夫决策过程，学术出版社，1970年。[11] C. Daws，A. Olivero，S. Tripakis和S.尤文KRONOS工具混合系统III：验证和控制，第208-219页，LNCS：1066，1996年。[12] T. A. Gonsalves和F. A.刀木以太网中站点位置和访问协议参数对性能的影响。 IEEE通信学报，第36卷，第4期，第441-449页，1988年4月。[13] T.埃罗河Lassaigne，F. Magniette和S.佩罗内近似概率模型检验。第五国际VMCAI'04会议记录[14] H. A.汉森分布式系统形式设计中的时间和概率。乌普萨拉大学博士论文，1991年。[15] H. Hermanns，M.夸特科夫斯卡湾Norman，D.帕克和M. 西格尔 使用MTBDD进行随机系统的性能分析和验证。《逻辑与代数编程杂志：系统设计与分析的概率技术特刊》（Journal of Logicand Algebraic Programming：Special Issue on Probability Techniques for the Design andAnalysis of Systems）。pp23 -67，56：1-2，2003。[16] W.锄头。有界随机变量和的概率不等式。美国统计协会杂志，58：13-30，1963年。[17] B. Jeannet，P. R.