同步总线仲裁器的定时性能模型检验

110URL：http://www.elsevier.nl/locate/entcs/volume 65. html15页s同步总线仲裁器的传奇：关于同步程序帕里托什湾 Pandya潘迪亚1，2技术和计算机科学学院塔塔基础研究所Homi Bhabha Road，Colaba，印度孟买，邮编400005摘要量化离散时间持续时间演算（QDDC）是一种间隔时间逻辑[14]。它非常适合于描述同步系统的定量定时特性。QDDC的自动机理论决策过程允许将QDDC公式转换为精确识别公式模型的有限状态自动机。该自动机可作为同步观测器，对同步程序的性质进行模型检验。这一理论已被实施到一个工具，称为DCVALID允许模型检查QDDC性能的同步程序写在Esterel，Verilog和SMV符号。在本文中，我们考虑两个著名的同步总线仲裁器电路（程序）从文献。我们指定这些仲裁器的一些复杂的定量属性，包括他们的响应时间和损失时间，使用QDDC。我们展示了如何使用工具DCVALID有效地模型检查这些属性（一些令人惊讶的结果）。1介绍对于同步程序，执行时间是以时钟节拍来衡量的也就是说，时间的概念是离散的。对于许多这样的程序，重要的是要分析定量的时间属性，如响应时间和延迟。不幸的是，这样的分析没有得到程序验证社区的足够重视。1由联合国大学/软件技术研究所海岸项目提供部分支助。使用持续时间演算的时间计划：理论与实践2电子邮件地址：pandya@tifr.res.in2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。111量化离散时间持续时间演算（QDDC）是一种非常适合指定此类定量定时属性的逻辑QDDC是一种具有原语的时间间隔逻辑的形式，其对给定行为片段中信号的出现次数进行计数。它是一种高度表达性的逻辑，可以简洁地指定许多复杂的属性。因此，QDDC解决了同步程序的性质与先前考虑的性质不同的性质[4，18，3，11]。为了说明这一点，在本文中，我们考虑两个著名的同步总线仲裁器电路（程序）。使用QDDC，我们指定这些仲裁器的一些复杂的定量属性，包括它们的响应时间和损失时间。尽管QDDC公式具有很高的表达能力，但它可以进行模型检验。自动机理论决策过程允许将QDDC公式转换为精确识别公式模型的有限状态自动机[14]。该自动机可以用作同步观测器，用于同步程序的模型检查[8，15]。我们已经将这一理论实现到一个名为DCVALID的工具中，该工具允许对用Esterel、Verilog和SMV表示法编写的同步程序的QDDC属性进行模型检查[13，16]。在本文中，我们展示了如何使用工具DCVALID来有效地模型检查的仲裁电路的时序特性，一些令人惊讶的结果。这是我们的主张，这些属性是很难分析的手和系统设计师的直觉，他们因此，工具的可用性对于验证这些属性至关重要。论文的其余部分组织如下。在1.1节中介绍了一些同步总线仲裁器电路第2节简要概述了逻辑QDDC本文还简要介绍了自动机理论在模型检测中的应用在第3节中形式化了仲裁器的性质。这些属性的分析，由我们的工具DCVALID进行，在第4节中介绍。本文最后作了简要总结。1.1同步总线仲裁器示例1.1具有n个单元的同步总线仲裁器具有请求线req1，.. . ，reqi，.. . ... . ，acki，.. . ，ackn.在任何时钟周期，请求线的子集为高。仲裁器的任务是将对应的确认线中的至多一个设置为高。优选地，仲裁器应该对所有请求都是公平的麦克米伦[11]提出了电路总线仲裁器3的图1的总线仲裁器3的总线仲裁器。他还分析了它的基本属性，例如使用开创性的SMV验证器对ck信号进行互斥。该电路也可以被编码为Esterel模块。我们提出了两个变体MacMillan的仲裁器在图4中。 (The原仲裁人3电路元件是标准的。方形框表示D锁存器，其延迟一个时钟周期的信号。112请求确认输令牌超过请求出骑马格兰特确认输令牌格兰特在请求确认输E1过骑E2EnTokenOut覆盖授权输W请求阿科特不TokenInOverrideOut授予电池互连0单元电路Fig. 1. MacMillan用虚线突出显示）。第一个变体MacarbV1是由于将原始仲裁器代码错误地翻译成Verilog而产生的，第二个变体MacarbV2是由于Rahul Jain。deSimone [5]提出了一种不同的仲裁器电路，如图2所示，他还给出了该电路的Esterel模型所有这些仲裁器都具有一次最多只能出现一个现有的模型检查器，如Xeve [5]、VIS [3]或SMV[11] 可以很容易地验证这种不变性。✷例1.2我们考虑这些仲裁器的一些复杂性质，这些性质以前没有被研究过其中许多涉及定量时间方面。对于给定的仲裁器电路，必须分析这些属性中的每一个113请求阿科特令牌请求出格兰特阿科特令牌在请求阿科特E1格兰特E2En电池互连单元电路TokenOut授权输请求阿科特TokenIn授予图二. de Simone对于给定的常数n，(i) 单元i的响应时间：仲裁器的单元i的最坏情况响应时间是否在m个周期内？换句话说，给定一个常数m，在任何行为期间和在跨越m个周期的任何时间间隔中，如果reqi连续为高，是否一定存在cki？求最小的常数m。(ii) 单元i的3周期响应时间：在k个周期内获得3个cki信号的最差情况响应时间求最小的常数k。(iii) 如果至少一个细胞的req高，但所有细胞的ck低，则周期丢失。仲裁器可以释放不超过l个连续周期吗？找到最小的l。114∈(iv) Fifo（i，j）性质：如果单元格i的req出现在单元格j的req之前（并且持续存在），单元格i的ack是否一定会出现在单元格j的a ck之前？在这种情况下，我们说Fifo（i，j）成立。确定给定仲裁器电路的具有Fifo（i，j）性质的所有对（i，j✷我们敦促读者尝试直观地回答例1.1中给出的四个同步仲裁器电路的上述问题2量化离散时间持续时间演算量化离散时间持续时间演算（QDDC）是一种用于指定有限状态序列（赋值）属性的区间我们简要介绍一下这个逻辑。设Pvar是一组有限的命题变量，表示某个目标。可作为系统状态的一部分。 LetVAL（Pvar）d=efP var→{0，1}be赋值的集合为每个变量分配真值 我们将识别出一个有缺陷的、非空的序列，即：VAL（Pvar）+.例2.1下图给出了变量{p，q}的行为。每个列向量给出一个赋值，单词就是这样的列向量的序列。p1 0 1 1 0Q0 0 0 0 1上面的这个词满足p在开始时成立，q在结束时成立，但在此之前不成立的性质QDDC是一种形式化这些属性的逻辑每个公式指定一组这样的词。✷给出一个非空的有限值序列sσVAL+，我们不满足σ上的QDDC公式D，σ |= D我们现在给出QDDC的语法和语义，并定义上述满足关系。QDDC公式的推导设Pvar是命题变量的集合设p，q是命题变量的值域，P，Q是命题（p，q的布尔组合）的值域，D，D1，D2是QDDC公式的值域.设c的范围为自然数常数。QDDC的语法如下。

