理论计算机科学电子笔记139（2005）25-47www.elsevier.com/locate/entcs时间自动机霍华德·鲍曼1，鲁道夫·戈麦斯2，3和李苏4英国坎特伯雷肯特大学计算机实验室摘要时间自动机是描述和验证实时系统的一个非常成功的符号，但时间锁可以自由出现。这些都是违反直觉的情况，其中规范对组件自动机的描述可能会无意中阻止时间超过某个点，可能会特别地，零时间锁表示在有限时间段内执行有限计算的情况Zeno-timelock对于实时模型检查器来说是很难检测的，例如UPPAAL和Kronos。我们开发了一个工具，它可以将UPPAAL模型作为输入，并返回一些可能导致zeno-timelocks的循环。该工具实现了一种算法，该算法改进了Tripakis引入的静态验证方法。我们说明了使用这个工具在现实生活中的案例研究，CSMA/CD协议。关键词：时间自动机，零时间锁，UPPAAL。1介绍时间自动机是形式化方法的成功案例之一。这在很大程度上是因为它们已经被证明可以使用符号模型检查进行自动验证。也许这种符号模型检查最突出的体现是UPPAAL工具[7]，它已经被用于1 电子邮件：H. kent.ac.uk2 由ORS奖励计划资助。3电子邮件：rsg2@kent.ac.uk4电子邮件地址：ls68@kent.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.00626H. Bowman等人/理论计算机科学电子笔记139（2005）25验证一些重要的实时系统（访问www.uppaal.com获取示例和文档）。尽管这些成功的应用程序的时间自动机模型检测，有一些困难的方法。也许最重要的是，时间锁可以自由地出现，而且，确定一个非平凡系统没有这样的时间锁是非常困难的非正式地说，如果一个系统可以达到一个状态，在这个状态下，没有可能的后续运行允许时间发散，即通过一个无限的量。重要的是要注意，时间锁可能会由于多种原因而出现，并且不同类别的时间锁需要以不同的方式处理特别是，我们可以区分以下两类时间锁。时间动作锁定是其中既不能执行时间也不能执行动作转换的状态，这通常在系统的紧急性和同步属性之间存在冲突时出现，即，当位置不变量确保组件自动机必须在没有其他组件自动机正在执行匹配的半动作的时间执行半动作时。因此，同步必须发生（由于紧急约束）在其未被启用的点处Zeno-timelock是指时间不能超过某个点，但操作继续执行的情况。因此，系统继续进化，但这些进化都不会使时间发散。这种悖论运行的特点是，在有限的时间内执行同样重要的是要认识到，时间锁与动作锁非常不同，动作锁是不定时规范中死锁的类似物。关键是，动作锁允许时间流逝;自动机可能无法执行任何进一步的“有用”计算，但它仍然可以传递时间，这意味着它不会阻止其他组件自动机传递时间。本地actionlock不会全局传播的事实是actionlock比timelock更受欢迎的原因由于全球时间的流逝依赖于本地时间的流逝，所以在时间锁定位置出现了全球传播正如一个时间自动机的集合只能以t个时间单位传递时间，如果所有的组件自动机都可以以t个时间单位传递时间因此，自动机在时间的流逝中自动同步。在以前的论文中，我们已经考虑了时间锁问题，对不同类型的时间锁进行了分类，并强调了与这些不同类别的需求相对应的解决方案[3，2，4]。我们的主要兴趣在这里虽然是与zeno-时间锁，我们提出了一种分析方法，以确保zeno-时间锁的情况下，建立在强非zenoness的概念引入TripakisH. Bowman等人/理论计算机科学电子笔记139（2005）2527[9]的文件。我们展示了如何Tripakis特别是，强非zenoness和同步组件之间的关系进行了更详细的分析此外，我们提出了一个工具，我们已经开发了实现这种语法验证UPPAAL类时间自动机规范。此外，新的句法属性，在强非Zenoness的精神，提出了也确保Zeno时锁自由。这种仅基于succient-only的方法只能保证zeno-timelock不会发生，但它有两个重要的优点：a）它在语法层面上工作，因此比可达性分析更有效，b）它直接在时间自动机模型上识别zeno-timelock的所有潜在来源。因此，即使该方法未能识别出模型没有zeno-timelocks，它也可以帮助用户将分析范围缩小到模型的特定部分据 我们 所 知 ，没 有 其他 工 具实 现zeno-timelock 自 由的 语 法 例如 ，UPPAAL不支持任何形式的zeno-timelock检查。其他一些工具做得更好，例如。Kronos [10]，但他们从其他问题中获得了支持。例如，Kronos不是像UPPAAL那样可用的工具。UPPAAL提供了一个开发良好的GUI，丰富的建模语言，图形模拟器和快速验证器等功能。Kronos可以验证TCTL公式<$Q <$Q=1为真，其满足表示确保时间锁定自由的充分必要条件，但其验证基于可达性分析。因此，对于某些规范，检查Kronos中的时间锁自由可能是最昂贵的检查要求，并且检查它的需要可能会阻止完全验证。我们首先定义时间自动机及其语法（见第2节）。然后我们总结了死锁的分类，特别是时间锁（见第3节）。在此之后，我们强调我们的zeno-timelock检查方法背后的理论（见第4节）。然后，本文的主体描述了我们的工具，并提出了一个通过验证CSMA/CD协议的zeno-timelock检查的案例研究（第5节）。最后，第6节提出了结论性意见，并提供了一个附录，其中包括证明的定理在文件中本文的扩展版本见[5]。2时间自动机记法基本套件CA是一组已完成的（或内部的）操作。HA={a？，a！|a ∈ CA}是a28H. Bowman等人/理论计算机科学电子笔记139（2005）25一组半（或未完成）的动作。这些给出了一个简单的CCS风格[6]点对点通信，例如，类似于UPPAAL [7]中的同步原语。因此，两个行动，一个？和一个！可以同步并生成完成的动作A。A=HACA是所有动作的集合R+表示没有零的正实数，R+0=R+n { 0}。C是集合所有时钟变量，取值为R+0。CC是一组形式为x<$n，x−y<$n或φ1<$φ2的时钟约束，其中n∈N，x，y∈C，φ1，φ2∈CC且<$∈ {<，>，=，≤，≥}。同样，如果CC，我们将C中的时钟生成的时钟约束集写为CCC。V=C→R+0是可能的时钟赋值的空间，VC=C→R+0是C中时钟的时钟赋值的空间。L是所有可能的自动机位置的集合。时间自动机A是所有时间自动机的集合，A的任意元素具有形式（L，l0，T，I，C），其中元素如下。L∈L是位置的有限集合;l0∈L是指定的起始位置。C是定时自动机的时钟集合。T<$L×A×CCC×P（C）×L是一个转移关系（其中P（S）表示S的幂集）。T的一个典型元素是（l1，a，g，r，l2），其中l1，l2∈L是自动机位置;a∈A标记转换;g∈CCC是保护;r∈P（C）是重置集。（l1，a，g，r，l2）∈Tistypically写成l1−−a，−g，→rL2，说明自动机可以从如果（时钟）保护G保持，则位置L1到L2，并且在过程中将执行动作A，并且R中的所有时钟将被设置为零。 I：L→ CCC是一个将不变量与每个位置相关联的函数非正式地说，自动机只能在不变量为真的情况下保持在给定位置因此，不变量被用来对紧急性进行建模：当相应的位置不变量为假时，必须立即进行当我们讨论TA的语义时，我们将精确地解释不变量，但是，重要的是要理解守卫和不变量之间的在这方面，我们可以区分可能和必须的时机。警卫表示可能的行为，即。他们说，过渡是可能的，或者换句话说，可以采取过渡。然而，警卫不能相反，不变量定义了必须行为。这个必须方面对应于紧急性，因为另一种表达是当不变式到期时，必须立即进行传出转换。语义在三元组（S，s0，n）的转移系统上对时间自动机进行了语义解释，其中S<$L×V是一个状态集，s0∈S是一个起始状态;H. Bowman等人/理论计算机科学电子笔记139（2005）2529−−−−−→i/i，j/j]−−−−−−−−−→ ||u[ i / i]|u [i/i]其中Lab=A <$R+.因此，过渡可以是两种类型之一：离散过渡，例如，（s1，a，s2），其中a∈A和时间跃迁，例如（s1，d，s2），其中d∈R+，且d的通过一个d表示时间单位转换写为：s1=s2，相应地s1=s2。对于一个时钟值v∈VC和一个延迟d，v+d是时钟值，使得对于所有c∈C，（v+d）（c）=v（c）+d。对于重置集r，我们使用r（v）来表示时钟估值vJ，使得当c∈r时vJ（c）= 0，否则vJ（c）=v（c）。v0是将所有时钟赋值为零的时钟赋值。时间自动机A=（L，10，T，I，C）的语义是一个变迁系统，（S，s0，ε），其中S={SJ∈L×VCy| s ∈ S，y ∈ Lab.s=sJ}{[l0，v0]}是可达状态的集合，s0=[l0，v0]，并且由两个定义推理规则（I（l0）（v0）必须成立）：l−−a，−g，→r lJg（v）I（lJ）（r（v））dJ≤d。 I（l）（v + dJ）[l，v]=a [LJ，r（v）][l，v]=10d [l，v+d]第一个规则给出了对不变量的解释，如果相应的不变量为假，则不能输入位置这种解释，通常被称为强不变解释，是UPPAAL所采用的解释，也是我们在第4节中提出的非紧急性质所假设的解释。并联组成我们假设我们的系统被描述为一个时间自动机网络这些由表示为，|A=|[1]，.，其中，A [i]是一个时间自动机。此外，我们让u，uJ等在集合上值域位置向量的U，记为，u [1]，.，[n]不，不，不。我们使用如下的替换符号：u[1]，. ，u[j]，... ，u[n]n[u[j]J/u[j]]=n [u[1]，. ，u[j−1]、u[j]J、u[j+1]、. ，u[n]n，并且我们将[u[j]J/u[j]]写为[jJ/j]和du[iJ/i1]. [iJ/im]如u[i]/i1，...，IJ1m/im]。1m如果n =i（1 ≤i≤n）. A [i] =（Li，Li，0，Ti，Ii，Ci）则乘积自动机，其特征在于|[1]，.， A [n]由下式给出：（L，l0，T，I，C），其中L={|u|u∈L1×. ×Ln} ， l0 = |1 ， 0 ， ... ， 1.1.1. 2. 3. 4. 5. 6. 7. 8. 10. 11. 12. 11|[1]，.，u [n] n）= I1（u [1]）n. n（u [n]）和C = C1n. C.u[i]−−x−？，g−i−，r→iu[i]Ju[j]x！，gj，rju[j]Ju[i]−−x，−g，→ru[i]Jx∈CA|ux,gi∧gj,ri∪rju[J] Jx，g，rJ30H. Bowman等人/理论计算机科学电子笔记139（2005）25[5]虽然我们的符号略有不同，但我们的网络可以与UPPAAL中使用的过程网络相关H. Bowman等人/理论计算机科学电子笔记139（2005）2531X⇒⇒anDnn其中1 ≤i/= j≤|u|. 注意，我们写x≤k/=r≤y代替x≤k≤y<$x≤r≤y<$k/=r。3死锁的分类从广义上讲，死锁是指系统无法继续运行的状态。我们希望系统能够永远运行，因此死锁可以被视为错误情况。在非定时系统中，死锁是系统永远无法执行操作的然而，在时间自动机中，转换的范围已经扩大到时间传递和离散转换（动作）。因此，在这种情况下，违反进步要求的方式可能各不相同。因此，定时自动机中的死锁可以是不同的类型。我们将重点介绍这些不同的类型，此外，作为对最新技术水平的评估，我们还将考虑UPPAAL提供的检查此类锁的方法在给出各种类型的死锁的正式定义之前，我们简要回顾一下我们将使用的术语，这在很大程度上继承自[3，9]。给定s=[l，v]，我们将写s+d而不是[l，v+d]。同样，我们将s=写成de-注：s=xsJ.从状态s0开始的A∈TAs的一个游程是有限的或无限的序列：ρ=sd00==s0+d的10==s1. Sdn−1n−1=n−1 +dn−1==sn==0.. . 、其中，i ≤ n。 si∈ S，ai∈ A;<$0 ≤ i ≤ n − 1。 di∈ R+0; dn∈ R+0<${∞}∞（sn==0）记s∈R+0。s=t）.注意，无限次运行包含无限次。有限数量的离散转换（即动作）。设Tr（A）表示定义函数delay（ρ），ρ∈Tr（A）为ρ中所有延迟di的和。如果delay（ρ）=∞，我们说ρ是发散游程。一般来说，动作锁是不能执行离散转换的状态，而时间锁是时间不能超过某个点的状态。 形式上，给定A∈TA，状态s= [l，v]是动作锁，如果d∈R+0。 [l，v+d]∈S<$$a∈A. [l，v+d]=λa。那么，你是怎么做到的系统在位置L空闲，不能执行任何动作然而，一个国家是一个时间锁，如果没有发散运行ρ∈Tr（A）开始于s。一个时间自动机A是无动作锁（无时间锁）的，如果它的可达状态都不是动作锁（时间锁）。锁和 时 间 锁 可 以 进 一 步 定 义 为 pure-actionlocks 、 time-actionlocks 或 zeno-timelocks（或纯时间锁）。定义3.1（纯动作锁）纯动作锁是系统的状态，它不能执行任何离散的转换，但仍然可以任意地传递时间。给定A∈TA，状态s= [l，v]是纯动作锁，如果R+0。 [l，v+d]∈S<$$a∈A. [l，v+d]=λa。32H. Bowman等人/理论计算机科学电子笔记139（2005）25图1a示出了具有纯动作锁的定时自动机的示例：一旦自动机到达位置S0，则不启用动作，但是不阻止时间流逝。定义3.2（Time-actionlock）Time-actionlock是既不能执行离散转换也不能执行时间转换的状态。给定A∈T A，一个状态s是一个时间-ationlock，如果$a∈A， d∈R+。s=as=d。时间动作锁的一个例子如图1b所示。上层自动机必须执行一个动作a！在超过5个时间单位之前，而底部的一个只能执行a？5个单位通过后然后，系统在经过5个时间单位后立即进入时间动作锁定义3.3（零时间锁）给定A∈T A，zeno游程是无限游程ρ∈Tr（A）s. t。延迟（ρ）/=∞。一个状态s是zeno-时间锁，如果a）至少有一个从s开始的无限次运行，b）所有从s开始的无限次运行都是zeno，c）没有从ss. t开始的运行ρJ∈Tr（Adelay（ρJ）=∞6.当系统进入零时间锁时，仍然可以执行转换（可以是离散或时间转换），但时间不能超过某个点。这模拟了系统在有限时间段内执行有限数量转换的情况图1c表示零时间锁，其中在超过5个时间单位之前，转换a必须执行无限次。S0 x=10S0 x=5一个！S1S0 x=5一Bx>5a？一S1P0P1Ca）、b）、c）、Fig. 1.死锁的分类讨论提出我们的分类的一个原因是，我们相信不同类型的死锁会带来不同类型的问题，因此应该区别对待。首先，尽管在特定规范的上下文中，pure-actionlock可能是组件或系统可能会达到无法执行任何操作的状态，这是完全合理的，只要[6]根据我们对运行的定义，ρ′不一定是无限的。H. Bowman等人/理论计算机科学电子笔记139（2005）2533这样的动作锁不会停止时间。因此，尽管检测纯动作锁的分析工具肯定有价值，但我们不相信有任何基本的理由可以在规范符号的级别上防止动作锁（通过构造）相反，我们强烈认为时间动作锁是违反直觉的。特别地，如前所述，一个组件中的局部“错误”对整个系统具有全局影响，即使系统的其余部分与时间锁定组件没有共同的动作。由于这些特别违反直觉的方面，我们认为应该通过建筑来防止时间动作锁，也就是说，时间自动机模型应该以这样一种方式重新解释，即时间动作锁不会出现。Bowman [3]提出了一种具有截止日期的时间自动机的方法[1]。最后，来看看Zeno-Timelocks。我们在此的立场是，应提供分析方法，以逐个具体检查是否出现零时间锁。我们提倡这种方法的原因主要是务实的，因为目前还不清楚如何改变时间自动机模型，以建设性地防止这种情况。特别是，任何在语义层面上确保每个周期都经过最小时间（比如时间）的机制，都会对规范抽象描述系统的能力施加严格的约束。第4节考虑的正是这样一种检测zeno-timelock的分析方法4Zeno-timelock我们现在提出一种分析方法，以确保zeno-timelock的存在，该方法建立在Tripakis [9]引入的强非zenoness概念的基础上。我们展示了如何Tripakis的结果可以扩展到保证zeno-timelock自由的系统，可能不是强烈的非zeno。特别是，强非zenoness和同步组件之间的关系进行了更详细的分析。此外，新的句法属性，在精神上的强大的非zenoness，也确保zeno-timelock自由。强非zenoness性质，我们在下面回顾，代表了确保zeno-timelock自由的充分但不是必要条件;强非zeno的系统保证不受zeno-timelock的影响，但存在一些系统不受zeno-timelock的影响，但不是强非zeno。定义4.1（强非zenoness）给定A∈T A，A是A中的位置和边的序列，la1，g1，r1La2，g2，r2...an，gn，rn我，0−−−−→ 1−−−−→−−−−−→n7请注意，早期版本的定时CSP确实采用了这种方法。34H. Bowman等人/理论计算机科学电子笔记139（2005）25S.T. l0=ln. A是强非zeno的，如果对每个这样的环都存在一个时钟c∈C，n∈R+且0≤i，j≤ ns.t. (1)c∈ri和（2）c在步骤j中是有界的，即gj<$c > j. 每个满足这些性质的循环也被称为强非zeno。强大的非zenoness保证没有zeno-timelocks，它是由平行组成保存下面的引理4.2形式化了这些结果[9]。引理4.2如果A∈TA是强非zeno的，则Tr（A）不包含zeno时锁。此外，如果A [1]，…，A [n] ∈ TA是强非zeno，则|A也是强非zeno。引理4.2提出了一种静态验证方法;如果系统的所有组件都是强非zeno，或者换句话说，如果每个组件中的每个循环都是强非zeno，则系统没有zeno时间锁。这个结果是由乘积自动机的结构证明的，其中每个循环都是两个不同分量自动机中具有匹配半动作的两个循环的结果（我们称之为同步循环），或者是一个分量自动机中没有半动作的循环（称为完全循环）。由于a）每个组成循环都是强非zeno的，b）强非zeno性仅取决于循环中给定保护中的时钟的存在，并且在循环中的某个点重置，以及c）这些条件在乘积自动机中的结果循环的边缘中保持，则乘积自动机中的每个循环都是强非zeno的。但请注意，组件中的强非zeno循环实际上因此，强非zeno环路和任何其他环路之间的同步也必须被认为是“安全的这可能会对用户产生相当大的影响相反，我们可以将组件集合中的所有同步循环配对，并且对于每一对，只要求一个循环是强非zeno的还要求所有不包含半动作的循环都是强非zeno的，因为这些循环在乘积自动机中被保留，但这种方法的好处仍然是显而易见的。我们已经发现，引理4.2所施加的确保zeno-timelocks不存在的要求可以被这个结果由下面的引理4.3形式化（证明在附录中给出）。引理4.3设HL是中所有同步环对的集合，H. Bowman等人/理论计算机科学电子笔记139（2005）2535A [1]，. ，A [n]，和，分别地，CL是所有完整循环的集合。 如果每对HL中的（至少）一个回路是强非zeno的，并且CL中的所有回路都是强非zeno的，则|A也是强非zeno的，因此没有zeno时间锁。我们现在提出另外两个属性，位置非紧急性和重置非紧急性，它们也在时间自动机语法的级别上工作，并且仅表示succient-only条件。然而，他们可以保证一个系统是免费的zeno-timelock，即使它可能不是强烈的非zeno，这样的zeno-timelock自由系统的语法检测的范围进一步扩大。这种直觉与强非零性的基础是相同的：我们必须证明，对于任何状态s，如果存在一些从s开始的无限次运行，那么它们中至少有一个必须发散（因此s不是零时锁）。现在，根据定义，无限次运行必须遍历某个循环无限次（否则运行不能包含无限次离散转换）。因此，我们只需要确保时间在任何迭代的每次迭代中至少可以经过<$∈R+时间单位，循环（其中，循环被认为是一个常量）。因为这些条件集中在在不变量上，它们覆盖了一些不是强非zeno的安全循环在下面的定义中，我们使用Clocks（I（l））C来表示出现在不变表达式I（l）中的时钟集合（其中l是位置）。定义4.4（位置非紧急性）A∈TA称为位置非紧急性，如果在每个结构循环中有一个位置，其中不变量为真，或者出现在不变量中的每个时钟都没有上限。例如，True和x>1（其中x∈C）可以是两个这样的不变量。从形式上讲，设la1，g1，r1La2，g2，r2an，gn，rn0−→1−→.. . −→ln，s.t. l0=ln是A中的结构环。一称为位置非紧急，如果对于每个这样的结构环，存在0≤i≤n S. t。d∈R+.c∈Clocks（I（li）），v∈VC. （v（c）>dI（li）（v））（注意这个公式对于真不变量是空的，因为Clocks（True）=）。这些循环也称为位置非紧急。定义4.5（重置非紧急）A∈TA称为重置非紧急，如果在每个结构循环中存在一个位置，在该位置不变量中至少有一个时钟具有非零下界，并且该时钟在循环中被重置形式上，让la1，g1，r1La2，g2，r2an，gn，rn0−→1−→.. . −→lns。t. l0=ln，是一个结构在A中循环 A称为重置非紧急的，如果对于每个这样的结构环，存在0≤i≤ns.t。d∈R+，c∈Clocks（I（li）），v∈VC. （v（c）= d<$I（li）（v）<$（vJ∈VC. vJ（c）（t==1）可以写成UPPAAL，以验证系统没有时间锁。然而，这种方法提供了一个充分但非必要的条件：如果公式满足，则系统保证是无时间锁的，但在某些无时间锁的系统中，公式可能不满足公式（t==0）-->（t==1）实际上实现了A[]（（t==0）=>A>（t==1）），它仅H. Bowman等人/理论计算机科学电子笔记139（2005）2537t =1a）、t==1t：=0t =1b）、t==1t：=0真图二. 测试自动机（a）和无时间锁系统（b）如果对于每个（t==0）-状态，在从（t==0）-状态的每个可能的游程中，（t==1）-状态是可达的。但是这个条件太强了;一个有zeno运行但没有时间锁的系统将伪造A[]（（t==0）=>A>（t==1）），因为zeno运行是一条路径，其中（t==1）-状态是不可到达的。图图2B示出了这样的系统。实际上，如果在每个（t==0）-状态处至少存在一个运行开始，其中（t==1）-状态是可达的，则系统是无时间锁的事实证明，这个条件可以用公式A[]（（t==0）=>E>（t==1））表示，但不幸的是，这样的公式不能用UPPAAL来写此外，可达性分析可能由状态爆炸引起，如果系统中出现零时间锁，则证明（t==0）-->（t==1）失败的跟踪可能没有足够的意义来发现时间锁的原因。我们声称，在许多情况下，我们的工具将更方便地帮助用户找到zeno-timelocks。与测试自动机一样，我们的工具实现了一种策略，该策略足以检测系统是否没有zeno-timelocks，但并不一定意味着系统包含zeno-timelocks。然而，与测试自动机策略不同的是，这里的分析是语法性的（因此，它可能比可达性要求低得多），并且它还直接在自动机结构上识别zeno-timelock的潜在原因本节将展示我们的工具如何在协议验证中补充UPPAAL5.1一种零时间锁检查器，该工具接收一个时间自动机规范（作为XML文件）作为输入，并返回一个可能导致zeno-timelock的循环列表。该工具旨在与UPPAAL集成;用户可以利 用 UPPAAL 该 规 范 由 UPPAAL 存 储 为 XML 文 件 ， 可 以 输 入 到 zeno-timelock检查器。基本上，循环检测算法在此规范上执行，以发现所有结构循环。第二阶段确定哪些循环是强非zeno的。然后，循环根据它们的半动作进行匹配;这个阶段返回一个匹配对列表和第二个不包含半动作的循环列表。最后，引理4.3应用于两个列表以返回不安全的对/单循环：如果两个循环都不是强非zeno，则对是不安全的，类似地，非同步循环是不安全的。38H. Bowman等人/理论计算机科学电子笔记139（2005）25如果它不是强非芝诺。5.2CSMA/CD协议CSMA/CD（带冲突检测的载波侦听多路访问）协议广泛应用于以太网，该协议控制共享公共介质的站点之间的数据传输。下面的描述主要来自[8]。希望首先传输帧的站监听介质以确定是否正在进行另一传输如果介质空闲，则站开始传输。否则，站点将继续监听，直到介质空闲，然后立即开始传输。可能发生两个或多个站几乎同时开始发送如果发生这种情况，将发生冲突，来自两次传输的数据将被混淆，无法成功接收如果在传输过程中检测到这样的冲突，则该站发送一个简短的干扰信号（以确保所有站都知道发生了冲突），然后停止传输。发射干扰信号后，电台随机等待一段时间，然后尝试干扰帧。只有当一个以上的站在短时间内（传播延迟的时间段）开始传输时，才会发生冲突如果一个站尝试发送一个帧，并且在数据包的前沿传播到最远站所需的时间内没有冲突，则该帧将不会有冲突，因为所有其他站现在都知道该传输（即，将发现介质繁忙）。其次，检测碰撞所需的时间不大于传播延迟的两倍图3（a-c）显示了UPPAAL中可能的CSMA/CD规范的一部分。在本规范中只考虑了两个站点，站点1（图1）。3a）和2号站（类似于图3模重命名）。站1的主要作用是在检测到冲突的情况下对帧的传输和重传进行介质（图3c）将模拟介质的状态，即是否检测到冲突以及如果发生任何冲突，干扰信号的广播站1和介质都具有从端到端传播延迟（26 μs）或从端到端传播延迟（26μs）导出的或帧传输时间（782μ s.）8 .第八条。我们还包括自动机UpperLayer1（图1）。3b）对使用站中的协议服务的客户端层进行建模（上层2类似）。它只是提供帧到协议层，确认正在进行的传输和成功终止。自动机工作站1在空闲状态下启动，等待上层18 常数符合IEEE 802.3标准（以太网CSMA/CD）H. Bowman等人/理论计算机科学电子笔记139（2005）2539一号站一号！trans1！fin1！x1==782发射空闲Ux1 =782101！send1？x1：=0cd1？101！x1<26x1：=0联系我们busy1！a）、中等繁忙1？y>=261？y：=0有效空闲的102？y：=0end1？y：=0busy2？y>=26end2？y：=0cd1！cd2！01？2002年？下一页1下一页2y 26 y 26y =26y =26y：=0 y：=0cd1！cd2！碰撞c）y =26上层1发送1！trans1？空闲发送b）fin1？站1trans1！发送x1=782||trans1？发送上层1d）、站点1中正在发送1001？y：=0x1 =782空闲的102？y：=0有效cd1？end1？y：=0101！126个<||x1：=0end2？y：=0重试cd1！cd2！01？2002年？发送Next1Next2 y 26 y 26x2 =782 y =26y =26y：=0 y：=0cd1？||cd1!02！26位=26）。40H. Bowman等人/理论计算机科学电子笔记139（2005）25介质在空闲状态下启动，等待站点开始传输（101？/102？）;然后它移动到Active并且时钟y被重置。状态活动表示一个站当前正在使用该介质。在Active中，y表示从站开始其传输起经过的时间。转换繁忙1？/busy2？表示站已经可以确认介质在使用中，因此还不可能进行新的传输。这些转换中的保护y>=26表示，在最坏的情况下，第二站不能在26μs之前确认介质繁忙。(the传播延迟）从第一站开始其传输起已经过去状态冲突表示发生了冲突，并且干扰信号即将到达站。介质从活动状态到碰撞状态经过101？/102？发生在Y 26，即，第二站在它能够确认介质已经在使用之前已经开始发送帧在Collision中，y表示自冲突发生以来经过的时间;请注意，当Medium处于Active时，第二次传输开始时，y会重置（转换组cd 1！-下一个2-cd2！CD2！下一个1-cd 1！以任意顺序对到达站1和站2的干扰信号进行建模。此外，Collision，Next 1/Next 2中的不变量y 26表示干扰信号将在不晚于26μ s到达站点在碰撞之后5.3验证我们将看到包含自动机UpperLayer1（UpperLayer2）如何掩饰协议规范中已经存在的时间动作锁，使其无法被UPPAAL检测到事实上，这种隐藏的时间动作锁导致了我们的工具将帮助识别的zeno-timelock我 们 通 过 检 查 actionlock-freedom 开 始 验 证 ;UPPAAL 发 现 A[]notdeadlock在我们的CSMA/CD规范中是令人满意的。然后，我们使用我们的zeno-checker，它发现一些同步对循环是不安全的，因此可能会导致zeno-timelock。这些不安全环路分别对应于站1和上层1之间的交互（图3d）、站2和上层2之间的交互（未示出）以及站1、站2和介质之间的交互（图3d）。3e）。图3e示出了可能潜在地导致zeno时间锁定的多个循环。我们在下面描述这些循环;我们使用来表示乘积自动机中的状态，其中s1，m和s2分别是Station 1，Medium和Station 2中的状态。R、I、T、A、C、N1和N2分别表示状态NEXT、空闲、发送、活动、冲突、Next1和Next2。同步导致完成动作101、102、cd1和cd2H. Bowman等人/理论计算机科学电子笔记139（2005）2541在相应的半个动作之间。(i)，CD1，，CD2，，CD1，，CD2，(ii) ， R2， R，A，T>， R1， T，C，T>， cd1， R，N2，T>， cd2， R，I，R>(iii) ， CD1， T，A，R>， CD2， T，C，T>， CD2， T，N1，R>， CD1， R，I，R>(iv) ， CD2， R，A，T>， CD1， T，C，T>， CD2， T，N1，R>， CD2， R，I，R>这些循环对应于这样的情况，即站继续过早地重定向它们的帧，因此在每次尝试之后再次碰撞它们被认为是不安全的，因为没有结构性条件确保时间在每次迭代中流逝;即。他们不是强烈的非zeno（注意图。3e时钟被重置，但是没有具有非零下限的保护换句话说，这些环路允许zeno运行对应于没有延迟的冲突之后的重传。然而，复合状态，其不变量为真（因为在空闲和空闲中的不变量为真），包含在每个循环中。 因此，每个循环都满足第4节中给出的位置非紧急性质，因此它们不会导致零时间锁（见引理4.6）。直觉上，每个循环总是存在一些无限执行，它们可以在状态中传递时间。现在我们将把注意力集中在车站1的不安全回路上（图1）。 3 d）;如果trans 1！ 是x1==782处唯一启用的转换。如果是这样的话，那么传输中的不变量将使这种转变变得紧迫，因此它将被无限地采取，而根本没有时间流逝。如果这样的zeno-timelock发生在这个规范中，则actionlock应该发生在transition trans 1！被移除。作为这个结论的一个基本原理，人们必须考虑到，对于一个zeno-timelock涉及trans 1！，这必须是站点1在x1==782处启用的唯一转换。 因此，UPPAAL应该能够检测到一个“隐藏”的actionlock，如果trans 1！从规范中删除。 事实证明确实如此，特别是trans 1！删除，UPPAAL会在结果系统中检测到一个actionlock 这是由于在保护过渡cd1的错误？在Station1中，x1 26（注：[10]突出显示了相同
我的内容管理
展开
