实时Maude：重写逻辑下的实时系统模拟和分析工具

理论计算机科学电子笔记36（2000）网址：http://www.elsevier.nl/locate/entcs/volume36.html22页Real-Time Maude：一个模拟和分析实时和混合系统的工具1彼得·萨巴·奥勒·韦茨基和乔·塞·梅塞格尔计算机科学实验室Menlo Park，CA 94025，美国S. A.电子邮件：{peter，meseguer}@ csl.sri.com摘要重写逻辑可用于在各种时间模型（包括离散和密集时间模型）下指定广泛的实时和混合系统。 实时Maude工具建立在Maude重写逻辑语言之上，支持在定时模块和定时面向对象模块中指定实时和混合系统，这些模块被转换为等效的Maude模块。 然后，该工具支持在几种重写模式下执行这些规范，对应于不同的提前时间标准。除了在给定的重写模式下默认执行的系统模拟之外，该工具还具有执行策略和命令库，可以在给定的重写模式和搜索范围内从初始状态搜索所有可能的计算，以部分地模型检查所需的属性，包括在一类线性时间定时时序逻辑公式中可表达的属性。本文讨论了该工具的理论基础，它的专用语言，以及它的评估和搜索策略库。用户可以添加新的正式分析策略库，如调度案例研究所示。我们还总结了我们的应用经验和未来计划。1介绍在许多反应式和分布式系统中，实时性对其设计和正确性至关重要因此，如何在重写逻辑的语义框架中最好地指定、分析和证明具有实时特性的系统是一个重要的问题。这个问题已经由几位作者从两个角度进行了研究一方面，1 由DARPA通过罗马实验室合同F30602-C-0312提供支持，由O.海军研究合同N 00014 -99-C-0198和国家科学基金会资助CCR-9900334。2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。OÜLVECZKY和MESEGUER2重写逻辑的一个扩展称为定时重写逻辑已被研究，并已被应用到一些例子和specification语言[？、、怎么样？、、怎么样？].另一方面，我们一直在研究如何直接在重写逻辑中表达实时和混合系统规范。、、怎么样？].除了能够证明广泛的已知实时系统模型，以及离散或密集的时间值，可以在重写逻辑中以直接的方式自然地表达之外，我们的方法的一个重要优点是可以使用重写逻辑的现有实现来执行和分析实时规范。由于一些技术上的微妙之处，这似乎很难为定时重写逻辑的替代，虽然映射到我们的框架确实存在[？].Real-TimeMaude工具通过使用Maude引擎作为其底层执行机制来利用此可执行性属性。该工具的规范语言直接支持实时方面，在定时模块和定时面向对象模块中具有特殊的语法特征。在理论层面上，这些句法特征支持实时重写理论的具体化。这些都是重写理论，其中一些规则提前了全局系统的时间，每个都有一个相关的持续时间表达式。有趣的是，通过一个简单的理论转换，每个实时重写理论可以转换为一个普通的重写理论，然后可以在Maude中执行。此转换由Real-Time Maude在内部执行。实时规范的可执行性和分析提出了该工具必须解决的新首先，时间的推进通常是不确定的。这反映在时间推进重写规则本身中，这些规则通常在其右侧和/或其条件中具有一个或多个新变量。第二种通常发生的情况是，一些时间关键的规则是急切的，并且必须立即且无延迟地执行，而其他规则是惰性的，并且应当仅在没有启用急切规则时执行 Real-Time Maude工具通过为用户提供不同形式的默认执行和形式分析的执行策略库来支持实时规范的执行和分析，直接解决刚才提到的非确定性和渴望/懒惰需求，并支持时态逻辑属性的模型检查。此外，由于在Maude中可以通过反射轻松定义新策略，因此该工具可以由用户轻松扩展，用户可以定义新的特定于应用程序的策略来执行其他形式的分析。2实时重写理论本节回顾了[？]中给出的实时重写理论的定义。].实时重写理论用于描述重写逻辑中的实时和混合规则分为计时规则（模拟系统上的时间流逝）和OÜLVECZKY和MESEGUER3≤−R{}→{}−→瞬时规则，即对瞬时变化进行建模，并假设其时间为零。为了确保时间在状态的所有部分均匀地前进，我们引入了一个新的排序系统，没有子排序，以及一个免费的编译器：状态系统的预期含义是，不表示所述整个系统处于状态T。然后，通过全局状态总是具有形式{t}来确保均匀的时间流逝，并且每个滴答规则具有形式{t}−→{tJ}。我们在[？尽管通过使用实时重写理论使持续时间信息显式化来突出系统的实时方面是有用的，但是通过以保留所有预期属性的方式向全局状态添加显式时钟，可以将这种理论简化为普通重写理论。时间被抽象地建模为一个交换幺半群（Time，+，0），带有额外的运算符，如<，和。（根据Maude理论，时间[？]. 这个理论可以用更多的公理来扩展，以公理化线性时域和/或向时域添加无限元素。定义2.1（[？]）实时重写理论Rφ，τ是元组（R，φ，τ），其中R=（R，E，L，R）是重写理论，使得：• φ是一个方程理论态射φ：TIME→（E，E），• 时域是泛函的;也就是说，只要α：r rJ是中的重写证明，并且r是φ（Time）类的项，则r=rJ并且α等价于恒等式证明r，• （E，E）包含一个我们通常称为State的指定排序和一个没有子排序或子排序且只有一个算子{}的特定排序System：State → System，它不满足非平凡方程;此外，对于任何f：s1. . 如果sn→sin，则排序系统不会在s1， . ，sn;• τ是项τ1（x1，...，x n）到R中的每个重写规则，（t） l：u（x1， . ，xn）−→u J（x1， . ，xn），如果C（x1， . . ，xn）其中u和uJ是排序系统的项。 当τ1（x1，...，x n）/= φ（0），上述规则（†）写成l：u（x，.，X）τ1（x1，.，x n）uJ（x，.，X）如果C（x，.，x）。1n−→ 1n否则，规则（†）保持未修饰。我们将分别为φ（Time）、φ（0）和φ（+）写Time我们称形式为（†）的规则为全局规则。如果全局规则l的持续时间τl（x1，.，x n）对于其变量的某些实例不同于0，并且在其他情况下是瞬时规则。不具有（†）形式的规则称为OÜLVECZKY和MESEGUER4−→R{ }−→{ }⟨⟩φ，τR⟨ ⟩→−→−→R⟨ ⟩ −→ ⟨⟩局部规则，因为它们不作用于整个系统，而仅作用于某些系统组件。局部规则总是被看作是零时间的瞬时规则重写证明α的总时间消耗τ（α）：ttJof sort系统定义在[？]作为在α中的每个报价规则应用中经过的时间的总和。给定一个实时重写理论R，计算要么是一个不可扩展的序列t0−→t1−→··−→tn（也就是说，t n不能被进一步重写），要么是一个无限序列t0−→ t1−→···的一步R-重写t it i+1，所有t i基项，从给定的初始项t0开始，sort系统应该注意的是，由于我们明确地（通过重写规则）对时间流逝进行建模，因此不需要通常要求计算时间的流逝完全取决于指定的时间--我们允许终止计算和总时间有限的无限计算。通过在状态中加入一个时钟，实时理论（，φ，τ）可以转化为普通的重写理论，而不会丢失定时信息。在这样的时钟系统中的状态具有t，r的形式，其中t是全局状态 的值，而r是一个排序时间的值，直观地说，如果在初始状态下时钟的值为0，那么它应该表示计算中经过的总时间从实时重写理论（R，φ，τ）到它的时钟版本RC如下：• 我们添加一个新的排序ClockedSystem和一个新的操作符：SystemTimeClockedSystem;• 瞬时（0次）重写规则保持不变;• eaC h规则l：u（x1， . ，xn）u J（x1， . ，xn），如果C（x1， . . ，xn）in ofsort制度被规则所l C：Xu（x1，.，x n），x r− →u（x1，.，x n），x r+ τl（x1，...，x n）如果C（x1，.，其中xr是排序时间的新鲜变量。它显示在[？]如果α：tt J是实时重写证明重写理论（，φ，τ），具有t，t J排序系统的基项，则对于时域中的每个值r，存在α到重写证明α J的唯一提升：t，rtJ，rJ在变换理论中，RJ=r+τ（α），并且变换理论中的任何αJ都是α的提升.2.1懒惰的规则在实时系统中，一些动作是时间关键的，这意味着当对应于这样的动作的规则被启用时，时间不应该流逝。与显式计算每个时间关键规则的使能条件不同，使用内部重写策略的重写逻辑概念[？] 、、怎么样？]，其执行是很好的支持莫德OÜLVECZKY和MESEGUER5→→→∗相关特征，以使用简单的策略来处理这些使能性和优先级方面其思想是将实时重写理论中的规则分为渴望规则和懒惰规则，并通过要求渴望规则的应用优先于懒惰规则的应用来限制可能的重写。也就是说，容许重写的集合是那些重写α：t−→tJ其中顺序地应用惰性规则，并且此外，仅当没有启用急切规则时才应用惰性规则2.2重写逻辑在[？]，我们已经展示了各种著名的实时和混合系统模型如何自然地被视为实时重写的特殊情况处理的模型包括定时[？]和混合自动机[？]，定时和相变系统[？[1]，timed Petri nets（见e. G. [怎么样？、、怎么样？]）和面向对象的实时系统。此外，Kosiuczenko和Wirsing的定时重写逻辑可以映射到我们的框架[？].我们简要地总结了一些技术，这些技术将在5.1节的案例研究中使用，用于指定面向对象的实时系统，其中对象只有功能属性;这样的规范有一个排序配置，其元素是消息和对象的多集。在这样的系统中，无限数量的对象可以由时间的流逝来确定，和/或可以由在滴答步骤中流逝的最大时间因此，使用函数δ：配置时间配置和mte：配置时间分别定义对象和消息的配置上的时间提前效应以及配置的最大然而，我们在[？]，函数δ的引入很容易导致缺乏连贯性[？、、怎么样？、、怎么样？在重写理论中，这直观地对应于具有“不合时宜”重写的可能性此外，排序项Configuration连同函数mte：ConfigurationTime的重写可能在时域中引入不期望的非平凡重写解决这些潜在问题的一种方法是只重写排序系统但是，这种解决方案会丢失并发性。在[？[1]的方法是使用特殊的Tokens形式的Tokens，并使扩展的配置 成 为 Tokens 和 Configuration 的 supersort TokenConf 中 的 一 个项，由原始配置的多集并集和tokens的多集并集组成。tick规则的形式如下（） tick：{Tt}−→r{Tδ（t，r）}如果C和r≤mte（t），对于T，一个排序令牌的变量，和t排序配置的术语。每个局部规则都有形式l：t−→· · ·tJ，如果C。OÜLVECZKY和MESEGUER6→R/一致性w.r.t.符号δ现在是毫无问题的，因为局部规则左侧的每个实例都具有最小排序TokenConf，因此不能是δ的参数。这也适用于运算符mte：ConfigurationTime，因此不会在时域中引入非平凡重写。3实时Maude质量标准Real-Time Maude工具是Full Maude的扩展，支持实时重写理论的规范，执行和形式化分析实时重写理论由定时模块和面向对象的定时模块具体化。 该工具将定时模块转换为一对，由一个（非定时）Maude模块和模块中惰性规则的一组标签组成。如图1所示，该工具可用于以三种不同的方式执行和分析实时重写理论，即：（i）通过在底层Maude解释器中执行规范;（ii）通过使用特定于工具的策略库;以及（iii）使用特定于应用程序的用户定义策略。Maude的默认解释器的第一次使用（i）对于大多数实时规范来说是不令人满意的因此，Real-Time Maude提供了一个专门为执行和分析实时规范而设计的重写策略在这样一个库中的策略是以响应的方式执行的，作为Maude的META-LEVEL模块的扩展此外，Real-Time Maude工具的用户可以在扩展META-LEVEL（或TIMED-META-LEVEL，它扩展了META-LEVEL，具有用于实时规范的有用功能）的其他模块中编写自己的应用程序特定策略，并可以在工具库中输入策略3.1实时模型在该工具中，实时重写理论（，φ，τ）被指定为用户级的定时模块，对于定时系统模块，将模块体封装在关键字tmod和endtm之间，对于面向对象的定时模块，将模块体封装在关键字tomod和endtom之间 为了说明不可执行的属性，实时Maude还允许用户通过分别使用关键字tth和endtth以及toth和endtoth来指定抽象的Full Maude理论和面向对象理论的实时扩展。一个时间规则l：t−→tJ，如果C，其中t，tJ项为sortSystem且τl= 0，则用语法crl[l]：t => tJin timeτlifC.对于无条件规则的情况，使用类似的语法 我们还可以通过在rl或crl前面放置关键字lazy来指定（瞬时或tick）规则为lazy。没有给出来自理论TIME的方程理论态射φOÜLVECZKY和MESEGUER7≤实时重写理论实时Maude符号模拟全莫德注释重写逻辑理论执行结果、痕迹形式化分析实时系统针对具体应用的战略执行结果、跟踪错误和分析结果错误和分析结果Fig. 1. 实时Maude工具的架构。明确在规范层面。相反，默认情况下，任何定时模块都会自动导入功能模块TIMED-PRELUDE，其中包括以下声明：操作零：->时间。op _plus_：时间时间->时间[assumption prec 33 gather（E e）]。op _monus_：时间时间->时间[prec 33 gather（E e）]。ops _le_ _lt__ge__gt_：时间时间->布尔值[prec 37]。var RR'：时间。等式R+零= R。等式RleR' = R lt R'或R == R'。等式Rge R' = R' le R.等式R>R' = R' lt R.态射φ然后隐式地将Time映射到Time，0映射到zero，+映射到_plus_，映射到_le_，等等。事实上，用户可以完全自由地指定时间值的数据类型-可以是离散的或密集的-通过：(i) 导入满足TIME理论的时间值的特定数据类型，并进行排序，比如这些值的TimeValues(ii) 声明一个包含TimeValues System。因此，状态的排序应始终声明为排序State的子排序。3.1.1模块操作由于Real-Time Maude扩展了Full Maude [？]，Full Maude提供的模块上的所有常规操作也在Real-Time Maude中得到支持，但有以下限制：• 一个模块导入了一个定时模块或理论，或者有一个定时理论作为参数，它本身必须被声明为一个定时模块或理论。2• 任何模块都不应该同时包含具有相同标签的eager和lazy规则然而，所有模块的数据库可能包含具有相同标签但属于不同模块的渴望和懒惰规则。• 一个实际的参数不应该引入相应的形式参数理论中没有提到的惰性规则33.1.2面向对象的定时模块定时面向对象模块扩展了面向对象和定时模块，为面向对象的实时系统提供支持特别地，如2.2节所解释的，面向对象的定时模块包括排序Tokens和TokenConf的指定。此外，由于与非定时的面向对象系统相反，δ和mte等函数以及tick规则将遵守全局配置，因此拥有更丰富的配置排序结构是有用的。因此，定时面向对象模块还包括MsgConf、NEMsgConf、ObjConf、NEObjConf和NEConfiguration排序，分别表示消息的多集、消息的非空多集、对象的多集、对象的非空多集和非空配置。子排序声明TokenConfClockedSystem。var R R '：时间。var CS：ClockedSystem.等式CS in time R in time R ' = C S i n t i m e （ R + R ' ） 。转换后的规则保持不变，但当然，原始规则中的intimer语法现在被解释为排序系统上的时间操作。可以证明该平移等价于第2节中给出的平移，即t在时间r中重写为tJ在时间rJ中当且仅当t，r在该平移中重写为tJ，rJ我们发现目前的翻译更方便，因为它更简单（实际上是同一性）。此外，通过这种方式，我们不需要找到新的变量来转换定时规则。(iii) 模块TIMED-META-LEVEL扩展了模块META-LEVEL，其中包含下一节中描述的实时规范策略库，包括元应用和元重写函数的定时版本以及搜索策略。在Full Maude中，导入META-LEVEL[M1，...，M n]，用于模块名称M1，...，Mn，导致Full Maude添加到META-LEVEL常数M1，...，其中，n为n，n为n的值。OÜLVECZKY和MESEGUER10模 块 M1 ， ... ， Mn. 以 相 同 的 方 式 ， 模 块 可 以 导 入 TIMED-META-LEVEL[M1，...，M n]，其导入模块TIMED-META-LEVEL并分配模块M1，.，M n与常数M1，...，Mn.为了完全定义一个定时模块，我们还需要访问模块的惰性规则因此，对于作为TIMED-META-LEVEL的参数出现的每个模块名称M引入一个常量lazyLabels-MJ，其中MJ是M的总而言之，一份声明包括时间元级别[M1，. . . ，Mn]。扩展为：包括元级[M1，. . . ，Mn]。包括时间元电平。ops lazyLabels-M1′. lazyLabels-Mn′：-> QidSet. eqlazyLabels-M1′=“ 模 块 M 1 的 l a z y l a b e l s ”.....eq lazyLabels-Mn′=''lazy labels of module M n ''.部分（i）和（ii）仅在定时模块上执行，最后一个在所有模块上执行。4执行和分析实时Maude规范我们的工具将实时规范转换为普通的Full Maude模块，然后可以使用Maude的默认执行策略执行然而，对于许多这些转换的模块，Maude• 为了模拟具有连续时域的系统，滴答规则通常具有以下形式：crl[tick]：{t}=>{tJ（x）}intimexifxletJJandC（t）.其中t的变量JJ包含在t的变量中，而变量x不出现在t中。直观地，tJJ计算允许的最大时间流逝以确保时间关键动作的及时性，并且条件xletJJ确保时间流逝可以暂时停止以用于非时间关键规则的可能应用（即，对可能在某种程度上“任意”发生的动作建模的规则Maude• 默认的解释器没有考虑到渴望和懒惰的规则。• 与其通过执行重写的次数来测量和控制执行，通常更有用的是通过重写证明中从初始项t0开始经过的总时间τ（α）来控制它：t0−→t。OÜLVECZKY和MESEGUER11为了解决这些问题，该工具以不同的基本模式执行报价规则，这些基本模式确定如何应用其持续时间项是未出现在规则左侧的变量的报价规则。这些以及一些用于优化规则应用的其他模式在第4.1节中进行了描述在4.2节和4.3节中给出了基于这些模式的标准执行策略和一些搜索策略本节中的策略将按照描述的方式工作，只有tick规则可以在其右侧或其条件中引入新变量。4.1重写模式一步重写的模式用于指示在由规则中的新变量表示的情况下如何实例化时间增加该工具目前支持以下三种不同的基本模式，用于确定报价规则应用程序中的时间增加：默认，最大可能时间增加w.r.t.每一次匹配刻度规则的左侧，以及最大可能的时间增加w.r.t.规则的所有匹配项所有这些模式都有时间限制和用户给定的默认时间增加值。出于优化目的，我们在下面描述了两种优化模式，它们不涉及非确定性报价规则中的时间增加。在我们的工具中，将时间增加0的报价规则应用程序被认为等同于无法执行重写。基本模式描述了以下策略，用于应用久期为新变量的报价规则• 在默认时间增加模式中，新的时间变量是用用户给定的默认时间增加值实例化的，该值必须是不同于零的基础项。• 在最大可能的时间内增加w.r.t. 在每个匹配模式中，该工具为每个匹配找到使条件成立的新变量的所有可能值的集合的表示。为了具有可能的唯一最大时间值，时域被假设为线性的，即，它满足[？]. x的值的集合可以用一组有限长的区间（t op x op tJ）或无限长的区间（t op x）来表示，其中op是le或lt。当最伟大的这些区间是右闭的，即，形式为t op xletJ，则tJ为被选择为实例化新变量的最大时间值;否则，必须使用某个给定的该工具仅处理具有一个新变量x的条件，并且其中条件是无x项和不等式以及形式为tletJ、tlttJ、tgttJ、tgetJ和t==tJ的等式的布尔组合，其中t或tJ不包含新变量x，如果t（或tJ）包含x，则它具有x仅出现一次，此外，除了加号和monus之外，x不嵌入函数符号中。OÜLVECZKY和MESEGUER12−→∗‡• 而不是找到最大可能的时间增加， 匹配数k，最大时间增加w.r.t. 所有匹配模式实例化具有最大时间增加量的最大值的新变量，对于规则的左侧，n个成功匹配中的每一个都是n，这三种基本策略可以通过不同的方式进行修改。例如，有时（例如在实时时间属性的模型检查中）让时间前进到某个时间r是有用的，即使基本策略允许时间前进超过时间r而不会在时间r处“停止”。因此，基本重写模式可以通过时间限制r来限定，如果可能的话，时间限制r将滴答规则的应用修改为在时间r停止，在下面的例子中：设e为差r−。τ（α）b在时限之间r和重写证明中的总时间τ（α）：t0t导致 当前状态T。然后，如果时间增量小于通过应用基本模式找到的时间增量，则持续时间变量被实例化为：- 是的如果值为的应用程序失败--或者因为为0，或者因为将时间变量实例化为不满足刻度规则的条件--则使用J实例化duration变量。以下两种优化模式不会影响时间的增加：• 全局模式允许用户指定模块中规则的所有左侧都是排序系统的术语。添加此模式大大加快了搜索过程，因为该工具不需要在正在重写的状态的所有子项中搜索重写• tokenOO模式涉及带有标记“X”的面向对象系统形式为{TOKCF}−→r{TOKδ（CF，r）}的时间规则（对于TOK和排序令牌和配置）的CF变量导致不明确的指定。这是因为排序信息不能在关联交换匹配过程的早期注入，因此匹配算法首先生成可能是指数数量的潜在匹配，其中一个是有序的为了克服这个问题，当使用tokenOO模式时，在应用tick规则之前，用状态的（最外层）中的tokens的数量来实例化形式（）的tick规则中的sortTokens变量4.2基本重写策略基本的定时策略由Real-TimeMaude命令给出（trew [n]tmodemodedti在时间限制内停 止。）和（trew-in [n]moduleName：t mode modedti超时限制。）其中：• n是（一步）重写的最大次数（没有限制）。OÜLVECZKY和MESEGUER13−→如果n= 0，则重写次数）• t是要重写的术语（排序系统）;• mode是重写模式，其是d、m、ma、gd、gm、gma、tokend、tokenm或tokenma中的一个，其中d表示基本默认时间增加模式，m表示最大时间增加w.r. t。每次比赛，ma最大时间增加w.r.t. 所有匹配，并且其中在这些中的任何一个前面的g指示使用全局模式，其中所有规则重写排序系统的项，并且其中在基本模式前面的token指示使用tokenOO模式，其实例化形式为（tokens）的规则中的Tokens变量;• 是默认的时间增加值;• limit表示重写证明α中的总时间流逝τ（α）的极限：tJ由策略执行，并且可以是ler、ltr或无时间限制，对于某些基本项r;• moduleName是应该在其中进行重写的模块的名称这些命令以公平、自顶向下的方式应用规则如果limit是ler的形式，那么给定的模式就被这个时间限制所限定如果下一次应用将使重写校样中的总时间流逝达到（在限制为ltr的形式的情况下）或超过时间限制r（在限制为ler的情况下），则重写的应用结束。4.3搜索策略该工具提供了一些命令来进一步分析实时规范，通过探索初始状态中的不仅仅一个，而是许多可能的行为对于密集时间域，在实践中，由于时间变量存在无限多个可能的匹配，因此在存在不确定时间增加的滴答规则的情况下，可能不可能单独探索所有可能的行为。相反，该工具提供了策略来探索所有可能的行为-直到重写序列的某个深度、持续时间或其他条件的满足-当使用前面描述的重写模式之一来实例化报价规则中的新变量因此，本文中提到的搜索策略被隐含地理解为分析在对报价规则的应用的所选限制内允许的所有可能的重写路径搜索可以嵌套，这样，一次搜索得到的重写路径集（每条路径由带有时间戳的状态表示）就可以作为其他搜索的在这种情况下，给定的时间限制适用于从初始状态开始的总时间，而不仅仅是从上一次搜索结束开始的计算持续时间（相反，当搜索由执行的一步顺序重写的数量限制时，每个新的子搜索从深度0开始。所有搜索命令的格式都是（strat SE.）其中SE是嵌套的OÜLVECZKY和MESEGUER14/−→/−→−→·−→−→·−→−搜索表达式如下所述。4.3.1基本搜索表达式基本搜索表达式包括：• 最简单的搜索表达式，其形式为项t，其中t是排序系统的基础项，表示嵌套搜索中的初始状态。命令（strattermt.）返回项t的简化形式。• 搜索表达式find [n]nJmaximum terms reachable fromSEmodemdti限期其中：n是表示在当前（子）搜索中在每个路径中执行的一步顺序重写的最大数目的数，并且其中n= 0意味着没有这样的限制;·nJ是返回的解决方案数量的上限，其中nJ= 0意思是SE是搜索表达式;m是模式d、m、ma、gd、gm、gma、tokend、tokenm或tokenma之一见第4.1节;是Time排序的基础项，表示默认的时间增加值;limit和前面一样，或者是ler，ltr，或者没有时间限制， r返回所有从SE返回的状态可到达的项，这些项不能在给定的时间和/或深度限制内进一步重写更准确地说，让t0是整个搜索的初始项，α：t0t是（子）搜索SE的一个解（由时间τ（α）中的项t那么，α;β：t0tJ是搜索的结果，仅当：β：tt_J是由可容许的一步序列构成的重写证明使用模式m进行重写，默认时间增量为100，并且在情况限制下，是ler，时间限制r。τ（α）;和不存在非平凡重写（使用模式）γ：tJtJJ使得τ（α; β; γ）在给定的时限内，或证明β：ttJ由nJ= 0个一步顺序重写组成。当τ（α;β）= 0时，得到的重写α;β：t0tJ在解的多集中表示为时间τ（α;β）中的t，否则表示为t。数字NJ限制了返回的多解集的大小，其可能不是一组（带时间戳的）项，因为时间r中的u可能表示导致时间r中的u的两个不同重写路径。• 窗体的搜索表达式find [n]nJdeadlocksfromSEmodemdti在时间限制内返回从搜索表达式SE的结果开始的给定时间和深度内可到达的所有死锁。·····OÜLVECZKY和MESEGUER15−→• 搜索表达式keepnfromSE返回不超过n个不同的来自搜索表达式SE的结果的时间戳项。4.3.2模式更高级的搜索策略是根据一个状态，可能还有通往该状态的路径上的总时间，是否与一个模式匹配来定义的。模式可以是常量noTerm（不与任何项匹配），常量anyPattern（与任何项匹配term），或者具有t（x）或t（x）的形式，其中C（x）。项t（x）应该是一个排序为System的项，或者是一个在时间v（x）中的形式为u（x）的项，允许我们陈述关于总时间流逝的属性此外，为了能够有效地检查匹配属性，要求模式是基不可约的w.r.t.理论的方程式也就是说，如果为了某种替代σ，项t（x σ）可以用一个方程来简化，那么xiσ对于x中的某个xi也可以。在重写a：t0w中达到的状态w匹配排序模式System，只要模式与w匹配（如果模式包含一个匹配，则满足where条件）;它在时间v（x）i中匹配形式为u（x）的模式，如果存在匹配σs。t. u（x σ）=w和v（x σ）=τ（α）（如果模式包含一个，则条件C（x σ匹配表达式的形式为[不]匹配模式u（x）[在时间v（x）]或[不]匹配extPatternu（x）[在时间v（x）]，其中C（x）其中方括号表示可选部分，或者匹配anyPattern，或者匹配noPattern，具有预期的含义。搜索表达式removeMEfromSE从SE中移除满足匹配表达式ME的解。4.3.3时态逻辑属性下文所述的搜索策略是出于对实时质量标准进行模型检查的需要。在更抽象的逻辑中陈述的属性[ 怎么样？]）.从排序系统的初始项t0开始的定时计算集由所有无限序列和不可扩展的有限序列组成σ：t0，0 −→t1，r1− →t2，r2− →···其中对于每个i≥1，要么σ的长度小于i+ 1，要么存在容许的一步顺序地面重写αi：ti−1−→ti，其中ri=ri−1+τ（αi）。σ的su x <$ti，ri<$−→···表示时间路径，记为σi。该工具目前支持以下类型的项目的模型检查OÜLVECZKY和MESEGUER16⟨⟩⟨⟩孔隙性质：• 直到：时间路径σi满足meU≤rmeJi ≠存在一个j≥i，其中rj≤rs.t.tj，rj满足匹配表达式meJ，并且对于所有i≤kj，<时间算子Ur和U在没有时间限制时可以类似地定义。• Until/stable：时间路径σi满足me可调≤rmeJi ∈σj满足meU≤rmeJ，另外，如果m ∈tj，rj满足匹配表达式meJ，那么每个m ∈tk，rk必须满足k>l且rk≤r。运算符UStabler和UStable可以用类似的方式定义。一对t，r满足一个时间属性σi，每个从t，r开始的时间路径σi满足σ i。一个这样的对的集合满足，如果集合中的每个对都满足。窗体的搜索表达式find [n]nJnot satisfyingMEUntilMEJfromSEmodemdti限期（其中n、nJ、m、n与前面的搜索策略相同，并且其中limit是ler、ltr或无时间限制）从搜索表达式SE返回的对开始搜索不满足属性MEUlimitMEJ（其中Ulim分别是U≤r、Ur或U）的定时路径。搜索策略从不满足属性的定时路径返回不满足属性的对。在时间限制是ler形式的情况下，重写模式包含该时间限制，使得如果可能的话，访问时间r由于对于密集时间模型，我们不能探索所有的重写，在一个新的变量的滴答规则的存在下，搜索的结果可能只是部分正确的，因为搜索发现的反例无效的属性，而没有反例并不能保证该属性持有。上述搜索的正面版本具有以下形式找到[n]nJ满足ME直到MEJ从SE模式mdti限期并返回在满足该属性的时间路径中满足匹配表达式MEJ的第一正路径的存在并不能证明公式w.r.t.初始项，因为其他路径可能无法满足该属性。形式的搜索表达式OÜLVECZKY和MESEGUER17∈∈{|∈ }查找[n]nJ 不满足我 来自SE模式mdti在时限内返回一些不满足属性ME可调限制MEJ的路径，由第一个建立不满足的对表示。以下有用的属性是上述搜索表达式的特殊情况，但在Real-Time Maude中有自己的命令• 不变性：在给定的深度和时间限制内可到达的所有项都应该满足给定的状态属性。 匹配表达式me的不变性可以由以下表达式给出：matchingnoPattern UntilStableme.• 活性：在每条路径中，在给定的深度和时间限制内，都有一个满足匹配表达式me的状态这个活性属性可以由表达式给出… 匹配任何模式直到我.用户可以通过在Real-Time Maude模块中导入TIMED-META-LEVEL模块并定义新策略来扩展Real-TimeMaude的策略库，如下一节所示5调度案例研究为了说明该工具的使用，我们将在本节中展示如何使用Real-Time Maude来指定和分析调度问题。我们考虑的问题，其中所有的周期和执行时间是固定的合理的数字，并在没有抢占是允许的。我们的规范化方法允许我们分析具有任意数量的进程和处理器的调度问题，而不需要对规范进行任何更改。5.1调度问题给定多个相同的处理机和一个奇偶性概率集合pii I，其中每个chpi都有一个奇偶性π（pi）Q+和执行时间τ（pi）Q+。计划是作为时间的函数的过程的所有过程，使得：(i) 没有一个处理器可以同时为多个进程(ii) 每个进程pi必须在其最后一个完成的周期内由一个处理器连续服务确切的时间τ（pi(iii) 每个进程都有无限数量的周期。调度问题通常通过指定满足前两个要求（“互斥”规范）的系统OÜLVECZKY和MESEGUER18∗−5.2相互排斥系统的状态可以被看作是一个面向对象的系统，由一组（多）代表进程的对象和一些特殊对象PRCSSR组成，其中PRCSSR的每次出现表示处理器的可用性由于时间作用于每个过程对象，最大时间流逝取决于每个过程对象，我们应该使用2.2节中描述的面向对象系统的规范技术，使用's，mte和δ，后两个分布在配置中一个进程由一个Process类的对象表示，该对象具有以下属性：• state表示进程的状态：sleep表示进程在当前周期内已经完成了所有的工作，只