ABEL硬件描述语言的Maude重写逻辑语义及硬/软件协同设计分析

理论计算机科学电子笔记176（2007）47-60www.elsevier.com/locate/entcsABEL的重写语义及其在软硬件协同设计与分析MichaelKatelmanandJos'eMeseguer1伊利诺伊大学厄巴纳-香槟分校计算机科学系厄巴纳，伊利诺伊州61801，美国。摘要提出了ABEL硬件描述语言的Maude重写逻辑语义。基于这种语义，并在Maude的底层LTL模型检查器，我们提出了一个可扩展的形式化分析框架和工具的硬件/软件协同设计。分析方法是基于对LTL时序逻辑公式的有限系统行为的跟踪检查。硬件、嵌入式软件以及两者之间的交互的形式属性都可以通过这种方式进行分析。我们提出了两个案例研究说明我们的方法和工具。关键词：协同验证，协同设计，重写逻辑，程序语义，硬件描述语言，Maude1引言嵌入式系统所需的有限功能类别表明其硬件和软件组件可能同时设计，通常称为硬件/软件协同设计[18]。协同设计的典型目标比通用微处理器要有限得多：它通常是嵌入式系统，例如在消费电子产品或各种控制系统中发现的嵌入式系统，例如在汽车或发电厂中发现的嵌入式系统。许多应用的一个重要的最近趋势是朝向具有它们自己的通信资源并且通过无线网络连接的分布式嵌入式系统。就规模而言，这类系统的数量现在使标准计算机的数量1电子邮件：{katelman，meseguer}@ uiuc.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.00748M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47协同设计工程是一个复杂的过程，远远超出了简单地将任务分配给适当的工程师。协同设计过程中的一个关键步骤，虽然不一定是第一步，是将系统划分为主要功能块，然后将这些功能块与特定的设计技术相匹配。 具体地，做出关于哪些组件将被实现为硬件以及哪些组件将被实现为软件的决定。 在此期间做出的选择 这一步直接影响到系统实现的成本和复杂性，以及实现的性能。例如，需要计算傅立叶变换的系统可以选择在通用微处理器上的软件中，在数字信号处理器（DSP）上的软件中，或者直接在硬件中作为专用集成电路（ASIC）的一部分嵌入式系统设计的当代研究[22，13，7]提倡对上述过程进行重大更改，其中主要功能首先在高级别建模DSP或ASIC。建模是通过一系列形式主义来实现的，各种通信、并发和计算方案。例如，在托勒密II系统设计环境[13]中，工程师可以使用许多支持模型的组合来描述计算，包括数据流网络和离散事件模型。通过将功能与实现分离，诸如Ptolemy II之类的工具试图协调系统设计过程，并通过利用模块化和抽象更快地生成验证设计。在有限的情况下，自动化工具已经能够直接从这些高级模型生成实现。1.1嵌入式系统验证我们对协同验证的看法，即协同设计被验证的过程和机制，由图1所示的概括图总结1.一、 视所适用的特定核查制度和核查级别而定，系统的组成部分进行了描述，可以更具体地解决各个框。在本文中，我们专注于实现级设计的共同验证，特别是我们专注于在这个级别上的硬件/软件交互。我们认为这项工作是一个更长期和更雄心勃勃的项目的一部分，以-主要指定和分析嵌入式系统，特别是系统关于图1，我们需要一个自然的硬件模型来捕获实现级设计。寄存器传输级（RTL）代码是最普遍和自然的选择，包括众所周知的硬件描述语言（HDL）（子集），如Verilog和VHDL。然而，对于本文中的工作，我们选择了另一种语言ABEL[24]，该语言由Xilinx Inc.拥有。并且主要用于对FPGA编程，FPGA是嵌入式系统中广泛使用的技术。 对于能够在ABEL设计的硬件组件上“运行”的软件，它必须处于硬件可以理解的级别，因此我们专注于我们软件模型的汇编语言编程。作为汇编代码一部分所允许的确切格式和指令集必须根据特定M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）4749Fig. 1. 共同验证概述微处理器是它的目标。 因此，在分析新的微处理器组件时，必须更新验证环境以支持新的指令集。图中的最后一个组件。 1是保留用于指定什么应该是veri- 在我们的例子中，这将是RTL微处理器和在这些处理器上运行的汇编语言程序的属性。 有很多兴趣- 关于这些系统的属性只能用跨越硬件、软件和软件及其数据结构的元级属性的属性来描述。本文的目标是展示重写逻辑可以用来统一属性所需的不同级别的自然方式。来描述它们，这样它们就可以一起推理。为此，我们提出了一个基于Maude的协同验证环境。我们的环境支持的特定验证方法是一种非常实用的形式分析，即跟踪检查，这是一种广泛用于验证硬件[4，1，6]和软件[11，19]的形式方法。在跟踪检查中，表示为时态逻辑公式的形式属性被检查系统的有限跟踪或运行。这样做的实际好处是节省了建造自检测试台所需的工程费用它可以帮助验证工程师专注于属性，而不是如何检查它们。本文的其余部分组织如下。第2节通过ABEL的方式介绍了如何在Maude中指定硬件描述语言的语法和语义的高级概述。 第3节详细解释了我们的框架用于指定和跟踪检查的协同设计，并通过两个深入的案例研究说明了我们提出的方法。第4节讨论了相关工作，第5节提出了一些结论。50M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47§§模块“DFFE”声明’D, ’EN方程’Q当其他'OUT =.Z. ;端模图二. 示例模块和电路图2ABEL语言的结构和语义这一节给出了我们的ABEL语义的一个高层次的概述，重点是主要的设计决策，而不是ABEL的特定细节。 在具体性可以更快地表达观点的地方，我们使用ABEL语法并解释必要的细节。许多不同类型的编程语言的重写语义已经在前面描述过（例如参见[15]）。本节的目标部分是解释RTL语义中与软件语言不同的那些领域。我们的第二个目标，事实上，从第一个目标中掉出来，是提供足够的语义细节来支持我们在3中对跟踪检查的讨论。 最后，通过ABEL， 我们还表明，在3中提出的框架将允许硬件设计者以符合当前工程实践的方式构建数字电路2.1电路语义同步数字电路需要尊重两个独立的执行顺序概念。首先，在每个时钟周期内，必须考虑组合（非状态承载）网络的拓扑结构：电路内的每个内部节点值只有在其输入变得准确之后才被认为是准确的，并且经过一定量的时间来从稳定的输入计算值。第二，锁存器应该遵守全局时钟，并且应该全部并行更新虽然合成电路将混合组合和顺序元件，为了模拟的目的，将两者分开是方便的。许多HDL仿真器都是这样做的，因此电路只被视为组合网络。这是通过改变电路的输入/输出接口来实现的，以包括每个状态元素的新位。新的输入和输出分别表示当前状态和下一状态值。这种转换被用作我们的ABEL语义的基础。每个时钟周期，每个标识符（在ABEL模块中指定，即在ABEL语法中）与变换电路中的至少一个值相关联。 这些关联采用排序NodeValue的三元组的形式，M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）4751§都聚集在一起op [_，_，_]：节点类型标识符值->节点值。第一个参数是一个标记，描述它在变换电路中是什么类型的节点：主输入（pi），当前状态输入（cs），主输出（po），下一状态输出（ns）或内部节点（in）。图2显示了一个ABEL模块（经过适当修改以用于Maude解析），它存储来自当前时钟周期的值，允许在下一个时钟周期期间使用该值。可选地，可以抑制该输出。由标识符“D”和“EN”表示的单比特线或引脚是模块的输入;“Q”是内部节点;"OUT“是唯一的输出。Q在下一个时钟周期中取其指定值的事实由istype reg限定符指定。在电路的方程部分中，对于下一个clock周期，Q被指定为D的当前值。如果使能引脚“EN”被断言，则“OUT”获得与“Q”相同的值（即，具有逻辑值1），并且特殊值Z 否则，请执行以下操作。 电路的当前状态可能如下所示：[pi，表示在前一个时钟周期内我们的语义有一个重写规则，通过评估ABEL构造将当前状态（一组排序NodeValue的三元组）转换到下一个时钟周期在当前状态和用户指定的输入。促进从一个时钟周期到下一个时钟周期的转换所必需的等式重写规则非常类似于用于指定简单命令式编程的语义的规则语言[15]方程的计算是基于它们在模块中被写下来的顺序进行的，而且，ABEL只支持本质上等同于赋值、if-then-else和switch语句的东西，这些语句非常容易指定。在某些情况下，由于ABEL的独特性，语义被证明是乏味的，但在技术上并不难处理。因此，与简单命令式编程语言的语义的主要区别在于，我们一遍又一遍地显式评估在[10]中描述了数字电路的替代语义，其中，在同步重写规则中，每个节点值被标记有节点采用所计算的值的周期数。在该方案中，不需要任何重写规则，但是为了与Maude模型检查器一起使用，如上所述指定同步是更干净和更有用的3跟踪检查硬件/软件接口本节介绍我们如何在Maude中设计一个有效的协同验证环境，用于实现级系统设计。我们的框架的一个大的组成部分由2中提出的ABEL语义组成，因此在下面的内容中，我们主要关注我们的框架如何利用ABEL语义进行跟踪检查。我们描述了语义如何允许我们使用Maude的LTL模型检查器 以及如何建立一个有效的命题语言来编写有意义的LTL公式的相关主题。语言涵盖硬件，52M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47软件，以及软件及其数据结构的元级属性，以便所有这些实体都可以一起推理，并且可以探索它们的交互。第3.2节介绍了一个案例研究。3.1共同验证环境硬件/软件协同设计从根本上讲是关于平衡的：决定系统的功能应该如何划分为硬件和软件组件。了解项目的目的和目标可以帮助定义指标，指导工程团队进行适当的划分，在各种指标之间取得平衡。考虑和影响设计决策的共同轴包括性能、功耗、尺寸、可编程性和降低的复杂性。显然，协同设计项目的验证应该包括硬件和软件之间的交互;既要确保系统范围的正确性，又要验证导致分区方案的工程选择。例如，如果指令吞吐量从来没有高到足以利用所有功能单元，那么使用此信息重新评估硬件分区并缩减设计可能是值得的。 如果软件很复杂并且依赖于与可用硬件的许多微妙的交互，那么如果没有可测试的实现，这种不一致性可能很难被发现，或者没有正式的分析。作为第二个示例，如果协同设计引擎试图最小化功耗，则正式验证当软件在芯片上执行时功率节省特征如何执行将是有用的。因此，实施后的协同设计决策的验证可能是必要的，以指导未来的重新设计或其他工作为HDL（如ABEL）的语义创建Maude规范代表了我们为促进共同验证而进行的第一步。重写逻辑的强大建模特性，特别是Maude，允许用户将设计的硬件和软件组件立即嵌入到统一的数学框架中。此外，系统的元级属性（例如，软件数据结构）也可以方便地建模并与设计的其余部分相关 这允许工程师以最合适和最自然的语言指定他/她的系统的属性，从而促进模块化验证分类，抽象掉不必要的细节，并有助于避免容易出错的编码。我们目前的验证框架是围绕模拟和LTL模型检查的组合构建的，称为跟踪检查。为了使跟踪检查适用，协同设计系统的状态必须以一种方式演化，对应于在固定输入上运行的具体模拟。我们的ABEL语义通过设计支持这一点：只有一个重写序列，模ACI公理。当使用命题模型检查器时，如Maude中的命题模型检查器，有必要开发一种强大的命题语言;一种可以在高抽象级别上轻松编写电路属性的例如，用于控制交通灯的电路设计应允许将灯的当前状态指定为红色，黄色或绿色，与每个颜色对应的信号值相反，M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）4753图三. 共同验证环境电路。当模型检查器用于更受限制的跟踪检查时，情况也是如此，因此我们为跟踪检查协同设计开发的命题语言具有许多这些功能。在硬件方面，可以使用以下命题检查与标识符关联的节点值op_asserted：标识符->命题。op_deasserted：标识符->命题。op_：：=_：Identifier Int-> Proposition.op_：：=_：Identifier标识符->命题。opp：Proposition-> Prop.对于与变换电路中的多个节点值相关联的标识符，所使用的值是与当前状态相关联的值。 如果单个位节点在当前状态下具有值1，则它们被断言，并且如果它们具有值0.可以使用整数常量或另一个多位节点的值，再次通过检查当前状态。符号：：=用于此目的，以避免与Maude中定义的其他类型发生冲突。此外，命名常量值（如以交通灯为例。如果模块将每种颜色声明为一个常量值，那么与每个常量值相关联的标识符可以直接通过写’LIGHT ::=与Maude中的LTL模型检查一样，状态命题的语义是54M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47表1简单处理器ISA：添加（addition）减法mul（multiply）（按位负载sw（商店）相等分支bgt（大于分支）停止用等式来定义，用查询当前状态值的等式来决定命题的真假。对于汇编程序，我们添加了其他命题：例如，我们有检查指令何时被执行的命题，指令何时被提交到程序员可见状态，等等。在案例研究中，我们提出了其他抽象，让我们推理特定的程序和数据结构。图3总结了验证环境的组件及其依赖关系，实线箭头可以从尾部到头部读作3.2硬件/软件案例研究我们的案例研究有三个主要组成部分：一个用ABEL设计的简单微处理器，一组用汇编语言编写的处理器程序，以及几个需要验证的属性。所有这些组件都由Maude使用内部定义的排序和运算符进行处理;图3中的虚线箭头显示了哪些模块负责定义这些外部表示（即RTL和汇编），这些表示可以在Maude中作为项进行处理3.2.1简单的微处理器我们的微处理器设计基于经典的五级有序流水线示例[12]，并支持表1所示的指令集架构（ISA）。 我们的处理器设计中缺少的显著功能，在一个功能齐全的芯片，包括I/O子系统，高速缓存和中断处理。 都留给未来的工作。 程序是在这样的假设下编写的并由图中的汇编程序转换成机器码3 .第三章。单元假定延迟意味着在处理器上动态执行的每个指令都应该被处理，就像所有前面的指令已经完成一样。每个指令都通过五个流水线阶段，最终完成并更新程序员可见状态。一条指令首先被提取（IF），然后被解码（ID），执行（EX），允许访问内存（MEM），最后允许写入寄存器文件（WB）。为了提高性能，一个已经计算过但还没有返回到寄存器文件的值被转发到任何使用该值的指令。另外，分支被静态地预测为不被采用，并且指令提取推测性地继续，直到这样的分支被执行为止。预测被证明是错误的，此时坏指令被无效。因为存储器访问发生在执行阶段之后，所以在加载之后的下一个周期期间获取的并且依赖于其结果的指令被延迟一个周期。M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）4755在fetch stage中循环。所有这些都是可以在模拟过程中监控的有趣功能。如果有违反这些属性之一，执行软件可以帮助把跟踪到一个更容易理解的上下文中。 另一方面，如果一个软件产生了不正确的结果，但是属性通过了测试，那么程序员可能想看看软件本身。3.2.2软件和验证示例我们指定的第一组公式专注于微处理器的内部属性。我们针对的主要组件是转发、分支和延迟逻辑。我们检查了每条指令在执行阶段都获得了适当的操作数值，不允许更新推测性指令 当一个分支被采用时的状态，并且只有某些条件会导致停顿，这些停顿是固定数量的周期。表2列出并简要描述了我们验证的每个处理器专用公式。我们用来验证转发逻辑的主要属性是hw-02，它由LTL公式指定op hw-02：->公式。方程式hw-02 =[]p（'MEM-WB/\->（register-value...对于第二寄存器源操作数也是如此上面的命题显示了对先前未描述的语言的补充，并且用于推理流水线阶段。命题’alu-input-A当输入到EX级ALU的名为alu-input-A的内部多位节点在2个周期前携带的值等于当前状态时， 在3个周期前取出的指令字的“A”位置指定的寄存器因此，LTL公式基本上表明，对于任何完成的指令，它在流水线EX阶段获得的寄存器操作数等于它提交时的寄存器文件内容。当然，一个更完整的公式将验证所引用的内部信号实际上具有其预期含义。然而，正如所给出的，该公式将能够捕捉到关于到操作数转发。谈到软件部分，我们首先用微处理器的汇编语言编写了一个冒泡排序程序。除了表2中的属性之外，我们还在元级别上为软件组件及其功能添加了四个新的属性。通过直接在Maude中定义整数数组的排序函数，以及从软件指针值和长度中提取数组的映射，促进了元级推理。这使得可以将排序数组的数学定义与汇编代码排序程序及其数据结构进行比较。获取数组56M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47表2处理器验证的LTL公式公式名称描述公司简介指令仅在IF中停止。公司简介ALU操作数在提交时反映寄存器文件。公司简介失速不得超过3个周期。公司简介停止后无状态变化公司简介在分支上，下一个提交的指令是目标。公司简介r0永远不会被覆盖。公司简介Taken branch刷新IF、ID和EX。公司简介失速只发生在分支占用和负载使用时。通常依赖于应用程序二进制接口（ABI）的参数和堆栈约定，也依赖于假设的数组实现。 它还将依赖于所使用的特定寄存器分配映射。ABI将在任何电路设计工作开始之前定义，并且寄存器映射将由编写汇编代码的工程师或生成它的编译器冒泡排序程序的正确性由LTL公式检查，该公式确保每当数组中有反转时，内部循环中的交换代码将在未来的某个时间点执行。检查有序整数数组中的反转的命题由下式给出：op inversion：IntArray -> Prop.eq inversion（IX：Int）=false。eq inversion（IX：Int，IY：Int，ILX：IntList）= IX> IY或inversion（IY，ILX）。除了使用反转检查来验证正确性之外，还可以监视函数的运行时间。 运行时属性可以用 循环数，相对于输入数组的大小，直到执行暂停指令。 在冒泡排序的情况下，这个值应该是数组大小的平方 对于一个更复杂的程序，通过使用适当的元级抽象（如整数数组）检查数据结构，可以方便地跟踪运行时间。在排序的情况下，运行时间可以根据输入数组中的反转数来指定，或者在矩阵的情况下，某种稀疏性度量可能是有用的。我们还检查了程序不是自修改的，并且表3列出了排序程序特有的所有属性，以及每个属性的简短描述。在2.5GHz/2GB PowerPC机器上，使用大小为13的数组运行排序程序，检查表2和表3中的所有属性需要大约4分钟和5000个模拟周期M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）4757表3冒泡排序公式名称描述公司简介阵列反转导致交换。公司简介运行时间为10n2个循环。<公司简介没有自修改代码。公司简介在数组边界之外没有读写操作我们研究的第二个程序取自图形编程。 是 计算曲面法线的着色器例程的一部分。 需要获得芯片理论峰值性能的高百分比的短汇编代码片段利用这种推理，我们开始为我们的微处理器编写相应的代码，目的是为了使指令的调度达到最高性能。因此，我们指定代码不应该有任何动态流水线停顿，并且应该在100个周期内完成。我们检查的所有属性都在表4中给出。表4Phong着色器公式名称描述公司简介主代码体中没有管道停顿公司简介计算正确的值。公司简介没有自修改代码。公司简介在数组边界之外没有读写操作公司简介在不到100个周期的时间内完成在尝试调度指令以获得高性能时，我们最初犯了一个错误，导致程序计算出不正确的结果。这被ps-02捕获，我们更新了代码。当我们修复代码时，无意中创建了一个load-use依赖项，并导致管道停顿，ps-01立即发现并修复了它。4相关工作IBM 当模拟电路时，每个监视器都会观察系统状态和内部信号如何随时间变化，并报告任何问题。[6]第二个是58M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47数字电路的跟踪检查工具。 它可以检查模拟痕迹是否违规在线性时序逻辑中指定的属性的一阶变量，数组和队列。数据结构允许在更高的抽象级别上指定属性，从而提高可用性并减少低级指定错误。然而，这些工具都不能很容易地用来理解硬件/软件交互。在嵌入式设计领域，有一些工业工具可以进行一定程度的硬件/软件调试。例如，Xilinx EDK [25]允许用户使用GDB调试他/她的软件，并在触发断点时范围内的内部硬件信号。然而，它在另一个方向上不起作用：硬件事件不能用来停止软件。此外，这些调试工具不支持形式分析Ptolemy II [13]是一个专注于嵌入式系统建模和设计的项目。一个完整的系统，包括硬件和软件，可以使用支持的“计算模型”在不同的抽象层次上建模。目的是让系统的建模指导其实现，在某些情况下，甚至可以从抽象视图自动完成。Ptolemy II捕获嵌入式系统的硬件和软件组件，但并不特别关注验证系统的特定实现跟踪检查也已成功地用于软件监控。例如，见[11，9]。事实上，这已经发展成为一个新的软件工程研究领域，称为运行时验证[19]。5结论和今后的工作我们已经提出了一个正式的语义在Maude的ABEL HDL，并解释了如何可执行的语义可以用作基础的共同验证框架。据我们所知，无论是ABEL语义，和跟踪检查ABEL协同设计的能力是新的贡献。 我们的经验到目前为止是相当令人鼓舞的，在重写逻辑和莫德已经给出了使用一个灵活的框架来指定和分析硬件和软件的复杂属性以及它们如何相互作用。然而，这仍然是一项正在进行的工作，有待于许多改进和新的发展。例如，我们应该提高HDL模拟器的效率，以实现更大的设计，并增加对其他HDL或其可合成子集的支持。类似地，我们应该结合已知的技术来优化跟踪检查，以提高性能。此外，将一阶变量添加到指定逻辑中将非常有用，并且不应该对跟踪检查造成问题。 此外，委员会认为， 我们应该发展一套更大和更有雄心的现实生活案例研究。我们的长期目标是开发新的方法和工具来正式指定和分析嵌入式系统。本文提出了这一目标，但没有解决一些重要的问题，除了上述的改进和扩展，将是未来的研究课题。我们已经指出，对于许多嵌入式系统，指定它们运行和验证的环境M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）4759确定与它们与这些环境的交互相关的属性，与指定和验证硬件/软件系统本身一样重要：这两项任务应该一起完成。虽然我们在案例研究中已经解决了一些实时和性能问题，但是环境的完整建模虽然非常重要，超出了本文的范围。建模这种环境的自然方法是将嵌入式系统视为可以混合的实时系统，甚至可以是随机和混合的。因此，从重写逻辑的角度来看，要使用的自然技术和工具将包括实时重写理论[20]、概率重写理论[3]、随机混合系统的建模[17]以及诸如实时Maude [21]和即将推出的PMaude [3]和SHYMaude [17]等工具。这将使我们能够处理机械和传感接口，例如许多控制系统中的接口，例如防抱死制动系统。在本文的术语中，它还将提供可以正式指定和分析的元级别属性的自然扩展。确认我们感谢评审对先前版本的详细评论，这些评论帮助我们改进了演示文稿。此外，我们还要感谢Sean Keller审阅了本文的草稿，并感谢Andrew Colombi提供了图形程序的一个版本。 这项研究得到了ONR资助N 00014 -02-1-0715的部分支持引用[1] Abarbanel，Y.，I.比尔湖Glushovsky，S. Keidar和Y. Wolfsthal，FOCs：从正式规范自动生成仿真标记，在：CAV538-542.[2] Abarbanel-Vinov，Y.，N. 艾曾布德-雷谢夫岛比尔角Escherner，D.Geist，T.海曼岛阿维尼翁，E. 里佩尔岛Shitsevalov，Y.Wolfsthal和T.Yatzkar-Haham，关于功能形式验证的有效部署，Form。方法系统设计。19（2001），pp. 35比44[3] 阿 加 ， G. ， Meseguer 和 K. Sen ， PMaude ： Rewrite-Based Specification Language for ProbabilisticObject Systems，in：3rd Workshop on Quantitative Aspects of Programming Languages（QAPL[4] 啤酒，我，S. Ben-David和A. Landver，RCTL公式的动态模型检查，在：CAV184-194。[5] 本-大卫，S.，C. Escherner，D. Geist和Y. Wolfsthal，IBM的Model Checking，Form。方法系统设计。22（2003），pp. 101比108[6] 坎菲尔德，W.， E. A. Emerson和A. 萨哈，检查 正式质量标准 下 模拟，在：ICCD[7] 爱德华兹，S.，L. Lavagno，E. A. Lee和A.陈志荣，嵌入式系统之设计与分析，国立成功大学硕士论文，（1997）。[8] Eker，S.，J. Meseguer和A. Sridharanarayanan，The Maude LTL Model 1999，in：F. Gadducci和U.Montanari，编者，第四次重写逻辑及其应用研讨会，WRLA[9] FengChen 和 GrigoreR oRansu， Toowa rdsAdherence-Orient edP rog ramming ： APa radigmCombiningSpecification and Implementation，第三届国际认证研讨会，ENTCS 2003，pp. 106-12560M. Katelman，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）47[10] Harman，N.一、使用Maude的简单流水线微处理器，WADT128-151[11] Havelund，K.和G. Rosu，Monitoring Programs Using Rewriting，ASE一百三十五[12] Hennessy，J. L.和D. A. Patterson，[13] Hylands，C.，E. Lee，J. Liu，X. Liu，S. Neuendor Schlider，Y. Xiong，Y. Zhao和H. Zheng，概述托勒密计划，技术报告，电气工程和计算机科学系，加州大学伯克利分校（2003年）。[14] Janick Bergeron，[15] Jo s'e Meseguer和Grigore R o ransu，The Rewriting L o gic Semantics P r oj e ct，in：Structur al O p rational Semantics 2005，ENTCS，2005。[16] Ma nuelCl av e landFranciscoDur'anandSte venE kerandPatri ckLincolnandNarcisoMar t's-OlietandJo s'eMeseguerandCarolynTalcott，“MaudeManual（Version2.2），”.URLhttp://maude.cs.uiuc.edu/[17] Meseguer，J.和R. Sharykin，Specification and Analysis of Distributed Object-Based Stochastic HybridSystems，Technical report，University of Illinois at Urbana-Champaign，CS Department（2005），toappear inP roc.混合动力系统2006，Springer LNCS。[18] Micheli，G. D.和R. K.陈志华，电脑硬体与软体协同设计，国立成功大学机械工程研究所硕士论文（1997）。[19] Oleg Sokolsky和Mahesh Viswanathan，编辑，[20] Oülveczk y，P. C. 和j. Meseguer，《Rewriting L o gi c中的实时和混合系统的性能》，理论计算机科学285（2002），第285 页。359-405[21] Oülveczky，P.C. 和j. Meseguer ，Real-TimeMaude2.1（2004），pr oc. 5thI NTL. 重写逻辑及其应用。[22] Sgroi，M.，L. Lavagno和A.陈志华，嵌入式系统设计与测试，硕士论文，北京，2000。[23] Vardi，M.，Designing a Property Specification Language（2005），在UIUC Formal Methods Seminar上的演讲。[24] Xilinx，OnlineABELReference，http://toolbox.xilinx.com/docsan/xilinx7/help/iseguide/mergedProjects/abelref/abelref.htm（2005）.[25] Xilinx，PlatformStudioandtheEDK，http://www.xilinx.com/ise/embedded_design_prod/platform_studio.htm（2005）.