时间并发约束编程和模型检测方法

理论计算机科学电子笔记48（2001）网址： http://www.elsevier.nl/locate/entcs/volume48.htmlpp. 1- 14用时态并发约束语言IAlberto Policriti2 Alicia Villanueva3乌迪内大学数学与信息学院意大利乌迪内摘要在本文中，我们提出了一种方法来建模并发系统中指定的时间并发约束语言。我们的目标是构建一个框架，在这个框架中，可以将模型检查技术应用到用这种语言指定的程序中。本文的工作是框架构建的第一步提出了一种将规范转换为tcc结构的形式化方法该结构是程序行为的图形表示。我们的基本工具是Saraswat等人定义的时间并发约束编程（TCC）框架。 来描述反应系统。通过这种语言，我们利用了声明性范式的自然属性和时间概念内置于编程语言语义中事实上，在这个基础上，引入将模型检查技术应用于有限时间间隔（由用户引入）的想法变得合理。有了这个限制，我们自然会迫使表示程序行为的空间是有限的，因此模型检测算法是适用的。图的构造是一个完全自动的过程，规范.关键词：时间并发约束编程，反应式系统，模型检测1介绍时间并发约束编程（见[6]）是并发约束编程范式的扩展，增加了时间约束，1电子邮件：falaschi@dimi.uniud.it2 电子邮件：policrit@dimi.uniud.it3电子邮件：alicia@dimi.uniud.it2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。FALASCHI，POLICRITI和 VILLANUEVA2除了CCP模式。tcc模型的基本贡献在于增强了约束规划检测负信息的能力，从而提高了约束规划检测正信息的能力。 这样的负面信息对于模型反应和实时计算至关重要[4]。此外，tcc还包含了这样一种思想，即一旦检测到负面信息，就为时已晚改变过去 如果某些信息在那一刻还没有被存储，不会被储存。模型检验方法是近二十年来发展起来的一种非常成功的形式化验证方法。利用该方法，可以在模型上验证反应系统的确定的行为属性。 它是一种算法方法，可以穷举系统可达到的所有状态，并分析所有可能的行为[1，3，8，5]。模型检测有两个主要优点：它是全自动的，它的应用不需要用户监督或数学学科的专业知识（与完全演绎的技术相反），当设计不能满足所需的属性时，它会产生一个反例。我们的最终目标是描述一个环境，在这个环境中，可以将模型检查应用于tcc语言指定的系统。要在我们的方法中应用模型检查，需要执行四个基本任务：• 将系统的规范转换为几乎被模型检查工具接受的形式主义，• 利用时间的概念和变量的初始值来计算模型检查将被执行的时间间隔中的变量域（我们假设初始值和时间间隔由用户提供• 为了以适当的（逻辑的）形式表示设计必须满足的属性，• 使基于模型检查的标准自动验证机制适应我们前面步骤的输出。这可能涉及人工辅助，例如评估结果或定位错误。在本文中，我们讨论了前两个任务，特别注意模型表示的形式主义和保证其有限性的限制。事实上，我们的方法的主要特征之一在于，使用基于（声明性）约束的语言，我们可以直接从规范中构建模型集合的抽象版本此外，我们还使用（明确的）时间存在的概念，tcc来绑定变量并获得模型，在这些模型中可以经典地执行模型检查。我们所创造的，是一个无限的世界。在给定的时刻，我们考虑本质上是确定的（终止的）CCP程序的程序，而对应于不同的时间瞬间被我们强加在可变域和时间间隔上的限制所限制。FALASCHI，POLICRITI和 VILLANUEVA3|– 隐藏– 过程调用（过程调用）（声明）g：：= pt1，.，tnD：：|（）– 定义– 结合（节目）P：：={D.A}|D.D在第2节中，我们将介绍编程语言tcc，包括对其语义和主要特性的简短描述在第3节中，我们介绍了tcc结构的定义，并给出了允许我们形式化该方法的基本定义在3.3节中，我们描述了如何执行建模系统的第一步，生成一个（一个集合）有限状态模型的（有限）图表示然后，在第4节中，我们（简要地）讨论了基于用户提供的时间参数和值的限制的引入最后，我们得出结论，并评论的步骤，是完成我们框架定义的必要条件。2时间并发约束程序设计时间并发约束编程是为确定性、时间和反应式系统开发的一个简单模型。使用这个模型的声明性范式的典型优点。例如，在这种模型中编程更直观，并且使用派生语言进行推理比使用命令式语言更容易。 另一个重要的特性是，规范是可执行的，也就是说，你所证明的就是你所执行的该语言支持规范（程序）的分层和模块化结构。因为它是一种确定性语言，所以程序和规范的构造和分析更容易。在图1中，我们可以看到tcc的原始语法。（代理人）A：：=C–||||||现在c然后AnowcelseAnextAabortskip一||一– 定时积极提问– 定时否定提问– 单位延迟– 中止– Skip– 并联组成图1.一、TCC程序的扩展该语言中有两种结构：CCP（Concurrent Cons-traint Programming）结构和Timing结构. Tell、平行组合和定时积极提问是中国共产党的理论建构.这些操作符不会导致“随时间延长”。特别地，并行组合是并发性在语言中的显式表示，定时积极询问和告知允许进程同步和状态FALASCHI，POLICRITI和 VILLANUEVA4进化另一类结构是时间结构：定时否定询问、单位延迟和中止，它们会导致时间延长单位延迟强制进程在下一个时刻开始。定时否定询问（Timed Negative Ask）是单位延迟（Unit Delay）的一个条件版本，基于对否定信息的检测：如果在当前时刻的静止状态下，存储没有足够的强度来包含一些信息，则它会导致在下一时刻启动一个过程。上述运算符不允许我们将信息从一个时刻传递到下一个时刻。为此目的引入了参数询问此运算符的语法定义为X$（c→A）其中X是一组变量，c是一个条件，A是一个主体。直观地说，这个操作符的工作原理是用域X搜索一个替换，使存储中的某个约束a和c在语法上相同。如果存在这样的替换（比如说γ），则执行代理A[γ]4参数化ask的一个附加条件是，所有出现在guard中的变量c和不在X中的必须被实例化。否则代理无法执行。我们将这个操作符的操作语义定义为<$γ/<$a∈σ（Γ）<$c [γ]<$a（Γ，X $（c→B））−→（Γ，B[γ]）其中，Γ是一个代理的多重集，σ（Γ）是包含在配置Γ中的存储。我们按照[7]中介绍的符号定义了这个规则。在[6，9]中，可以找到其他可能的操作符相对于基本操作符的定义。例如，总是A，现在c然后A否则B，多优先级等待，每当c做P，做P观察c等都是使用图1所示的操作符定义的。我们总是可以把一个复杂的程序转换成一个只使用基本运算符的简单程序。 这是一个重要的-这是因为，原则上，我们只需要为基本操作符构建模型化机制。事实上，我们不会完全按照这种方式进行，但我们会留下一些操作符（例如alwaysA）不被翻译。 这样做是为了在第一个建模步骤之后获得无限状态模型的有限表示。例如，在图2中，我们可以看到一个用tcc编写的程序，它带有上面的程序计算从Init开始的一系列整数。 在它在第一个时刻产生Init值，在下一个时刻获得下一个值，依此类推。将alwaysA替换为基本运算符所需的第一步可以4用σ[γ]表示替换γ对句法宾语σ的应用FALASCHI，POLICRITI和 VILLANUEVA5V V计数器（Init，I）：：（{I：Init}||always（X，X1）$（（I：X，X1 is X +1）−→next{I：X1}））图二、例如：计数器程序。请参见图3。我们只显示第一个转换步骤，因为完整的转换将产生无限的规范。计数器（Init，I）：：（{I：Init}||（X，X1）$（（I：X，X1是X +1）→下一个{I：X1}）||always（X，X1）$（（I：X，X1 is X + 1）→next{I：X1}））图三.示例：计数器程序已转换。在下文中，我们假设使用tcc语言，该语言富含参数Ask和always操作符。图1中构造的操作语义在[7]中定义。为了给出alwaysA运算符的语义，我们在[7]中的转换系统中添加了以下规则：总是（Γ，alwaysA）−→（Γ，A，next alwaysA）我们再次遵循[7]中使用的符号来定义这个规则。3建模验证系统属性的首要活动之一是构造系统的形式化模型。这个模型应该捕捉那些将被验证的属性。反应式系统不能用它们的输入输出行为来建模：有必要捕获系统的状态，即对系统的描述我们必须建模当一个动作发生时系统的状态如何变化（系统的转换在我们的例子中，状态转换图必须从上面介绍的tcc形式主义开始构建，并且最终包含明确的时间概念。3.1基础知识为了开始我们的建模任务，我们使用经典的Kripke结构概念。这类结构能够捕获反应系统的行为，正如我们将在下面展示的那样，可以从程序的tcc变量集合ar表示变量的通用集合 V ar是出现在程序子句中的变量集，FALASCHI，POLICRITI和 VILLANUEVA6VR--→系统属性并描述程序在每个时刻的状态。ar中的变量是有类型的，其中变量的类型，如布尔型、整数型等，表示变量范围所在的域D我们基本上可以像往常一样用一阶公式来描述状态和跃迁的集合（参见。[5，2]）。在我们的例子中，唯一的区别是，现在我们表示跃迁的一阶公式（（V，VJ，T））有一个额外的参数T，表示跃迁是否对应于到下一个时刻的通道。我们的图（结构）的状态是一组约束，定义变量的值，以及一组标签，表示系统的执行点。标签是在原始程序中引入的，可以激活或禁用，这取决于系统在每个时刻的存储。如果存储允许执行与特定标签关联的操作，则该标签处于活动状态，否则将被禁用。当整个系统中存在一个活动的正常标签（可能处于另一种状态）时，表示临时操作的所有标签都被禁用。定义3.1设C是tcc语法中的约束集，L是为标记系统的原始规范而生成的所有可能标签的集合。我们将状态集定义为S2C L现在我们可以正式定义能够表示系统行为的图（结构）。定义3.2设AP是一组原子命题。 Atcc结构M是5元组M=（S，S0，T，R，L），其中(i) S是状态的有限集合。(ii) S0是初始状态的集合。(iii) T= t，n是可能的转换类型的集合。t表示时间转换，而n表示正常转换。(iv) R<$S×S×T是一个必须是全的转移关系，也就是说，对于每个状态s∈S，都有一个状态sJ∈S使得R（s，sJ，t）或R（s，sJ，n）。(v) L：S2 AP是一个函数，它用在该状态下为真的原子命题集来标记每个状态。从状态s开始的M中的路径被定义为一个（无限）状态序列π=s0s1s2. . . 证明了s0=s且R（si，si+1，X）对所有i≥0成立.现在，我们展示如何从下面的公式导出tcc结构M=（S，S0，T，R，L）：系统的TCC我们不能直接应用[2]的方法来建模系统行为，因为它们假设变量的域是有限的，因此变量的可能赋值的数量是有限的。 我们将状态集定义为系统中出现的所有限制组合的集合，并在分析具体化时构造它们。在每个州FALASCHI，POLICRITI和 VILLANUEVA7将出现表示该时刻变量的可能值的约束的集合在下文中，我们定义了一个构造，它将返回一个与给定tcc规范相关联的tcc结构的图这样的图可以简单地看作是tcc结构的图形对应物，节点表示状态，弧表示转换。为了呈现我们有两种过渡的事实（取决于R中第三个参数的值），我们将使用两种弧。静止点可以在图中识别出来，因为它们是时间过渡之前的点3.2标签标签的概念允许表示状态中的执行点。我们通过将原始规范转换为标记版本来引入此信息。这种转换包括在规范中引入与构造函数的每个实例相关联的不同标签。在图4中，我们展示了一个计算一系列整数的程序的标记版本。我们标记程序的方法类似于[5，2]中使用的方法：我们只将经典方法应用于我们的特定运算符。一个简单的算法将原始程序翻译成标记的程序。下面我们将详细介绍这一转变。设P是一个语句，它的标记版本Pl定义如下：• 如果P=c，则Pl={ l}c。• 如果P =现在c则A则Pl={l}现在c则Al。• 如果P=nowcelseA，则Pl={l}nowcelseAl。• 如果P=下一个A，则P1={ 1}下一个A1。• 如果P=中止（跳过），则Pl={ l}中止（跳过）• 如果P = A||B则P1={1}（A1||BI）。• 如果P=X^A，则Pl={ l}X^Al。• 如果P=g且g是过程调用，则Pl={l}g。• 如果P=总是A，则Pl={ l}总是Al。• 如果P=X$（c→A），则Pl={ l}X $（c→Al）。将此转换应用于Counter示例的结果如图4所示。{l0}计数器（Init，I）：：{l1}（{l2} {I：Init}||{l3}总是{ l4}（X，X1）$（（I：X，X1是X +1）→ {l5}下一个{ l6}{ I：X1}））。见图4。 示例：计数器程序标记FALASCHI，POLICRITI和 VILLANUEVA83.3图构建在本节中，我们将解释如何以自动的方式构造tcc结构程序由一组子句和一个目标组成。我们从一个初始节点开始构建，该节点被标记为代表程序目标的标签然后，我们重复一系列步骤，因为建设完成。我们定义了一系列与语言语法中定义的每个运算符相关联的操作，这些操作将在分析规范时生成图形。在每个状态中，我们通过提供可以在下一步中执行的指令的标签来表示程序的执行点。 每个标签对应于不同的并行过程，并且可以是活动的（这意味着执行与该标签相关联的操作符的条件得到满足）或禁用的（这意味着由该标签表示的操作符不能在该时刻被执行，因为存储不需要必要的条件）。重要的是要注意，时间操作（next，现在celseP等）不能在所有“正常”操作执行之前执行。 这是因为我们必须在进入下一个时刻之前到达静止状态（在当前时刻不能产生更多的信息）。只有在宁静中，我们才能确信我们拥有下一个时刻所需的所有信息粗略地说，我们的过程包括重复以下步骤（当存在活动标签时）：• 本地化将被执行的代理A（设l是关联的标签 它），• 为了执行与这种代理相关联的动作• 以确定在规范中跟随A的代理集（及其标签），• 为了将在前一步骤中获得的新标签添加到标签集合并去除标签L，• 修改上一步中定义的标签集，根据商店当我们到达一个没有活动标签的状态s时，我们就处于一个静止点。然后我们必须进入下一个时刻。为了使这段话，我们必须分析标签的标签功能的静态。首先，我们分析Next代理，然后是Negative Asks，最后是Always操作符。在图的构造中，它意味着我们通过时间转移创建与s相关的新节点t。在这样的节点中，我们引入与静止点中存在的时间代理的身体相关联的标签。存储区被设置为空存储区，执行过程如过程草图中所述继续进行。注意与always代理相关联的时间标签对于这样的标签，我们有FALASCHI，POLICRITI和 VILLANUEVA9||进行额外的验证我们在图中搜索一个等于t的前一个静态节点，如果我们找到它，那么我们将t与这样的节点联系起来并完成构造。如果没有等价节点，那么我们在节点t的标签集合中引入与always运算符相关联的标签系统的这种循环行为的存在并不能保证，它取决于系统本身。因此，为了确保图构造的有限性，我们使用（有限）时间间隔的概念。这是验证将被执行的时间间隔，然后我们取这个时间间隔的上限，如果我们到达这样的时刻，而构造正在执行，那么我们停止并获得一个仅对这个特定验证有效的模型。否则，如果我们在到达这样的时刻之前完成构建，我们构建的通用模型对系统的任何验证都有效我们现在描述每个句法结构的图的构造。• 说出去的告诉C在当前时刻向存储器添加一些信息。在我们的图构造中，它被转换为一个与执行它的节点s相关的新节点sJ我们将标签函数L（sJ）定义如下：表示存储的部分定义为s的存储加上约束c;表示新执行点的部分通过移除表示tell运算符的标签并获得指定中以下代理的标签来计算。最后，我们修改了活动和禁用的标签。• 正面提问如果c，那么P验证当前存储中的保护是否满足，如果满足，那么程序执行可以继续主体指定。在我们的图表示中，我们构造了一个新节点，其中表示标记函数的存储的部分被定义为前一个状态中的存储和代理的保护中指定的约束的并集。注意，有必要引入保护的信息，因为条件中存在的变量可能是过程的参数。然后，如前一种情况一样计算表示新执行点• 斯吉普skip不做任何操作，这意味着在图表示中，我们将创建一个新节点s，并将通过删除表示skip agent的标签并执行活动和禁用标签的修订来将标签函数L（s）定义为前驱的标签函数• 并联（A B）表示并行代理，其中A和B并行执行。它将生成不同的执行分支。在我们的图构造中，我们引入了一个与前一个节点相关的新节点，该节点继承了表示商店的标签函数的一部分。表示新执行点的标记函数部分将按照前面的情况进行计算。重要的是注意到对于一个节点，将存在与包含在其中的激活标签一样多的直接后代。FALASCHI，POLICRITI和 VILLANUEVA10→• 躲起来了该运算符表示变量对系统其余部分的隐藏。它在与隐藏操作符相关的子程序中很有用。在图形表示中，它被表示为一个新节点，其中隐藏运算符中的变量被重命名为分开。我们应用通常的方法来计算标记函数中表示执行点的部分。• 程序调用。此操作符引用规范中的另一个过程。所有过程都有不同的标签和变量。在我们的图构造中，它被创建一个新节点，在该节点上应用了对过程p的参数进行替换的替换a，并且P被引入。最后，我们修改了活动和禁用的标签。• 参数询问。X$（c A）允许将一个时刻的某些信息传递到下一个时刻。 如果条件c中的所有变量， 不包含在X中的被实例化，然后计算出使存储中的c和某个约束一致化的替换γ，然后计算代理A[γ]被处决了 在我们的图构造中，表示这种代理的标签只有在关于实例化的条件满足时才是活动的。变量是满意的。然后，我们将引入一个新的节点，它与前一个节点相关，具有正常的转移，其标记函数计算如下：首先计算所有替代Γ;然后创建一个新的代理，作为将替代Γ应用于参数询问的主体A的结果。 新的标签与这样的代理相关联，并在节点的标签功能中引入。除了表示所执行的参数请求的标签之外，使用与前一节点的标签功能相同的项目来完成标签功能。与前面的情况一样，检查标签是活动的还是禁用的。• 总是. 总是A允许我们在系统行为中模拟一个循环。在图构造中，我们通过创建一个新节点s来继续，其中表示存储的标记函数的一部分从祖先节点继承，执行点的一部分使用我们的两个过程follow和revision来计算。这些过程将产生一个与always操作符关联的临时标签（再次）和与alwaysA代理主体关联的标签。请注意，我们没有为时态代理引入任何操作，因为这些代理将导致的所有操作都将在我们到达静止点时执行。代表其主体的标签将在下一时刻的第一个节点中引入。下面的定理证明了我们的图构造的正确性。定理3.3设T是由tcc规范S用上述方法构造的tcc结构。那么构造T是正确的，因为δ（T）[[S]]其中δ是表示由序列给出的迹的函数，星号-FALASCHI，POLICRITI和 VILLANUEVA11- -从根开始，在T和[[S]]的路径中的每个tcc节点中的程序存储的t表示由第1节中讨论的规则丰富的[7]中的tcc规范S的操作语义。3.4说明性示例为了说明上一节中解释的操作，我们展示了一个编程示例的tcc结构和图构造。指定的系统计算一个整数序列（见图4）。我们把目标lg计数器（1，Sal）到这个指定，我们施加时间间隔[1， 3]。在图5中，矩形框示出了由参数化ask的每次执行生成的代码片段，其被标记为l4。4图形限制到目前为止，我们已经介绍了一种从系统的规范开始构建tcc我们已经得到了一个有限图，但它不能用经典的模型检验算法来处理：它实际上是一个无限模型集合的抽象表示。这种结构不能与经典方法一起使用的原因是我们没有将可变结构域限制为有限的。此外，需要在每个状态下都有所有变量的值，而在我们的图表示中，有些变量没有特定的as- signed值（例如，因为它取决于其他变量的值）。这个问题的解决方案是对表示引入某种限制，迫使可变域是有限的。其主要思想是，我们在进行这种转换时考虑了来自用户的信息，这些信息将被要求指定在哪个间隔内她想验证变量的初始值是什么。然后，我们分析程序，并给出一个区间的值的变量域上，这个变量可以在该时间间隔。这些值是通过考虑程序子句的结构计算的可能值的限制。我们考虑所有变量的修改，并考虑所有增量和减量动作以及数据依赖性，我们获得最大值和最小值。当然，不一定达到这些值。 有限域以不同的方式处理，因为没有必要限制它们。定义4.1[域限制]设V∈V是程序P的变量集，V ∈V是具有无穷域的变量集.设tI，tF∈N，tI，tF≥0，初始时刻tI≤tF，则我们定义：• valt（V）表示在时刻t的变量值的集合。FALASCHI，POLICRITI和 VILLANUEVA12图五、计数器程序的tcc结构• valtI（V）作为用户定义的初始变量值集。• valmax（V）表示变量可以达到的最大值的集合• valmin（V）是变量可以达到的最小值的集合• analyze（S，valtI（V），tI，tF，valmin，valmax）作为计算在这样的时间间隔内的valmax（V）和valmin（V）的函数，其中S是从规格P获得的tcc使用这些新值，我们将变换图形表示，以获得用户引入的时间间隔内系统行为的有限表示，并从用户定义的变量的初始值开始l3 a1l6初始化：1溶L1索尔：我Al3L4a1l6SL3初始化：1溶L2L3索尔：我Al3L4一：2人初始化：1溶I：1l3初始化：1索尔：我L2Al3L4溶液：Ial3 X：2X1：3 a2l5I：2初始化：1溶胶：I I：1Al3L4索尔：我L3a2l6初始化：1溶胶：I I：1X：1 X1：铝合金Sol：Ial3L4a2l6SL3索尔：我Al3L4一：3人索尔：我Al3X：3 X 1：4I：3A3L5a1 l5下一个a1 l 6{I：2}FALASCHI，POLICRITI和 VILLANUEVA13经典方法和我们的方法之间的主要区别在于，在经典方法中，在系统的定义中引入了对可变域的限制，而在我们的框架中，我们可以指定具有无限可变域的系统并构造相应的图结构。然后，我们有一个基本的结构，我们只需要在每次用户想要执行模型的时候进行图形限制，并引入必要的信息。5结论我们定义了一种自动转换，它以tcc程序作为输入，并将系统行为的表示作为图结构返回。经典的模型检测方法不能应用于本文所构造的图结构，因为经典著作中构造的Kripke结构与本文所构造的tcc结构存在一定的差异。主要的区别是我们引入了两种状态转换。在经典方法中，状态之间的转换表示时间的增加，而在我们的框架中，正常转换在同一时刻改变状态。只有在执行定时转换时，时间才会增加。这引入了同步原语，因为要执行定时操作的进程必须等到所有其他进程完成其正常操作。经典的方法是异步的，因为它们认为所有并行进程都是相互独立的，因此它们可以在不等待其他进程计算的任何信息的情况下执行。我们通过以下事实来确保我们的建筑的有限性。在每个时刻，我们的语言类似于（终止）确定的CCP，所以每个图都是有限的。此外，对于不同的时刻，我们通过考虑时间间隔对可变域施加限制来确保有限性。注意与Clarke等人的工作的相似之处。[2]事实上，当他们强制并行操作的所有过程可以在同一时刻完成时，他们引入了一些同步。这项工作的主要贡献是介绍了一种方法来验证TCC中指定的反应系统的属性。这种语言是一种声明性语言，但在其语义中内置了时间的概念，这就是为什么我们可以为用户提供的给定时间间隔定义一个模型时间间隔的原因。 由此产生的方法非常强大，因为它利用了 使用约束语言进行编程并因此确保有限性的事实不需要对语言的表达性施加严格的限制。这个项目的第二部分将处理表示用户想要验证的属性。我们计划以类似于Clark等人的方式在这一步的基础上进行形式化。[2]的文件。随后，我们的目标将是处理如本文所述的结构，以产生标准（等效）有限KripkeFALASCHI，POLICRITI和 VILLANUEVA14结构将作为模型标记器的输入。为此，需要解决的主要问题是循环的（有限）展开和将定时转换减少到不定时（标准）转换。引用[1] Clarke，E.，O. Grumberg和D.E. 龙，模型检验，Springer-VerlagNatoASI系列F152（1996）。[2] Clarke，E.，O. Grumberg和D.Peled，[3] Clarke，E. M.，E. A. Emerson和A.李国忠，有限状态并发系统的时序逻辑验证，北京：计算机科学出版社，1998.244-263。[4] Henzinger，T.，Z. Manna和A.Pnueli，Timed transition systems，in：J. de Bakker，K. Huizing，W.- P. de Roever和G. Rozenberg，editors，Real Time ： Theory in Practice ， Lecture Notes in Computer Science600 ，Springer-Verlag，1992 pp. 226-251[5] 曼纳角，巴西-地和A.Pnueli，《安全》，[6] 弗吉尼亚州萨拉斯瓦特，R. Jagadeesan和V.Gupta，时间并发约束编程，在：S。Abramsky，editor，Proceedings of the Ninth Annual IEEE Symposiumon Logic in Computer Science（1994），pp.71比80[7] 萨 拉 斯 瓦 特 河 谷 一 、 R. Jagadeesan 和 V.Gupta ， Programming in TimedConcurrent Constraint Programming ， in ： B.Mayoh ， E. Tyugu 和 J.Penjaam，编辑，约束编程：1993 NATO ASI Parnu，爱沙尼亚，SpringerVerlag，1994，pp. 361-410[8] Sipma，H.B、T. E. Uribe和Z.Manna，演绎模型检验，在：R。Alzheimer和 T. Henzinger ， editors ， Computer-Aided Verification ， 8th InternationalConference（CAV209-219[9] V.A.Saraswat，R.Jagadeesan和V.Gupta，定时缺省并发约束编程，符号计算杂志22（1996），pp.475