理论计算机科学电子笔记246（2009）131-145www.elsevier.com/locate/entcs生成tccp执行符号表示的工具1Alexei Lescaylle2 Alicia Villanueva3DSIC，UniversidadPolit′ecnicadeValenciaCaminode Vera s/n，46022瓦伦西亚，西班牙摘要时间并发约束语言（Timed Concurrent Constraint Language，tccp）是由F. de Boer等人，作为并发约束范式（Saraswat，1993）的扩展，用于指定反应式和嵌入式系统。在本文中，我们描述了StructGenerator系统，该系统给出了tccp程序的规范，一种对这种tccp程序的行为进行建模的符号表示（tccp结构）。由此产生的结构允许一个验证程序通过使用模型检查算法。它类似于Kripke结构，但由于ccp模型的性质，它在一些重要的方面不同于经典方法，这些将在本文中描述。 StructGenerator系统用C++实现，它将包含tccp程序规范的文件作为输入，并生成相关的tccp结构。在本文中，我们介绍了StructGenerator的设计和实现。我们还展示了它的功能执行两个实际的例子。保留字：时间并发约束程序设计，符号表示，工具演示。1引言并发约束范式（简称ccp）[10]是一个简单但强大的模型，它基于存储作为约束的概念，而不是经典的存储作为赋值的概念。因此，计算模型是基于由约束条件的结合而不是被定义为变量的估值组成的状态。时间并发约束语言（TimedConcurrent Constraint Language，简称tccp）作为ccp的扩展在[4]中引入，用于以直观的方式描述反应式系统。作者在语言语义中引入了时间的概念，并引入了新的代理来处理负面信息，即，信息不存在于1这项工作得到了西班牙MICINN的资助，资助号为TIN 2007 -68093-C 02 -02、HA 2006 -0007，并得到了联合国艾滋病规划署（UNIVER S ID DDPOliEEVALENCIA DD-06-07TACPAS）的支持。2电子邮件地址：alescaylle@dsic.upv.es3 电子邮件地址：villanue@dsic.upv.es1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.019132A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131the system.在反应式系统中，对超时或抢占等行为进行建模时需要负信息在过去的几年中，并发和反应系统的验证技术得到了广泛的发展。模型检查技术[5]是一种形式化的技术，它允许人们验证模型是否满足一个属性。这种技术支持了所谓的状态爆炸问题，这促使许多优化方法的发展，以减轻它。我们可以在文献中找到许多基于抽象解释，偏序，符号表示等不同建模和（片段）编程语言的优化。一般的ccp框架，特别是tccp语言，由于存储为约束的方法，象征性地表示经典状态集作为约束的连接，从而实现搜索空间的自然压缩。请注意，这一事实并不妨碍我们应用其他优化技术，如[1，2]。在[6]中提出了一种tccp的模型检查算法，该算法给出了一个tccp程序，将其转换为符号表示（tccp结构），该符号表示是验证阶段的输入。 [6]中的建议类似于经典的一是以tccp结构为中心，发挥克里普克结构的作用。 然而，正如我们稍后将展示的，tccp结构在一些重要的方面不同于Kripke结构，因此验证算法必须重新制定并适应ccp模型。在本文中，我们提出了StructGenerator，一个自动构造tccp结构的系统，给出了tccp程序的规范。该构造算法在某些方面不同于传统的构造算法。[6]中提出的一种方法，其中纳入了[3]中的一些概念，使技合方案框架更加灵活。本文的结构如下。第二节简要介绍了tccp语言。第3节描述了tccp结构的概念，提出了处理ccp模型的主要困难。在这一节中，我们还展示了如何实现tccp结构的构造。第4节通过开发两个运行示例展示了如何使用该工具，最后，第5节结束。2TCCP语言时间并发约束语言（Timed Concurrent Constraint Language，tccp）是在[4]中定义的并发声明性语言，作为并发约束编程范式（ccp，[10]）的扩展。在ccp模型中，存储作为赋值的概念被存储作为约束的概念所取代。计算模型基于（1）一个全局存储，其中累积了约束，以及（2）一组可以通过存储与其他代理交互的代理。CCP模型是不确定的，没有时间定义的概念。直观地说，ccp程序的执行是通过向存储器询问和告知信息来进化的。它是一个简单但功能强大的模型，其中部分信息可以很容易地处理。tccp的时间扩展在语义中引入了时间的概念，即，没有时间流逝的特殊代理被定义。然而，一个能够处理负面信息的新代理（A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131133条件代理）。我们可以在文献中找到CCP时间扩展的其他方法，这些方法可以做出不同的设计选择[11，7，9]。在tccp中，程序的执行也是通过向存储器询问和告知信息来进行的，但是这次这些动作消耗时间。在实践中，这意味着咨询和更新商店都需要时间。最后，我们注意到，它是不可能的，从存储中删除信息，因此不同于其他扩展，存储行为单调。该模型是参数w.r.t.一个圆柱约束系统C在[4]中被定义为一个结构C，≤，H，真，假，Var，Var，其中H是一个lub操作，真和假是C的最小和最大元素，Var是一个可数的变量集，Var是一个关于变量的圆柱操作。有关约束系统的详细信息，请参见[4，10]。正如我们之前所说，tccp语言被定义为对反应式或嵌入式系统进行建模。在这些系统中，信息的缺失会导致一个动作的执行，这促使了新的条件代理w.r.t.的引入。CCP模式。让我们简单回顾一下tccp的语法[4]：卢恩A：：=跳过|告诉（c）|i=1 ask（ci）→ Ai|现在c然后A else A|一||一|xA|p（x）其中c，c，i是有限约束（即，原子命题）的C.一个tccp程序P是一个形式为D.A的对象，其中D是一组形式为p（x）：-A的过程声明，A是一个agent。 直觉上，跳过代理完成了不做任何事情来处理;tell（c）将约束c添加到存储中;选择代理卢恩i=1ask（ci）→Ai非确定性地执行（在接下来的时刻）一个Ai的代理，只要它的守卫ci满足。如果没有条件ci，选择代理暂停;条件代理（现在是c，然后是A 1，否则是A 2）如果存储满足c，则执行A 1，否则执行A2; A 1 ||A 2并行执行两个代理A 1和A 2（使用的并发模型是最大并行性）;Aagent用于定义进程A的局部变量x;最后，p（x）是过程调用代理，其中x表示进程p的参数集。代理通过全局时钟进行同步。在tccp的语义中，消耗时间的代理只有tell、choice和过程调用代理。原始tccp执行模型[4]中的存储可以看作是一块黑板，在那里信息被不断地写入，永远不会被取消。存储单调增长，因此不可能更改给定变量的值我们可以使用流来模拟变量值随时间的演变。这允许我们处理命令风格的变量。为了以更简单的方式检索关于信息被添加到存储的顺序的[3]提出了一种新的计算模型，其中结构化存储替代了经典的存储概念StructGenerator系统考虑了这种新的计算模型。直观地说，结构化存储[3]由存储的时间序列sti组成，其中每个存储包含在第i个时刻添加的信息。像蕴涵这样的概念必须被修改，以获得一个尊重tccp原始语义的模型。134A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）1313tccp执行的符号表示在[6]中，在定义模型检查算法的背景下，提出了一种用于建模tccp迹线的图结构（tccp结构）。这种结构可以被看作是克里普克结构的一个变体，其中，在ccp模型之后，作为变量赋值的状态的概念被作为约束的结合的状态的概念所取代。 这意味着tccp结构中的节点可以表示Kripke结构的一组经典节点。StructGenerator系统实现了这种结构的构造。正如我们将展示的，这种构造的主要困难来自于tccp存储的单调性。此外，无论是在构建tccp结构阶段，还是后来的验证阶段，我们都必须考虑到，与经典方法不同的是，存储中某些信息的缺失并不（必要）意味着该信息的否定成立。让我们简单地描述一下符号表示。tccp结构的状态包含一组原子命题;更具体地说，它由来自tccp中底层约束系统的一组原子约束组成。tccp结构的每个状态还包含一组表示当前执行步骤的标签这些标签与tccp程序中的每个座席唯一关联。请注意，需要一个标记程序的预处理。标签允许我们设置那些必须在下一个时刻执行的代理由于在程序执行期间，存储单调增长，通过定义，并且不同于经典方法，不可能有两个语法上相等的状态。这意味着为了定义执行的有限表示，需要状态之间的等价概念（这最终将决定图结构中的循环）。 这个概念对于有一个有限的构造算法也是必要的。非正式地，我们说两个状态是等价的，如果（1）两个状态中的标签集一致，并且（2）一个状态中的约束集等价于第二个状态中的约束集模重命名[6]。为了处理流等价，我们使用当前值的概念（即，流的最近增加的值[3]）来设置流在两个状态中是否相等。请注意，定义流的约束的数量总是在增加（因此我们永远不会有两个状态在语法上相等），但是，遵循命令式的变量概念状态等价的定义允许我们克服由tccp存储的单调行为引起的算法终止的问题。记住，tccp是用来模拟反应系统的。在对算术功能进行建模的情况下，通常不能确保终止。3.1执行StructGenerator是用C++实现的。它由大约3100行代码组成每个类处理tccp的一个实体（代理、约束、声明、存储、状态、. . .）.我们决定实施A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131135系统，因为我们需要将它连接到一些约束求解器，并且我们发现已经为该语言定义了一些接口来简化这些连接此外，我们必须处理复杂的数据结构，因此C++为我们提供了定义类和构造类的能力。正如我们上面所说的，StructGenerator系统以一种自动的方式构造已经描述过的tccp结构，因此它旨在以一种符号化的方式表示tccp程序的行为。文[6]中提出了一种构造这种结构的算法.我们遵循了该算法的主要思想，但是，如上所述，我们决定通过使用[3]中更灵活的计算模型来细化一些定义，这使我们能够更容易地处理流。直观地说，实现将经历以下阶段。首先，给定文本文件中tccp程序的指定，系统解析程序，其中每个代理的出现都用不同的标签标记。此后，建立初始状态，并从每个初始状态，我们构造从这样的状态达到以下语言的语义的状态。状态被生成，但直到确认才被引入结构中。当检查结构中是否存在等效节点时，即可实现确认。 让我们描述每个节点的生成过程。对于每个新状态迭代地执行该生成过程（最初对于初始状态）：1 为了生成遵循语言语义的节点的可能后继，2 为了检查对于每个可能的后继是否存在等效节点3 确认在新节点结构中的引入(a) 如果不存在等效节点，则将后继节点添加到tccp结构中(b) 在存在等效节点的情况下，使两个状态等效的所计算的重命名与连接原始节点和等效节点的边相关联。后继节点被丢弃。当所有的节点都被处理以生成后继节点时，迭代过程结束构造的关键点是第二和第三阶段，在那里我们寻找等效节点。正如我们之前所说，这一步对于（部分）确保算法的终止至关重要如图1所示，StructGenerator系统被构造成2个模块，程序解析器和构造过程。 程序解析器模块将包含程序规范的文件作为输入。然后，通过使用辅助过程Declaration Parser和Agent Parser，生成数据结构Declarations，它存储所有程序信息：Agent、约束、标记等。生成的信息声明是构造过程模块的输入，构造过程为此，它使用了与上述迭代过程中的第一阶段相对应的节点创建过程。简而言之，它通过使用三个辅助函数来构造结构的状态136A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131user@pcname：$StructGenerator输入tccp程序的文件名（*.tccp或 *.txt）：.. . 微波错误. txt.....创建声明的图形：微波错误- 创建状态的子项：1- 创建国家的孩子：2- 创建国家的孩子：3- 创建国家的孩子：4.tccpStructGen规范一个给定的tccp程序（档案）建设过程程序解析器结构的给定的TCCP程序..................输入...........................输出声明剂解析器宣言解析器节点创作找到如下即时图1.一、StructGenerator框架第四步，跟随并发现。Intuerity、instant和follows遵循tccp语义计算（1）代理可以在某个时刻添加的约束，以及（2）必须在下一个时刻执行的代理。换句话说，它们计算新节点的内容（标签和约束）。find是在如上所述的结构中查找等效节点的函数。我们工具的界面是控制台引导的。要运行该工具，我们必须输入StructGenerator命令。然后，系统要求用户输入文件名，编写tccp程序的规范图二是简单执行。图二. StructGenerator运行[4]感兴趣的读者可以在[6]中找到原始瞬时的定义，并遵循函数。A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131137{ld}微波错误（门、按钮、错误）：-{le0} D，B，E（{lp1}（{lt2}tell（Error=[|E]）{lp 3}（{lt 4}告诉（门=[|D]）{lp 5}（{lt 6}告诉（按钮=[|B]）{lp 7}（{ln 8}现在（门=[打开|D]按钮=[开|B]）然后{lp 9}（{le 10} E1（{lt 11}告诉（E=[是|E1]））{le 12}关闭B1（{lt 13}告诉（B=[关闭|B1]）其他{le14} E1（{lt15} tell（E=[no| E1]））{lc 16}微波误差（D，B，E）。图3.第三章。tccp中的微波错误声明。4实例在本节中，我们将介绍两个实际示例。第一个是微波炉控制器的（部分）规范，我们从[6]中借用。第二个是[1]中使用的调度器示例的规范，以驱动模型检查 器 的 符 号 版 本 。 我 们 首 先 提 供 并 发 系 统 的 tccp 规 范 ， 然 后 提 供 由StructGenerator生成的tccp结构。我们还以图形方式显示节点之间的连接。4.1微波误差系统图3.给出了系统的tccp规范为了更清楚地说明规范和生成的图之间的标签显示在大括号{}内。过程声明微波错误模拟了在系统打开的同时检测微波炉门何时打开的过程。这种情况由条件代理ln8控制。在条件保持的情况下，该过程强制（利用告知代理lt13）微波在下一时刻被关闭。请注意，告知代理是在同一时间执行的。当检测到错误时的时刻，但是被告知的约束仅在随后的时刻对其他人此外，必须发出错误信号（代理lt11）。如果条件不成立，则程序发出（通过另一个告诉代理LT 15）将在全局存储器中可用的无错误信号时间瞬间之后。这些信号可以被其他进程捕获，因此可以看出存储允许进程的同步接下来，我们展示了在执行结构生成器时获得的符号表示，输入微波错误（的非标记版本）。目前，输出以文本方式显示，列出图结构中的状态集以及状态之间的关系。对于所考虑的系统，生成7个状态。 每个状态包含一个标识符，例如状态1。在这种情况下，状态1包含：138A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131• 一组约束：yes（Door=[d（open）|D]和按钮=[b（on）]|B]），• 一组标签：LT 2-微波错误，LT 4-微波错误，LT 6-微波错误，. 、• 一组定义变量：门、按钮、错误、E1、B1、D、B、E和，• 最后，看看孩子们的部分，我们可以说状态1与状态3和状态4，边缘上没有定义重命名已成功创建图表.....--tree：0-> called：microwaveerror---- state0--constraints：（true），标签：ld-微波错误，变量：门，按钮，错误，儿童：在树：0->状态：1-重命名：在树：0->状态：2-重命名：--状态1--约束：是（门=[d（打开）|D]和按钮=[b（on）]| B]），标签：lt 2-微波错误，lt 4-微波错误，lt 6-微波错误，lt 11-微波错误，lt 13-微波错误，lc 16-微波错误，变量：门，按钮，错误，E1，B1，D，B，E，孩子们：在树：0->状态：3-重命名：在树：0->状态：4-重命名：--状态2--约束：不（Door=[d（open）|D]和按钮=[b（on）]| B]），标签：lt 2-微波错误，lt 4-微波错误，lt 6-微波错误，lt 15-微波错误，lc 16-微波错误，变量：门、按钮、错误、E1、D、B、E、子项：在树：0->状态：5-重命名：在树：0->状态：6-重命名：--状态3--约束：（错误=[e（）|E]），（Door=[d（）|D]），（Button=[b（）|B]），（E=[e（是）|E1]），（B=[b（of f）|B 1]），是（D=[d（open）|D′]和B=[b（on）]| B']），标签：lt 2-微波错误，lt 4-微波错误，lt 6-微波错误，lt 11-微波错误，lt 13-微波错误，lc 16-微波错误，变量：门，按钮，错误，E1，B1，D，B，A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131139E，B1'，E1 '，D '，B '，E '，孩子们：140A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131在树中：0->状态：3-重命名： E/错误，在树中：0->状态：4-重命名： E/错误，--状态4--约束：（错误=[e（）|E]），（Door=[d（）|D]），（Button=[b（）|B]），（E=[e（是）|E1]），（B=[b（of f）|B1]），not（D=[d（open）|D′]和B=[b（on）]| B′]），标签：LT 2-微波错误，LT 4-微波错误，LT 6-微波错误，LT 15-微波错误，LC 16-微波错误，变量：门、按钮、错误、E1、B1、D、B、E、B1在树中：0->状态：5-重命名： E/错误，在树中：0->状态：6-重命名： E/错误，--状态5--约束：（错误=[e（）|E]），（Door=[d（）|D]），（Button=[b（）|B]），（E=[e（否）|E1]），是（D=[d（打开）|D ′]和B=[b（on）]| B ']），标签：lt 2-微波错误，lt 4-微波错误，lt 6-微波错误，lt 11-微波错误，lt 13-微波错误，lc 16-微波错误，变量：门，按钮，错误，E1，D，B，E，孩子们：在树中：0->状态：3-重命名： E/错误，在树中：0->状态：4-重命名： E/错误，--状态6--约束：（错误=[e（）|E]），（Door=[d（）|D]），（Button=[b（）|B]），（E=[e（否）|E1]），而不是（D=[d（打开）|D ′]和B=[b（on）]| B']），标签：lt 2-微波错误，lt 4-微波错误，lt 6-微波错误，lt 15-微波错误，lc 16-微波错误，变量：门、按钮、错误、E1、D、B、E、E在树中：0->状态：5-重命名： E/错误，在树中：0->状态：6-重命名： E/错误，在这个例子中，由于只有一个过程声明，所以只生成了一个树。我们可以看到这个事实，因为所有节点都在树：0中。系统生成的树与程序中的声明一样多注意，某些关系，例如状态0到状态1和状态2的关系，没有重命名。重命名A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131141只有在建立循环时才与关系相关联。我们可以图形化地观察图4 -5中生成的结构中节点之间的关系。见图4。 生成的tccp结构中节点之间的关系直观地说，状态1表示程序中的条件成立（因此发生错误）的情况，而状态2表示条件不成立的情况。现在考虑状态2。 该状态与状态5和状态6相关。 这些状态与已经存在的节点相关：状态5移动到状态3和4。 这意味着状态5的后继者与这些状态等价（遵循上面非正式给出的在这些情况下，使状态相等的方法。4.2构建系统为了说明如何为每个声明生成一个树，我们在图中显示。5.引用[1]的tccp程序示例的标记版本它由两个谓词组成。第一个是建造，它模拟了建造房屋过程中三个不同任务的持续时间。它5 该图没有显示与每个循环边相关的重命名。状态0状态1状态3状态2状态4状态5状态6142A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131谓词get约束。 并行地，询问代理检查三个变量的值是否被实例化为整数，并且在这种情况下，表示调度限制的几个约束被添加到存储。最后递归调用建筑过程，使我们能够重新计算计划进度。谓词get约束更简单，因为它只是将不同任务持续时间的值添加到存储中。{ld} 构建（[PD| PD']、[PT| PT ']、[PE| PE ']、[PA| PA']） ： -{le 0}获取D1，T1，E1（{lp 1}（{lx 2}获取约束（D1，T1，E1））{la3}ask（atom（D1）and atom（T1）andatom（E1））→{lp 4}{lt 5}（告诉（PD+D1= PT））{lp 6}{lt 7}（告诉（PT+T1= PE））{lp 8}{lt 9}（告诉（PE+E1= PA））{lc10}build（PD '，PT'，PE '，PA'）。{ld}获取约束（W1，I1，P1）：-{lp 0}{lt 1}（告诉（W1））{lp 2}{lt 3}（告诉（I1）{lt4} tell（P1）。图五. tccp中的生成执行StructGenerator后得到的结构如下所示注意，在状态1中，标签集合包含到过程调用代理lx2的标签。状态1链接到节点状态2和状态3，如可以观察到的，其在获取约束声明和构建声明中具有来自代理的标签。已成功创建图表.....--tree：0->called：build---- state0--constraints：（true），labels：ld-build，变量：PD、孩子们：在树：0->状态：1-重命名：-- state1--constraints：（true），标签：lx 2-build，la 3-build，变量：PD、孩子们：在树：0->状态：2-重命名：A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131143在树：0->状态：3-重命名：--状态2--约束：（true），yes（atom（D1）and atom（T1）and atom（E1）），标签：lt1-get constraints，lt3-get constraints，lt4-get constraints，lt5-build，lt7-build，lt9-build，lc10-build变量：PD、孩子们：在树：0->状态：4-重命名：-- state3--constraints：（true），不是（原子（D1）和原子（T1）和原子（E1）），标签：lt 1-get约束，lt 3-get约束，lt 4-get约束，la 3-build，变量：PD、孩子们：在树：0->状态：5-重命名：在树：0->状态：6-重命名：--状态4--约束条件：（D1）、（T1）、（E1）、（PD+D1= PT）、（PT+T1=PE）、（PE+E1= PA），标签：lx 2-build，la 3-build，变量：PD、孩子们：在树中：0->状态：2-重命名：--状态5--约束：（D1），（T1），（E1），yes（atom（D1）and atom（T1）and atom（E1）），标签：lt 5-build，lt 7-build，lt 9-build，lc 10-build，变量：PD、孩子们：在树中：0->状态：4-重命名：PT/PD，T1/D1，PE/PT，E1/T1，PA/PE，--状态6--约束：（D1），（T1），（E1），不是（atom（D1）和atom（T1）和atom（E1）），标签：la 3-build，变量：PD、孩子们：在树中：0->状态：5-重命名：在树中：144A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）1310->状态：6-重命名：A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131145--tree：1->called：get constraints---- state0--constraints：（true），标签：ld-get约束，变量：W1、I1、P1，子项：在树：1->状态：1-重命名：-- state1--constraints：（true），标签：lt 1-get约束，lt 3-get约束，lt 4-get约束，变量：W1，I1，P1，孩子们：在树中：1->状态：2-重命名：--状态2--约束：（W1）、（I1）、（P1），标签：变量：W1、I1、P1，儿童：在图6中，我们用图形表示系统状态之间的关系。 状态2表示当ASK代理的条件成立时的情况，而状态3表示当条件不成立时的情况。 状态2与状态4相关，状态4又与状态2相关，并且还与状态3相关。这是由于执行了过程调用代理lc 10-build，它对构建过程的递归调用进行建模。 第二棵树表示谓词get约束，描述将相应变量添加到存储器的过程的5结论和今后的工作在本文中，我们介绍了StructGenerator系统，它给出了tccp程序的规范，构 造 了程序 所 有 可 能 执 行 集 的 符 号 表 示 。该 系 统 可 在 网 址http://www.dsic.upv.es/~villanue/tccp-StructGenerator/。与尊重到在符号表示中，tccp结构可以被看作是克里普克的变体结构，其中节点的概念适用于ccp框架，并且与经典方法不同，重命名可以与某些边相关联。由于tccp模型，这种符号表示的构造变得不平凡，因为由于存储的单调行为，我们必须处理无限多组状态。为了避免这个问题，使用了状态之间等价的概念，结合使用流的当前值，146A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131见图6。 生成系统中节点之间的关系来实现一个有限的生成过程。作为未来的工作，我们计划在这个工具中考虑最近在[8]中提出的新代理我们还计划使模型检查算法适应这个新框架（包括新的代理，并在[3]的结构化计算模型中制定）。注意，StructGenerator生成的tccp结构有足够的信息作为模型检查工具的输入。最后，我们希望通过自动显示节点之间关系的图形版本来改进工具的界面引用[1] M.阿尔蓬特湾Falaschi和A.维拉纽瓦tccp程序的符号模型检验器。在Proceedings of the InternationalWorkshop on Rapid Integration of Software Engineering techniques（RISESpringer Verlag，2005.[2] M. Alpuente，M.M. Gallardo，E. Pimentel和A.维拉纽瓦tccp程序抽象模型检测的语义框架。理论计算机科学，346：58[3] M. Alpuente，M.M. Gallardo，E. Pimentel和A.维拉纽瓦 TCCP验证的实时逻辑。Journal of Universal Computer Science，12（11）：1551[4] F. S. de Boer，M. Gabbrielli和M. C. Meo.一种时间并发约束语言。 信息与计算，161：45[5] E. M. 克拉克湖，澳-地Grumberg和D.佩尔德。模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。树0状态0树1状态1状态0状态2状态1状态3状态2状态4状态5状态6A. Lescayille，A.Villanueva/理论计算机科学电子笔记246（2009）131147[6] M. Falaschi和A.维拉纽瓦 时间并发约束程序的自动验证。逻辑程序设计的理论与实践，6（3）：265[7] 古普塔河Jagadeesan，V. A. Saraswat和D. G.博布罗混合约束语言编程。在Hybrid Systems II，LNCS的第999，第226Springer Verlag，1995年。[8] A. Lescaylle和A.维拉纽瓦使用tccp规范和验证通信协议。在第16届函数和（约束）逻辑编程国际研讨会（WFLP'07）的会议记录中[9] M.尼尔森角Palamidessi和F. D.瓦伦西亚时态并发约束程序设计：表示、逻辑与应用，2002。[10] V. A.萨拉斯瓦特并发约束编程语言。麻省理工学院出版社，马萨诸塞州剑桥，1993年。[11]V. A.萨拉斯瓦特河Jagadeesan和V. Gupta。时间并发约束编程的基础。在第九届IEEE计算机科学逻辑年会论文集，第71-80页。IEEE Computer Press，1994.
我的内容管理
展开
