符号搜索法在量化离散时间持续时间演算中的应用

理论计算机科学电子笔记128（2005）247-262www.elsevier.com/locate/entcs用符号搜索法帕里托什湾Pandya1技术和计算机科学学院塔塔基础研究所HomiBhabha Road，Colaba印度孟买，邮编400005摘要QDDC是一种用于指定同步程序的定量定时方面的逻辑。最坏情况下的响应时间和延迟（当已知时）等属性可以在此逻辑和模型检查中优雅地指定。然而，计算这些值需要通过试错法找到参数k的最小/最大值，使公式D（k）对程序有效。在本文中，我们讨论了如何自动机理论的决策过程QDDC连同符号搜索最短/最长路径可以用来计算的极值（最小/最大长度）模型的长度公式D。这些技术已在QDDC公式的DCVALID验证器中实现。我们通过有效地计算一些同步总线仲裁器电路的响应时间和死区时间来说明这种技术的使用。关键词：符号模型检验，响应时间计算，离散时间演算，极值模型，SMV。1介绍对于同步程序（例如时钟电路），执行时间是以时钟节拍来衡量的，即时间的概念是离散的。对于许多这样的程序，重要的是要分析定量的时间属性，如响应时间和延迟。做这样的定量分析仍然是形式化方法社区的一个挑战性问题。1电子邮件：pandya@tifr.res.in1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.015248P.K. Pandya/Electronic Notes in Theoretical Computer Science 128（2005）247量化离散时间持续时间演算（QDDC）[12]是一种高度表达的逻辑，用于指定状态（行为）的有限序列的属性它与Moszkowski [11]的区间时态逻辑和Zhou等人 [16]的持续时间演算密切相关（它们的关系见[12，15，6]）。它为描述行为提供了新的基于间隔的模式。例如，以下公式适用于为所有片段提供的行为σσ的σJ，其中（a）P在开始时为真，（b）Q在结束时为真，(c)之间没有Q的出现，σJ中状态出现的次数其中R为真，最多为3。Q（[P|0-[[<$Q|-[Q|0μ（μR≤3））。在这里，Q模态的范围涵盖了行为的所有片段操作符-类似于行为片段和[[<$Q]的串联（融合）|陈述了<$Q在行为片段上的不变性。最后，RISPR计算R在行为片段中出现的次数QDDC的语法和语义的精确定义在第2节中给出。尽管QDDC公式具有很高的表达能力，但它们可以进行模型检验。自动机理论决策过程允许将QDDC公式转换为精确识别公式模型的有限状态自动机[12]。该自动机可以用作同步观测器，用于同步程序的模型检查[8]。我们已经实现了这个理论到一个工具称为DCVALID [12，13]，它允许模型检查同步程序的QDDC属性写在Esterel [2]，Verilog和SMV [10]符号。量化离散时间持续时间演算（QDDC）是一种非常适合于指定同步程序的定量定时属性的逻辑。它AD-Dresses的性质的同步程序从前面考虑的定性不同的类。最坏情况下的响应时间和延迟（当已知时）等属性可以在此逻辑和模型检查中优雅地指定。然而，计算这些值需要通过试错法找到参数k的最小/最大值，使公式D（k）对程序有效。这样的试错法本质上是不完整的。在本文中，我们提出了许多有趣的定时特性的公式，作为系统的极值（最短/最长）子执行的长度满足逻辑QDDC中写入的属性D。我们所说的子执行是指执行的有限（不一定是初始）片段。例如，响应时间可以用公式表示为请求确认保持不变的最长子执行的长度逻辑QDDC非常适合以这种方式指定复杂的时序要求。我们称这种方法为基于极值模型长度的规范。在本文中，我们展示了如何自动机理论决策过程，P.K. Pandya/Electronic Notes in Theoretical Computer Science 128（2005）247249QDDC与最短/最长路径的符号搜索一起可以用于计算极值模型长度。这些技术已在QDDC公式的DCVALID验证器中实现。该实现建立在中可用的最短/最长路径的符号搜索例程之上，NuSMV验证器。我们说明了使用我们的技术计算响应和死区时间的一些同步总线仲裁器电路使用我们的工具DCVALID和NuSMV，一些令人惊讶的结果。这是我们的主张，这些属性是很难分析的手和系统设计者的直觉，他们因此，工具的可用性对于分析这些属性至关重要。在本文中，我们还提供了我们的极值模型长度计算与传统的模型检测的效率的实验比较。论文的其余部分组织如下。同步总线仲裁器电路模型将在下一小节中介绍。第二节简要介绍了逻辑QDDC及其模型检验。极值模型长度的概念在第3节中定义。第4节介绍了用于象征性地计算极值模型长度的主要技术。第5节简要介绍了该技术在我们的工具DCVALID中的实现。文中还给出了总线仲裁器电路时序分析的实验结果。文章最后进行了讨论。1.1同步总线仲裁器例1.1具有n个单元的同步总线仲裁器具有请求线req1，.. . ，req i，.. . .，acki，.，ack n.在任何时钟周期，请求线的子集为高。仲裁员的任务是将对应确认线中的至多一个设置为高。优选地，仲裁器应该对所有请求都是公平的。图1的总线仲裁器电路（称为MacArbV0）由McMillan [10]使用基于符号模型检查2的开创性SMV验证器进行分析。图2给出了McMillan仲裁器的一个变体MacArbV1(The来自原始仲裁器的改变由虚线突出显示）。这两个仲裁器都具有一次最多可以出现一个ack信号的特性。Q例1.2我们考虑ar的一些定量定时特性，2电路元件是标准的。方框表示将信号延迟一个时钟周期的D锁存器250P.K. Pandya/Electronic Notes in Theoretical Computer Science 128（2005）247电池互连0请求确认输出代币输出请求在E2授权输出确认输授予请求确认E1出来覆盖TokenInEn单元电路TokenOut OverrideIn授权输出W请求阿科特不TokenInOverrideOut授予Fig. 1. McMillan调制单元电路TokenOut OverrideIn授权输出W阿科特请求不TokenInOverrideOut授予图二. McMillan's Arbiter的变体行尸• 3周期响应时间：在最坏情况下，reqi必须连续保持高电平以确保acki出现三次的最少周期数。P.K. Pandya/Electronic Notes in Theoretical Computer Science 128（2005）247251• 死区时间：连续丢失周期的最大可能数量。如果至少一个单元格的req为高，但所有单元格的req都为低，则周期丢失。acklow，即lostcycled=ef（i ） reqi）请求（jACK J）。Q2量化离散时间演算（QDDC）设Pvar是一个有限的命题变量集，表示一些可观察的系统状态的各个方面。LetVAL（Pvar）d=efPvar→ {0， 1}是以下的集合：赋值给每个变量一个真值。我们将用有限的、非空的估值序列来识别行为I.E. VAL（Pvar）+的元素。例2.1下图给出了变量{p，q}的行为。每个列向量给出一个赋值，单词就是这样的列向量的序列。p1011 0Q0000 1上面的这个词满足p在开始时成立，q在结束时成立，但在此之前不成立的性质。QDDC是一种形式化这些属性的逻辑。每个公式指定一组这样的词。设σ∈VAL+的非空有限序列，σ不满足σ上的QDDC公式D| = D.QDDC公式设Pvar是命题变量的集合。设p是命题变量的值域，P，Q是命题的值域，D，D1，D2是QDDC公式的值域.命题是由变量Pvar和常数0， 1（分别表示为true，false）使用布尔连接词，<$等构造的。QDDC的语法如下。[P|0|[[P||D1-D2|D1-D2|D|不好意思D|η op c|其中op∈ {<，≤，=，≥，>}。Letσ∈VAL（Pvar）+bea behaviour. Let#σ表示σ的长度，σ [i]表示第i个元素。例如，如果σ=v0，v1，v2，则#σ= 3且σ[1] =v1。令dom（σ）={0，1，.，#σ−1}表示σ内的位置集合。σ中的区间集由Intv（σ）={[b，e] ∈dom（σ）2|b≤e}其中每个区间[b，e]标识位置之间的σ的子序列b和e。252P.K. Pandya/Electronic Notes in Theoretical Computer Science 128（2005）247令σ，i| = P表示命题P在位置i处求值为真，σ。我们忽略了这个明显的定义。我们归纳地定义QDDC公式D对于行为σ和区间[b，e]∈Intv（σ）的满足如下。σ，[b，e]|=[P |0 ib=e和σ，b |= Pσ，[b，e]|=[[P |i∈< e和σ，i| = P对于所有i：b≤i< e σ，[b，e]|=<$Di <$σ，[b，e]|= Dσ，[b，e]|= D1<$D2i <$σ，[b，e]|=D1和σ，[b，e]|= D2σ，[b，e]|=D1-D2i对于某些m：b≤m ≤e：σ，[b，m]|= D1和σ，[m，e]|= D2.实体η和ηP称为测量。项η表示区间的长度，而P表示P在区间[b，e]内为真的次数（我们将区间视为左闭和右开）。从形式上讲，eval（η，σ，[b，e]）d=ef e−b⎧ ⎫defe−1<$1 if σ，i| = Peval（σ，[b，e]）=i=b.0，否则为0让t在测量范围内变化。然后，σ，[b，e]|= t op ci = eval（t，σ，[b，e]）op c.称行为σJ是σ的p-变式，条件是#σ= #σJ，并且对于所有i∈dom（σ），且对所有qp，我们有σ（i）（q）= σJ（i）（q）。然后，最后，σ，[b，e]|= p.D i <$ σJ，[b，e]|= D对于σ的某个p-变式σJ。σ|= Di <$ σ，[0，#σ−1]|= D.来源的构建体我们也可以定义一些派生的构造。布尔组合子可以像往常一样使用来定义。• 的|d=ef[1]|0对于f [ b，b ]的p_i_n_t_v_s成立。• [[P||-[P|0）表示，假设P仅在包括端点的扩展闭合定义[ b，e ]上保持不变 。 |0)statesthatpro positionPholdsi nvaria ntlyoverthe extendedclosedinterv a l[b,e]includingtheend poi nt.F或mula[[P||中文（简体）||0）另外也适用于P为真的点区间。|0) additionally also holds for point intervalswhere P is true.• QDd=eftrue-D-t rue holdsprvidedDholds forsomeesubinterval.• QDd=ef<$Q<$Dholdpro dDholdforallsubi nter v als.P.K. Pandya/Electronic Notes in Theoretical Computer Science 128（2005）247253QDDC的可判定性下面的定理描述了满足QDDC公式的模型集设pvar（D）是QDDC公式D中出现的命题变量的有限集合。令VAL（Pvar）=Pvar→ { 0， 1}为Pvar上的赋值集。定理2.2对于每个QDDC公式D，我们可以有效地构造字母表VAL（pvar（D ））上的有限状态自动机A （D ）， 使得对于所有σ∈VAL （pvar（D））∈，σ|= Di<$σ∈L（A（D））.推论2.3 QDDC公式的可满足性（有效性）是可判定的。QDCVALID从QDDC公式到有限状态自动机的简化，如定理2.2所述，已经在一个名为DCVALID [12]的工具中实现，该工具还检查公式的有效性，如推论2.3所示。这个工具是建立在MONA之上的[9]。MONA是一个复杂而有效的基于BDD的有限词上一元逻辑的自动机理论决策过程的实现。一个相关的工具，称为CTLDC [13]，将自动机转换为Esterel，SMV或Verilog模块，为属性提供同步观测器[8]。使用这个，DCVALID可以模型检查M是否|其中M是Esterel、SMV或Verilog程序，D是QDDC公式[13]。例2.4[仲裁器规范]我们在QDDC中形式化了例1.2• 3周期响应时间：最小k，使得以下对仲裁器有效Q（[[reqi||η≥k −1• 死区时间：最小k，使得以下对仲裁器有效Q（[[lostcycle||（

下载后可阅读完整内容，剩余1页未读，立即下载