实时Maude：形式化分析实时系统及高性能扩展

理论计算机科学电子笔记174（2007）65-81www.elsevier.com/locate/entcs实时MaudePetterCsabaOélveczkyaanddJos'eMeseguerba奥斯陆大学信息学系b伊利诺伊大学香槟分校摘要本文综述了实时Maude的最新进展。 Real-Time Maude扩展了Maude重写逻辑工具，以支持基于对象的实时系统的形式化规范和分析。它强调规范的易用性和通用性，并支持一系列分析方法，包括符号模拟，无界和时间有界可达性分析以及LTL模型检查。Real-Time Maude可用于指定和分析许多系统，这些系统由于其无界特性，例如无界数据结构或动态对象和消息创建，无法通过当前基于时间/混合自动机的工具进行建模。我们通过总结两个例子来说明这种表现力和普遍性。案例研究：（i）具有无限队列的高级调度算法;以及（ii）最先进的无线传感器网络算法。最后，我们给出了一些（通常很容易检查）条件，以确保Real-TimeMaude系统.在实践中，我们的研究结果意味着实时Maude关键词：形式分析，实时系统，重写逻辑，Maude，面向对象规范，无线传感器网络，完备性1介绍形式化工具的用户一方面面临建模形式的表达性和通用性之间的选择，另一方面也面临可判定和完整分析方法的可用性对于实时系统，基于时间和线性混合自动机的工具，如UPPAAL[13]和HyTech [12]，已经成功地建模和分析了一系列令人印象深刻的系统。然而，虽然它们的限制性规范形式主义确保了有趣的属性是可判定的，但这样的有限控制自动机不能很好地支持具有不同数据类型、通信模型和高级面向对象特性的更大系统的规范。Real-Time Maude [18，20]是一个高性能工具，它扩展了基于重写逻辑的Maude系统[9，10]，以支持实时系统的形式化规范和分析Real-Time Maude强调具体的表现力和易用性，1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.02066P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）65关键属性的算法可判定性。在Real-Time Maude中，系统的数据类型（可能是无界的）由等式规范定义，瞬时转换由重写规则定义，时间流逝由“tick”重写规则定义Real-Time Maude以一种自然的方式支持分布式面向对象实时系统的规范，其灵活的规范形式主义使我们能够轻松地定义不同的通信模型，不同层次的抽象。可执行实时Maude规范。我们的工具提供了广泛的有效分析方法。定时重写可以模拟系统的许多可能的公平并发行为之一。时间广度优先搜索和时间有界线性时序逻辑模型检查可以分析所有行为-相对于 如下面所解释的对密集时间的给定处理-从给定的初始状态向上到一定的时间。 通过将搜索和模型检查限制在行为之上， 在一定的持续时间内，可达状态的集合被限制为可以进行模型检查的有限集合（除非系统表现出病态的芝诺行为）。时域可以是离散的或密集的。时间自动机一般来说，时钟区域的扩展不能在更复杂的系统中实时Maude表达。Real-Time Maude通过选择不同的“时间采样”策略来处理密集时间例如，一种策略允许用户选择以用户指定的时间间隔访问状态;另一种策略允许时间在“有趣”的事情发生之前“尽可能”提前。实时Maude搜索和模型检测算法分析所有行为，直到给定的时间推进策略。这样的分析对于密集时间通常是不完整的因为不能保证采样策略覆盖所有感兴趣的变量，但是，正如我们下面所解释的，在许多实际应用中很容易实现完整性。本文的目标，正如其标题所示，是给实时Maude的最新进展的概述。具体进展已在其他地方单独报告[16，22，23，19]，但没有最新技术水平的概述。本文试图填补这一空白，并提供答案的问题，如：（i）什么是实时Maude好？(ii)它与UPPAAL和HyTech有什么不同？(iii)什么样的逻辑属性可以被决定？以及（iv）Real-Time Maude可以处理哪些其他工具无法处理的应用程序特别是，我们强调表现力，通用性和完整性方面，以及具有挑战性的应用程序。Real-Time Maude的形式主义和分析方法的通用性在第3节中，我们总结了对复杂CASH调度算法 [7]提出的优化的建模和分析。CASH算法具有先进的容量共享功能，可以重用未使用的执行预算。它不能由上述基于自动机的工具建模，因为P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6567未使用资源的队列中的元素的数量可以增长超过任何界限。因此，需要一个无界数据类型来对队列进行建模。在与Marco Caccamo的合作中，第一作者详细说明了该算法，并使用Real-Time Maude对于并发和实时系统的基本模型有一些扩展，增加了对用户可定义数据类型的支持，例如不同类型的着色（定时）Petri网[1]，TE-LOTOS [14]和IF工具集[5]。Real-Time Maude不仅通过规范语言的全面通用性和分析方法的范围，而且还通过其简单性来补充此类系统：使用统一和直观的形式主义来指定数据类型（通过方程）和系统的动态和实时行为（通过重写规则）。此外，委员会认为，与基于固定通信模型的形式主义相反，许多不同的通信模型可以很容易地表达。这后一个功能是重要的建模先进的无线传感器网络算法。这些算法对它们的建模和分析提出了许多挑战，如第4节所述。在与Stian Thorvaldsen的联合工作中，第一作者最近对复杂的OGDC算法进行了建模、模拟和分析，无线传感器网络中的密度控制据我们所知，我们在OGDC上的工作代表了在高级无线传感器网络算法上使用正式工具的第一次尝试。在第4节中，我们展示了如何在OGDC的抽象层次上对无线传感器网络中的通信进行建模，并简要总结了OGDC算法的建模和分析。如上所述，Real-Time Maude提供的基于时间采样的分析方法对于密集时间通常是不完整的，因为不是所有时间都可以被访问，并且不能保证通过采样技术获得的行为覆盖所有可能的行为。在第5节中，我们为典型的面向对象规范给出了一些容易检验的条件，以确保最大时间采样分析是完整的分析方法。 满足这些条件的是一个大而有用的类，即落在类之外的面向对象的规范包括我们的许多大型案例研究，例如AER/NCA主动网络协议套件[21]和OGDC无线传感器网络算法。在实践中，我们的研究结果意味着时间有界LTL公式的时间有界搜索和模型检查是一个大的和有用的非Zeno实时系统类完整的决策过程。2实时MaudeReal-Time Maude定时模块指定了形式为（E，E，φ，IR，TR）的实时重写理论[17]，其中：• （E，E）是一个隶属方程逻辑[15]理论，其中E为签名1，E为一组条件方程和成员关系。 理论（E，E）具体说明了1也就是说，排序是一组排序、子排序和函数符号（或运算符）的声明68P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）65系统的状态空间作为代数数据类型。（E，E）必须包含一个时间排序的规范，对时域（可以是密集的或离散的）进行建模。• φ是一个函数，它将每个函数符号关联到其冻结的2个参数位置[6]。• IR是指定系统的瞬时（即，零时间）局部转换，其中的每一个被写入crl [l]：t=>tJifcond，其中l是标签。这样的规则指定了从t的实例到tJ的对应实例的一步瞬时转换，只要条件成立。重写规则被应用于对方程取E. 3• TR是一组tick（重写）规则，用语法编写crl [l]：{t}=>{tJ}（时间τ） 如果有条件，来模拟系统中的时间流逝。运算符{_}是一个内置的GlobalSystem排序构造器，τ是一个表示重写持续时间的排序时间初始状态必须是类GlobalSystem的基项，并且必须使用规范中的方程可还原为{t}形式的项。然后，滴答规则的形式确保系统所有部分的时间流逝一致在面向对象的定时模块中，类声明C类|att1：s1，. ，attn：sn.声明一个类C，它的属性att1到attn的排序为s1到sn。 一个给定状态的C类对象被表示为一个，其中O（Oid排序）是对象的标识符，val 1到val n是 属 性 att 1 到 att n 的 当 前 值。消息m是排序Msg的项。我们可以很容易地定义一个消息s（se[20]），它是（m，τ）的一个序列，其中没有一个消息m将中在并发面向对象系统中，状态的形式为{t}，其中t是内置排序Configuration的一个项。4 t通常具有多集结构， 对象、成熟的消息和延迟的消息。配置的多集并集是由并置运算符（空语法）表示，并置运算符被声明为关联和可交换的，因此重写是Maude直接支持的多集重写。并发对象系统的零时间动态行为通过一个瞬时重写规则描述其并发迁移模式而公理化。例如，规则rl [l]：m（0，w）< O：C|a1：x，a2：0'，a 3：z>2重写不能采取 地方 中 冻结论证 位置的 一 功能 符号， 所以 的 一个术语f（t1，. ..，ti，.. .，tn）不会重写为f（t1，. ..，ui，. ..，tn），当ti重写为ui时，如果i∈φ（f）.[3]方程和成员的集合E是一个并集EJ<$A，其中A是一组方程公理，如结合性、交换性和恒等式，E是Church-Rosser模A。在操作上，术语是在应用IR或TR中的任何重写规则之前，简化到其EJ-范式模A4一般来说，运算符{ }被声明为接受排序系统的参数。 在面向对象的模块中，排序Configuration被自动定义为System [20]的子排序。P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6569=>< O：C|a1：x+ w，a2：0'，a 3：z>dly（定义了一个转换族，其中带有参数O和w的消息m被类C的对象O读取和消费。这些转换具有改变对象O的属性a1和发送具有延迟x的新消息m ′（O ′）的属性，如a3，其值不会改变，也不会影响其他属性的下一个状态，不需要在规则中提及。 属性，如a2，其值与下一个状态相关联，但本身不变，可以在规则的右侧省略。因此，上述规则可以表示为：rl [l]：m（0，w）< O：C|a1：x，a2：O '>=>< O：C |a1：x + w>dly（m ' （ O' ） ， x ） .一个面向对象的规范通常只有一个勾选规则，它通常具有以下形式：var C：配置。var T：时间。crl [tick]：如果T = mte（C），则在时间T中{C} =>{δ（C，T）}<[nonexec]。函数δ定义了时间流逝对配置中的对象和消息的影响，函数mte定义了在必须发生某些瞬时动作这些函数根据以下等式分布在配置中的元件vars NeC NeC '：NEConfiguration.var R：时间。等式δ（无，R）=无。等式δ（NeC，NeC'，R）=δ（NeC，R）δ（NeC'，R）。eq mte（无）= INF。等式mte（NeC，NeC'）= min（mte（NeC），mte（NeC'））。函数δ和mte必须通过特定于应用的方程在各个对象上定义。刻度规则以任何小于或等于mte（C）的量T非确定性地提前时间，因此在T被赋予具体值之前是不可执行的（[nonexec]）。我们的工具通过选择不同的“时间采样”策略来设置T的值来处理这些规则例如，在上述形式的刻度规则中，最大时间间隔采样策略将时间提前最大可能的时间间隔mte（C）（除非mte（C）等于无限值INF）。另一种时间采样策略总是通过用户给定的时间增量来提前时间时间不确定性报价规则中的时间差Δ。所有的应用程序，这样的滴答规则，无论是重写，搜索，或模型检查，是使用选定的时间采样策略。这意味着系统中的一些行为，即通过不同地应用报价规则获得的行为，不被分析。定时模块在合理的假设下是可执行的，实时Maude提供了一系列形式分析功能。Real-Time Maude70P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）65持续时间 它是用语法（tfrew t in time <=τ.）其中t是初始状态，τ是时间排序的基项。Real-Time Maude搜索满足这些搜索条件的一个状态的命令具有语法5（tsearch [1] t=>*pattern使得cond< = τ。）Real-TimeMaude还提供了一个不定时的命令来搜索在任何时间内可到达的状态这种搜索虽然不能保证终止，但有时比定时搜索更有效，因为它不必跟踪持续时间。Real-Time Maude扩展了Maude命题也可以被计时，因为它们考虑了所花费的时间。这样，时序逻辑不需要复杂的显式实时语法，但可以表达许多重要的实时属性。关键是全局系统状态有一个全局时钟组件，还可能包含定时器和其他与时间相关的子组件，这些时间方面可以用原子命题来检验。3CASH调度算法的建模与分析日益复杂的调度算法使得它具有挑战性，如果不是不可能的话，使用基于自动机的形式化建模这样的算法。在与Marco Caccamo的联合工作中，我们对最先进的CASH调度算法[7]和该算法的改进进行了建模和分析。这项工作在[16]中报告;在这里我们给出一个概述。CASH算法试图最大化系统性能，同时保证关键任务及时执行。其思想是，当任务实例（或作业）需要少于其分配的执行时间（通常是其平均情况下的执行时间）时，它可以通过将未使用的执行时间放置在未使用预算的全局容量共享（CASH）队列中来使剩余的执行时间可用于其他作业。然后，作业可以重新使用来自未使用的预算的执行时间，该预算具有比作业自己的最后期限更早的最后期限如果作业不需要所有的执行时间，它会将剩余的预算放在CASH队列中。当系统空闲时（即，没有作业准备好执行），则必须根据经过的时间来释放具有最早截止日期的空闲容量。关键的可互换性结果可以是瓜尔-5使用箭头=>+和=>搜索命令！代替=>*，分别搜索在一个或多个步骤中可到达的状态和不能进一步重写的状态。P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6571优先级是每个作业可以在其截止日期之前执行其分配的执行时间（包括其使用的空闲预算），只要服务器的带宽之和小于或等于1。CASH算法的开发人员之一Marco Caccamo希望使用Real-Time Maude来分析CASH算法的潜在优化，其中，当闲置，释放具有最新截止日期的预算。 这样一来，“valuable” resources with earlier deadlines could be reserved for executing jobs 关键的问题是，可验证性结果是否也适用于修改后的调度算法。使用定时重写来模拟CASH算法表明，CASH队列中的备用预算的数量可以增长到超过任何界限。这意味着3.1CASH算法我们已经为所有可能的任务集指定了（两个版本）CASH算法，允许作业在任何时间到达并执行任何非零时间。我们以面向对象的风格指定了该算法，其中每个任务服务器都由类Server的对象建模。详细说明见[16]。在下文中，我们只是给出一个具体说明。我们将备用容量表示为期限：d预算：b，其中d是其相对期限，b是其剩余预算。备用容量的现金队列由项[CASH：c1. c n]，其中c1... Cn是空闲容量的队列。此数据类型的排序和运算符指定如下：对Capability CapacityQueue排序。 subsort容量 Capacity[ctor]. opemptyQueue：-> CapacityQueue [ctor].op：CapacityQueue CapacityQueue -> CapacityQueue[ctor aslogid：emptyQueue]。给现金排序 子排序现金<配置。op'[CASH：_']：CapacityQueue->Cash[ctor].为了说明指定风格，我们提出了以下规则，该规则对新作业（其到达通过将服务器的状态属性从空闲更改为执行或等待来隐式建模）到达任务服务器O时的情况进行建模，而另一个任务服务器OCASH算法基于最早期限优先（EDF）调度，这意味着具有最早期限的作业必须始终执行。因此，取决于是否此新作业的新的相对截止日期（由先前的相对截止日期给出T加上O的周期NZT）在当前执行作业的相对截止时间T72P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6535等待状态并允许Ovars O O'：Oid.vars T T'：Time.var NZT：NzTime.rl[idleToActive]：< O '：服务器|state：executing，timeToDeadline：T'>=>if（T + NZT）T（< O'：服务器|state：waiting>）else-cannot preempt O '; start waiting：（< O'：服务器|>>）的内容菲为了使我们的分析更方便，我们添加了一个常数DEADLINE-MISS和一个规则，该规则将剩余预算大于其相对截止日期的对象重写为DEADLINE-MISS：varSTATE：ServerState。OP DEADLINE-MISS：-> Configuration [ctor].crl [deadlineMiss]：< O：服务器|state：STATE，usedOfBudget：T，timeToDeadline：T '，maxBudget：NZT>=>最后期限-缺失if（NZT-T）> T ' /\（STATE == waiting or STATE == executing）.3.2CASH算法我们分析的主要目的是调查是否有可能达到在当前期限内无法执行剩余预算的状态。由于时域是离散的，我们选择时间采样策略' def 1 '，在每次应用滴答时重写规则 通过这种方式，可以探索所有可能的任务集。 以下项目init2定义了两个服务器的初始状态。 由于它们的带宽之和为34≤1，如果算法正确，则不可能达到错过的截止日期：opinit2：->GlobalSystem。等式初始化2={P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6573[CASH：emptyQueue] AVAILABLE-BISSOR}.我们使用时间有界搜索来检查是否可以从状态init2到达错过的最后期限。模式{DEADLINE-MISSC： Configuration}匹配任何包含常量DEADLINE-MISS的状态，因为变量C：Configuration匹配配置的其余部分在时间12内可到达的状态之间进行有时限搜索，发现错过了最后期限：Maude>（tsearch [1] init2=>* {DEADLINE-MISSC：Configuration}时间<= 12）溶液1C：配置<-. ;TIME_ELAPSED：时间<-12Maude中搜索命令的底层跟踪工具用于显示从状态init2到错过的截止日期的重写步骤序列。同样值得一提的是，对现金流进行了广泛的蒙特卡罗模拟，算法没有发现错过的最后期限[16]，强烈表明这是一个非常微妙的错误，不太可能通过测试或模拟发现4无线传感器网络算法建模与分析无线传感器网络由一组小型、廉价和低功耗的传感器节点组成，这些节点使用无线技术相互通信[3]。最常见的是，它被假定为传感器节点通过广播使用无线电transmittance与无向天线进行通信。传感器节点往往具有有限的电源（由电池提供），几乎不可能更换。先进的无线传感器网络算法对正式工具提出了一系列挑战，包括：(i) 关于时间依赖行为的建模和推理。例如，网络的寿命通常是一个至关重要的目标，在这种情况下，必须对功耗进行建模。此外，无线传感器网络算法可能使用定时器，消息传输可能受到消息延迟等的影响。(ii) 许多算法依赖于空间特征，例如位置、距离、覆盖区域等。(iii) 模拟不同的通信形式对于通过无线电发送的传感器节点，可以广播直接通信的适当模型，其中仅距发送者一定距离内的节点接收具有足够强度的信号。(iv) 无线传感器网络的算法通常包含概率行为。(v) 模拟和分析大量传感器节点随机分布在一个传感区域内的系统74P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）65(vi) 正确性，特别是性能，都是必须分析的关键方面。在Real-Time Maude中，空间特征（挑战（2））可以由用户使用合适的数据类型定义。关于挑战（3），Real-Time Maude我们在本文中展示了如何模拟地理上有界的广播与传输延迟。Real-Time Maude不提供对概率行为的建模和推理的显式支持（挑战（4）和部分（6）），这由Maude的另一个扩展PMaude支持[2]。然而，尽管如此，为了在Real-Time Maude中直接模拟系统，可以使用伪随机数生成器对行为进行对于正确性分析，我们可以通过[22]中解释的非确定性来建模概率行为关于（5），我们可以很容易地定义具有任意给定数量的伪随机散布节点的状态，如[22]所示。最后，如[22，23]所述，可以通过实时Maude分析Jennifer Hou最近向我们提出了无线传感器网络的最佳地理密度控制（OGDC）算法[24]，这是一项具有挑战性的建模和分析任务。OGDC已经在仿真工具ns- 2中进行了仿真，并将其性能与类似算法的性能进行了比较OGDC提出了上述（1）至（6）的所有挑战我们在Real-Time Maude中对OGDC进行了建模、模拟和分析[23]。据我们所知，我们在OGDC上的工作代表了复杂无线传感器网络算法的第一个正式建模和分析。我们能够在Real-Time Maude中完成OGDC开发人员使用ns-2无线扩展执行的所有分析[11]。此外，我们对算法进行了时间有界可达性分析和时序逻辑模型检查。这种分析通常会探索某种状态下的所有可能行为，但在我们的案例中，它们也与用于模拟概率行为的采样技术有关。本文旨在给出一些高层次的想法如何建模无线传感器网络算法。论文[22]更详细地解释了如何在Real-Time Maude中对传感器网络算法进行建模和分析。报告[23]详细描述了OGDC案例研究4.1无线传感器网络在[22]中，我们已经解释了如何对传感器网络的各个方面进行建模。例如，为了模拟概率行为，我们在状态中包含RandomNGen类的对象，它携带用于“采样”概率行为的伪随机生成器的种子在本节中，我们将展示如何建模在OGDC算法的抽象层次上，对无线传感器网络中的通信进行了研究。首先，我们需要确定位置。如果传感器节点位于一个二维空间中，则我们可以将其视为一个平面。你是我的朋友。P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6575使用有理数的内置排序Rat，这样的对可以表示为以下排序位置的项：排序位置。op_._ ：Rat Rat -> Location [ctor].下面的函数定义了两个位置之间距离的平方：op distanceSq：Location Location -> Rat.变量X X ' Y Y'：大鼠。eq距离Sq（X. Y，X'。Y）=（（X-X'）*（X-X'））+（（Y-Y '）*（Y-Y'））。给定一个常数transRange表示传感器节点的传输范围，我们可以检查一个传感器节点是否在另一个传感器节点的传输范围内：vars L L '：Location.op _withinTransRangeOf_：Location Location -> Bool.等式L withinTransRangeOf L <' = distanceSq（L，L'）= transRange * transRange。每个传感器节点都可以适当地表示为一个对象，比如一个名为WSNode的类。无线传感器节点通常没有明确的标识符，但可以通过其位置进行识别。在Real-TimeMaude中，我们通过给子排序声明子排序Location Oid来让对象标识符成为位置<。在下文中，我们对广播进行建模，其中分组必须到达发送方的无线电范围内的所有节点，并且其中传输受到传输延迟Δ的影响。这个想法是发送者l发送一个将来自l的广播m（其中m是消息内容）形成为配置。该广播消息由等式定义为等效于一组单个，对于在L的无线电范围内的节点L j，使用具有延迟Δ的ddd_e_d_e_d消息声明如下：对MsgCont进行排序。-留言内容msg broadcast_from_：MsgCont Location -> Msg.msg msg_from_to_：MsgCont Location Location -> Msg.以下等式可获得所需的等效性：变量C ：配置。var MC：MsgCont.eq {（来自L的广播MC）C}={distributeMsg（L，MC，C）}。distributeMsg的任务是为配置C中的每个传感器对象创建一个寻址消息，该传感器对象在L的传输范围内。运算符{_}的使用使等式能够获取整个状态，以确保系统中所有适当的节点都将获得消息。函数distributeMsg递归地定义在配置中的元素上：6Real-Time Maude还提供了一个内置的浮点数数据类型，以及平方根等函数，但我们更喜欢尽可能保持在有理数范围内。76P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）65op distributeMsg： Location MsgCont Configuration -> Configuration[冻结（3）]。var MSG：Msg.var O：Oid.eq distributeMsg（L，MC，none）=none。eq distributeMsg（L，MC，MSG C）= MSG distributeMsg（L，MC，C）。eq distributeMsg（L，MC，C）= distributeMsg（L，MC，C）.eq distributeMsg（L，MC， C）=< L'：WSNode|>distributeMsg（L，MC，C）（如果L在L'的transRangeOf L'内然后dly（msgMC从L到否则没有Fi）。第一个方程说，将具有内容MC的消息分配给空配置（用none表示）所产生的配置就是空配置。第二个等式表示，将具有内容MC的消息分配到由消息MSG和配置C组成的配置所产生的配置是由MSG和将MC分配到C的结果组成的配置。第三个等式只是说明，可能出于模拟目的而包含的关键的等式是最后一个等式，它说将MC从发送者L分发到由位置L'处的节点和配置C的其余部分组成的配置与递归地如果L也就是说，我们已经将此消息添加到系统中。如果两个节点l和lJ之间的传输延迟是它们之间的距离的函数，比如f（l，lJ），我们只需用f（L，L'）代替Δ在此设置中，从传感器节点l广播消息m由规则建模，该规则以第2节中解释的通常Maude风格将广播消息发送到配置中。在第4.2节中，我们展示了这样一个规则的一个例子。同样，读取消息是通过读取msgm来完成的。. .以通常的Maude风格发送消息。4.2OGDC无线传感器网络算法建模与分析在二维平面中，具有感测范围rs的节点可以感测半径为rs的圆形覆盖区域中的事件。期望的是，活动节点的覆盖区域覆盖要被监视的整个区域（越好.为了延长无线传感器网络的生命周期，通常会部署大量的节点，以便可以有意地将一些节点“置于睡眠状态”以节省功率。OGDC算法[24]是一种最先进的算法，它定期选择可以休眠的节点，同时保持感知区域的覆盖范围。P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6577在OGDC中，网络生命周期被划分为轮。一轮开始于每个节点进入自愿过程，在该过程中，它概率性地选择是否自愿成为起始节点。每个志愿节点都将其backlog timer设置为一个小值。然后，当它的备份定时器到期时，节点变为活动的，并且广播包含节点的位置和随机方向的通电消息（参见下面的规则startingNodePowerOn当节点接收到上电消息时，它检查其整个覆盖区域是否被周围的环境覆盖。活动节点，在这种情况下，节点变得不活动。否则，节点根据节点与最佳位置的接近程度来设置其后退计时器当节点的反向计时器到期时，节点变为活动的并且广播通电消息。当每个节点处于活动或非活动状态时，网络进入稳态阶段当一轮结束时，密度控制过程重新开始下面我们介绍OGDC的Real-Time Maude规范中的11条重写规则之一。如上所述，当节点的备份定时器到期时（即，值为0），并且该节点自愿成为起始节点。节点变为活动状态，并广播包含节点位置和随机方向的通电消息 此操作由以下重写规则建模：varL：位置。varP：NzNat.M：不，我不知道。rl [startingNodePowerOn]：<随机：RandomNGen|种子：M>=><随机：RandomNGen |seed：random（M）>从L广播（powerOnWithDirection randomDirection（M））。如第2节所述，在进行分析之前，必须选择时间采样策略。我们在第5节中展示了我们可以在OGDC中的事件之间“快进”，而不会丢失任何有趣的行为。因此，在我们的分析中，我们使用了最大时间采样策略，它尽可能地提前时间（由mte定义）。在[24]中，Zhang和Hou使用仿真工具ns-2和无线扩展[11]来模拟OGDC并测量活动节点的数量、这些节点提供的覆盖百分比以及整个网络生命周期内系统中的总功率我们在初始状态中添加了一个名为分析消息的新结构，以在每一轮结束时计算状态的适当性能度量。然后，定时重写可以用几百个传感器节点模拟OGDC算法，并可以测量OGDC开发人员使用ns-2测量的所有在我们的模拟中，我们通常会得到比[24]中报告的更多的活动节点在[23]中给出了一个合理的解释，并且基本上意味着，在OGDC算法中，如果在仿真中考虑传输延迟（如在我们的情况下所做的那样），则更多的节点将变得活跃，而不是如果这样做，则更多的节点78P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）65延迟被忽略，这可能是[24]中模拟的情况。由于传输延迟在OGDC算法的定义中起着重要作用，因此在仿真中应考虑到它们。因此，我们的正式模型可以提供一个更合适的模拟设置OGDC比ns-2的无线扩展。我们还对规范进行了模型检查，以探索从初始状态开始的所有行为，相对于我们对概率行为的处理，以找出在最坏的情况下达到稳态阶段需要多长时间，以及在第一轮中是否在该阶段覆盖了整个感知区域。5实时模型前面的部分展示了实时Maude形式主义的表达能力和通用性。这种表现力的代价是，实时Maude分析对于密集时间通常是不完整的，因为时间中的所有时刻都无法访问。 对于离散时间，完整性可以通过穷举随时随地都在拜访这使得广度-第一搜索违反一个invari-一个完整的半决策过程。此外，对于在一定时间内只能达到有限组状态的系统，时间有界LTL模型检验成为一个完整的决策过程。然而，访问所有离散时间通常会导致状态空间爆炸，使许多正式的分析不可行。在最近的工作中，在[19]中详细报道，我们研究了在什么条件下实时Maude的最大时间采样策略产生完整的我们只考虑满足方面的时间公平路径的集合。 （时间不公平路径是一种无限的病态路径，其中总持续时间以某个时间值τ为界，即使在无限多的滴答规则应用中，时间可能已经超过时间τ。此外，我们只考虑没有下一个运算符的LTL公式，因为带有的公式对“口吃”的滴答步骤很敏感例如，如果时间可以在一个时间单位中前进两个时间单位，如果在两个连续的刻度步长中的每一个中，时间通常也可以前进一个时间单位。对于具有第2节中给出的形式的刻度规则的非常有用和通用的面向对象规范类（参见[19]的细节），证明以下五个简单和自然的条件就足够了，对于所有对象t和时间值τ和τJ，以确保LTL模型检查的完整性：(i) mte（δ（t，τ））=mte（t）monusτ，对于所有的τ≤mte（t）. (The函数monus定义为xmonusy=x−y，如果x≥y，否则为0。这一要求表明，如果时间可以在一个对象（状态）t上最多前进时间mte（t），并且该对象在时间上前进的量为τ≤mte（t），那么时间可以使结果对象（的状态）δ（t，τ）最多前进mte（t）monusτ。[7]我们称一个分析方法是完备的，如果使用该方法找不到反例的事实意味着对于所讨论的分析来说不可能存在反例P.C. 奥尔韦茨基Meseguer/Electronic Notes in Theoretical Computer Science 174（2007）6579(ii) δ（t，0）=t.也就是说，对象的状态不应该由于时间“前进”时间0而改变(iii) δ（δ（t，τ），τJ）=δ（t，τ+τJ），其中τ+τJ≤mte（t）.也就是说，如果时间先以时间τ前进，然后以τJ前进，那么这应该具有与时间一步前进τ+τJ相同的效果(iv) 对于瞬时重写规则的左手侧的每个基实例σ（l），mte（σ这个要求是说，在启用瞬时规则的状态下，时间不应该提前（超过0）(v) 对于要分析的属性中的每个原子命题（或