|[P]|[[P]]| D1^d2| D1&&D2|！D|从P.D|斯伦OP C |Scount P op c哪里操作符在{=，，=，>，>=}115|{∈|联系我们σ。Letσ∈VAL（Pvar）+beabehaviour. Let#σ表示σ的第i个元素，σ[i]表示第i个例如，如果σ=v0，v1，v2，则#σ= 3且σ[1] =v1。 令dom（σ）={0，1，.，#σ-1}表示内的位置集合设σ，i=P表示命题P在位置i处求值为真，σ。我们忽略了这个明显的定义。σ中的区间集是Intv（σ）=[b，e]dom（σ）2b e，其中每个区间[b，e]标识位置b和e之间的σ的子序列。我们归纳地定义了QDDC公式D对行为的满足度[1][2][3][4][5][6][7][8][9] 这表示为σ，[b，e]|= D. σ，[b，e]|=

ib = e和σ，b| = Pσ，[b，e]|=[[P]]i <$σ，i |= P对于所有i：b ≤ i ≤ eσ，[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实体slen和scount P称为测量。 项slen表示间隔的长度（以步数计），而scount P表示P在间隔[b，e]内为真的次数的计数eval（slen，σ，[b，e]）d=efe−bdef 埃莱如果σ，i，则为|= Peval（scount P，σ，[b，e]）=让t在测量范围内变化然后，i=b0，否则为0σ，[b，e]|= t op ci eval（t，σ，[b，e]）op c注意，对于具有3个步骤的状态序列，即4个状态，slen=3成立。也对于P为真3次的序列，计数P = 3称一个行为σJ是σ的p-变元，条件是#σ=#σJ，并且对于所有i∈dom（σ），对所有qi=p，有σ（i）（q）=σJ（i）（q）. 然后，σ，[b，e]|= ex p. Di <$σJ，[b，e]|= D对于σ的某个p-变式σJ最后，σ |= Di <$σ，[0，#σ − 1]|= D我们也可以定义一些派生的构造。 布尔组合子||，=>，<=>表示或，暗示和等价可以定义为&&，！和往常一样。def• <>D = true^D^true成立，前提是D对某个子区间成立。def• []D=！& lt;>！为所有子区间提供D保持。116|例2.2我们给出QDDC公式的一些例子• 实施例2.1的性质可以如下在QDDC中公式化。它具体说明了P最初成立而Q在结束时成立但在此之前不成立的行为。

^[！Q]^Q>• 下面的公式适用于为σ的所有片段σJ提供的行为σ，这些片段（a）在开始时P为真，（b）在结束时Q为真，并且（c）在其间没有Q的出现，σJ中R为真的状态的出现次数至多为3。[]（

^[！Q]^ =>（scount R <= 3））QDDC可以描述系统的安全性和有界活性 由于它只指定有限个状态序列，因此它不能处理一般的活性属性。有许多扩展解决这个问题[15]。2.1模型检测QDDC一个同步程序P的执行α是一个有限的或无限序列的赋值（状态）。如果α的所有有限个前缀都满足D，则QDDC公式D对执行成立（有效）。最后，如果D对D的所有执行都有效，则公式对程序P有效。令α[i]表示序列α的第i个元素，并且令α[i：j]表示位置i到j（包括i和j）之间的子序列定义2.3 [前置有效性]设α| = D我的 α [0：e]|= D对于所有e∈dom（α）。 设P| = D我的 α |= D对于P的所有执行α模型检验问题是通过算法确定P=D. 我们概述了一个自动机理论的方法，模型检测QDDC下面下面的定理描述了QDDC公式的模型集设pvar（D）是QDDC公式D中出现的命题变量的有限集合。设V AL（Pvar）=Pvar→ { 0， 1}是Pvar上的赋值集。定理2.4对于每个QDDC公式D，我们可以有效地构造字母表V AL（pvar（D））上的有限状态自动机A（D），使得对于allσ∈V AL（pvar（D））<$，σ|= Di<$σ ∈L（A（D））关于这个定理的证明，我们请读者参考[14]这种构造已经被实现到一个名为DCVALID的工具中[13，14]。例2.5例2.2的第一个性质可以在QDDC中表述为公式

^[！Q]^。下面给出对应于该公式的自动机。每一条边都用一个列向量来标记，该列向量给出变量P、Q的真值，如例2.1所示。此外，字母X用于表示0或1。注意，自动机是最小的，确定的和总的。117ǁ11X003X0 1XX，1XXX14从这个自动机，我们可以看到，一个模型和计数器模型的最小长度的公式如下。（QDDC中不考虑空词型号计数器型号P 1 X P 1Q 0 1 Q 0给定QDDC公式D，我们可以使用自动机A（！D），如定理2.4所获得的，作为同步观测器，用于确定在执行期间D的违反。其基本思想是系统M和观察者A（！D）以同步并行（锁步）模式执行。这意味着我们考虑转换后的系统MJd=efMA（！D）观察者是一个完全的、确定性的自动机。它不会以任何方式抑制或约束M的活动。在执行MJ的任何一点，观察者都将观察到M分量中出现的状态序列如果这个状态序列满足！D则观察者将处于其最终状态，否则观察者将处于其非最终状态。因此，M违反D，当且仅当存在M j的某些执行，在此期间，观察者！D进入最后状态。(SeeHalbwachs等人 [8]详细介绍了观察者验证方法。）定理2.6M| = D iA的最终状态（！D.无法到达（M A（！（D））我们省略了这个定理的证明，它可以在别处找到[15]。如果M是一个有限状态系统，那么（M A（！D））。对于这样的系统，最终状态的可达性可以通过符号广度优先搜索来分析[11]。现在已经有很多成熟的模型检测工具可以很有效地完成这种搜索。例如，如果M和A（！D）作为Esterel模给出，Esterel验证工具Xeve [5]可以执行此搜索。类似地，如果它们作为SMV模块给出，则SMV工具[11]可以执行搜索，如果它们作为Verilog模块给出，则VIS工具[3]可以执行搜索。请注意，所有这些工具的建模语言都支持同步并行组合，允许观察者运行2118与系统同步利用这些搜索过程，我们已经构建了一个模型检测工具，用于检查Esterel，SMV和Verilog设计的QDDC属性2.2工具DCVALID从QDDC公式到有限状态自动机的简化，如定理2.4所述，已被实现为称为DCVALID的工具[13，14]。该工具生成一个总的，确定性的和最小的自动机的公式，它也可以检查的有效性，通过搜索拒绝路径中的自动机的公式。例2.5中的自动机是通过工具DCVALID从公式一个相关的工具，称为CTLDC，将自动机转换成Esterel，SMV或Verilog模块，以提供一个同步观察者的属性。它还连接模块以与给定的系统模块同步运行可以使用现有的工具（如Xeve [5]，SMV [11]和VIS [3]）分析所产生的这确定QDDC属性对于给定系统模块是否有效，如定理2.6所述。因此，DCVALID可以确定M是否|其中M是（纯）Esterel、SMV或Verilog程序，D是QDDC公式。如果验证失败，该工具将生成一个反例。逻辑QDDC的细节、工具DCVALID的架构和一些性能统计数据在其他地方描述[14，16]，为了简洁起见，在此省略基本上，DCVALID是建立在MONA之上的[7]。MONA是Buchi和Elgot的自动机理论决策过程的有效和复杂的实现，用于有限词上的一元逻辑（MLSTR）。DCVALID的工作原理是将QDDC公式转换为MLSTR公式的布尔组合每个组件然后被MONA翻译成一个虽然最坏情况下的复杂性是非基本的，但该工具通常能够处理相当大的公式[14]。3QDDC中同步总线仲裁器的规范我们现在在QDDC中正式定义同步总线仲裁器的四个属性，这在前面的示例1.2中给出(i) 单元i的响应时间仲裁器的单元i的最坏情况响应时间是否小于或等于m个周期？形式上，下面的公式对于给定的仲裁器电路有效吗[]（[[Reqi]]&&（slen = m-1）=><>< Acki>）找到使这个公式对给定仲裁者有效的最小值m(ii) 单元i的3周期响应时间最坏情况下获得3个 cki信号的响应时间是否小于或等于k周期？下面的公式对仲裁人是否正式有效？[]（[[Reqi]]（slen = k-1）=>（scount Acki >= 3））119找到使这个公式对给定仲裁器有效的最小k(iii) 损失时间仲裁器是否可以损失不超过l个连续周期？例如，下面的公式对仲裁者有效吗[]（[[lostcycle]] => slen = l-1）找到使公式对给定仲裁者有效的最小l(iv) FIFO（i，j）属性查找（i，j）对，以使以下公式对给定仲裁器有效。这个公式表明，如果对单元i的请求在单元j的请求之前到达，并且它持续存在，那么对单元j的确认不能在单元i的确认之前发生。[]（（！reqj>^[[reqi&&！acki]]）=>！<> ackj>）4Arbiter属性QDDC的模型检查器在第2.2节中描述。对于具有固定常数n的给定n个单元仲裁器，DCVALID工具（与诸如Xeve的可达性分析工具一起）可以检查诸如[]（[[Reqi]]（slen = k-1）=>（scount Acki>= 3））对于给定的常数k值，对于仲裁器是有效的。为了找到使这个公式有效的最小k，我们必须尝试不同的k值。第3节中给出的同步总线仲裁器的四个属性针对各种5单元仲裁器电路进行了检查。这些性质被验证为de Simone这些仲裁器的电路图已在前面的例1.1中给出使用工具DCVALID和Xeve/SMV进行验证实验，并根据电路的Esterel和SMV代码检查属性。de Simone这个电路包含一个潜在的组合循环和一个复杂的需要对Esterel进行因果关系分析[2]。我们在下面给出模型检查的结果在每种情况下，给出了使公式有效的最小常数这是通过试验和错误发现的(The读者可以参考第3节，了解被验证属性的定义性质1：单元i的响应时间mSimarb：m= 5个循环，对于细胞i= 1至5Macarb：m= 5个循环，对于细胞i= 1Macarb：m= 10个循环，对于细胞i= 2至5MacarbV1：m= 5个循环，对于细胞i= 1MacarbV1：m= 6个循环，对于细胞i= 2至5MacarbV2：m= 5个循环，对于细胞i= 1MacarbV2：m= 10个循环，对于细胞i= 2至5120TokenOut覆盖授权输W请求阿科特不TokenInOverrideOut授予TokenOut覆盖授权输W请求阿科特不TokenInOverrideOut授予MacarbV1MacarbV2图三. MacMillan's Arbiter的变体性质2：电池i的3周期响应时间kSimarb：k= 15个循环，对于细胞i= 1至5Macarb：k= 15个循环，对于细胞i= 1Macarb：k= 20个循环，对于细胞i= 2至5MacarbV1：k= 15个循环，对于细胞i= 1MacarbV1：k= 16个循环，对于细胞i= 2至5 MacarbV2：k= 15个循环，对于细胞i= 1MacarbV2：k= 20个循环，对于细胞i= 2至5121特性3：最大连续丢失周期数Simarb：l= 0，即无循环损失。Macarb：l= 5，即最多连续丢失5个周期。MacarbV2：l=0，即无丢失周期。在MacarbV 1的情况下，对于所有大的l值，属性失败或检查器耗尽时间/内存。因此，无法找到l的上限性质4：Fifo（i，j）对我们精确地列出了Fifo（i，j）性质成立的那些（i，j）对Simarb：（1，2），（2，3），（3，4），（4，5），（5，1）Macarb：（1，2），（1，3），（1，4），（1，5），（2，3），（3，4），（4，5）MacarbV1：（1，2），（1，3），（2，3），（3，4），（4，5）MacarbV2：（1，2），（1，3），（1，4），（1，5），（2，3），（3，4），（4，5）这种模型检查的一个重要方面是，如果验证得出属性无效的结论，则会生成一个反例场景例如，如果针对值为l = 4的MacMillan的5单元仲裁器检查属性3下面给出了使用DCVALID和Xeve生成的这种反例如果我们在此输入上模拟仲裁器，我们发现实际上连续丢失了超过4个周期req1;req1 req2;req1 req2 req3;req1 req2 req3 req4;req2 req3 req4 req5 ; req2req3 req4 req5;req4 req5 ; req4req5;req5;req4;性能QDDC是一种高度表达性的逻辑，可以简洁地指定复杂的属性。在最坏的情况下，自动机A（D）的复杂度可以是D的大小的非初等，尽管这在实践中很少观察到(See[14]一些统计数据。在这里，我们为MacMillan的仲裁者Macarb验证属性3提供原始性能数据对于一个n-胞腔的仲裁器，该性质在胞腔i= 3的情况下被验证为m= 2n。测试在1.4GHz Pentium 4处理器机器上进行，具有512 Mbytes的RAM，运行Linux 2.4.16内核。测试中使用了Esterel V5.92和SMV版本2.5.4.3所有时间值都以秒为单位。122|细胞SMVEstereln观察员一代验证观察员一代编译验证（checkblif）50.060.010.060.151.27100.130.070.070.2835.211001.063.511.063.09**2004.67140–––** 由于内存溢出，100单元仲裁器的Esterel验证在8小时后中止。5总结QDDC是一种高度表达性的逻辑，它允许方便地指定syn-task程序的复杂属性。它特别适合于定量定时属性的指定，如响应时间。此外，QDDC是由一个模型检测工具DCVALID，可以有效地分析这些属性的支持。QDDC是密集时间逻辑持续时间演算的离散时间版本[19，9]。逻辑的表达能力足以让我们编写一个同步语言的合成语义，比如纯Esterel [17]。我们已经表明，电路/同步程序，如例1.1的同步总线仲裁器，在它们的复杂性中体现了相当程度的复杂性。MacMil- lan的Arbiter及其两个变体的响应和损失时间的令人惊讶的值类似地，对于各种仲裁器，满足Fifo（i，j）性质的（i，j）的值因此，逻辑和同步程序的定时属性的模型检查器值得认真研究。逻辑QDDC和工具DCVALID允许执行这样的分析。QDDC是一种离散时间间隔时序逻辑，用于指定同步程序的其他此类逻辑包 括 Emerson 等 人 的 RTCTL [6] 和 Amla 等 人 的 同 步 规 则 时 序 图 [1] 。Jagadeesan等人开发了一个名为TEMPEST的工具集，用于验证Esterel程序的安全性和一些响应特性[10]。应该注意的是，本文中验证的所有定时性质都具有这样的形式：对于给定的常数（自然数）l，M=D（l）成立。例如，属性3规定不能丢失超过l个连续周期真正的问题是找到l的最小值，使该性质成立。本文提出的方法允许这样的最小/最大值，只有通过尝试不同的值l。这可能很麻烦，123有时是不可能的。例如，在验证仲裁器MacarbV1的属性3时，我们发现该属性不适用于任何可能的常数l值。然而，有没有可能这个性质确实对l的某个非常大的未尝试的值成立。最近，我们已经扩展了我们的工具DC- VALID的方法，可以使用这些方法，我们已经确定性质3实际上对于常数l的任何值都不成立，并且仲裁器MacarbV1可以无限制地释放许多连续的周期。正在编写的一份单独的文件将介绍这些技术和结果。引用[1] Amla，N.，E. Allen Emerson，R.P. Kurshan和Kedar S.陈文生，同步时序图之模型检验，国立成功大学电机工程研究所硕士论文，2000年。[2] Berry，G.，Esterel的建构语义学，1999年。[3] 布 莱 顿 ， R.K. ， G.D. Hatchtel 等 人 ， VIS ： 验 证 和 综 合 系 统 ， 在 Proc.Computer Aided Verification，CAV[4] Bouali，A.，马莫拉特河de Simone和H.陈文辉，“同步无功系统在Esterel中的程序设计”，载于《FTRTFT'96学报》[5] Bouali，A.，XEVE：一个Esterel验证环境，Proc.计算机辅助验证，CAV[6] 埃默森，EA，A.K. Mok，A.P. Sistla和J. 李文生，定量时间推理，中国科学 技 术 出 版 社 ， 20 0 0 年 。[7] Henriksen，J.G.，J. 詹森，M。约根森，N。克拉隆德湾佩奇，T。劳厄，A. Sandholm，Mona：Monadic Second Order Logic in Practice，inTools andAlgorithms for the Construction and Analysis of Systems，First InternationalWorkshop，TACAS[8] Halbwachs，N.，F.林志荣，“动态系统的动态特性与动态系统的动态特性”，国立成功大学机械工程研究所硕士论文，2000年[9] Hansen，M.R. Zhou Chaochen，Duration Calculus：Logical Foundations，Journal of Formal Aspects of Computing9，1997.[10] Jagadeesan，L.J.，C. Pouchol和J.E. Von Olnhausen，Esterel程序的安全特性验证和电信软件的应用。 在proc CAV'95 ， LNCS 939 ， Springer-Verlag，1995年。124[11] McMillan，K.，符号模型检验，Kluwer Academic Publishing，1993。[12] Moszkowski，B.，A Temporal Logic for Multi-Level Reasoning aboutHardware，IEEE Computer，18（2），1985。[13] Pandya，P.K.，DCVALID用户手册，塔塔基础研究所，孟买，1997年。（修订版见http://www.tcs.tifr.res.in/www.pandya/dcvalid.html）。[14] Pandya，P.K.，使用DCVALID确定量化离散时间持续时间演算公式：自动机理论方法，实时工具研讨会（RTTOOLS[15] Pandya ， P.K. ， 模 型 检 验 CTL*[DC] ， 在 Proc. TACAS 2001 ， Genova ，Italy，LNCS 2031，Springer-Verlag，2001。[16] Pandya，P.K.， SMV的模型检查CTL[DC]规范，Verilog和Esterel设计，技术报告，TCS-00-PKP-3，塔塔基础研究所，2000年9月。[17] Pandya，P.K.，Y.S.罗摩克里希纳和R.K. Shyamasundar持续时间演算中Esterel的合成语义。第二届AMAST实时系统研讨会：模型与证明，波尔多，1995年6月。[18] Raymond，P.，通过数据流网络识别正则表达式，在Proc.23rd InternationalColloquium on Automata，Languages，and Programming，（ICALP帕德博恩（德国），1996年7月。[19] 周朝辰，C.A.R. Hoare and A.P. Ravn， A Calculus of Durations， Info.Proc. Letters，40（5），1991.