静态程序分析中用于定义新的控制流检查的GPSL/GXSL语言的研究

理论计算机科学电子笔记254（2009）181-197www.elsevier.com/locate/entcs一种用于静态程序分析的沃尔夫冈·赖夫Lehrstuhlfur？rSoftwar ete chnikundProgrammierspracchen，Universita？tAugsburrgUniversitéatssstraße14，86135Augsburrg，Germany{vistein，ortmeier，reif} @ informatik.uni-augsburg.de拉尔夫·胡克澳大利亚国家信息通信技术有限公司（NICTA）新南威尔士Locked Bag 6016，Sydney NSW 1466，Australia{ralf.huuck，ansgar.fehnker} @ nicta.com.au摘要静态程序分析器通常带有一组硬编码的检查，几乎没有给用户添加其他属性的空间。 在这项工作中，我们提出了一种统一的方法，使新的静态分析检查的规范，以简洁的方式。 特别是，我们提出了我们的GPSL/GXSL语言来定义新的控制流检查。 该语言与CTL规范密切相关，CTL规范与SQL查询相结合。此外，我们还提供了一些在我们的工具GOANNA中实现的规范，并报告了我们在添加新的检查.关键词：抽象规范，静态分析，CTL规范，GPSL/GXSL，XPATH查询1介绍静态程序分析已被证明是检测商业源代码中的错误和漏洞的有用工具[4，13，2，11]。许多研究致力于提高分析技术的速度、深度和精度。然而，在编写一般的静态分析检查或扩展现有的预定义检查数据库以满足域、公司或项目特定需求方面，几乎没有工作。1571-0661© 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.066182M. Vistein等人理论计算机科学电子笔记254（2009）181在这项工作中，我们提出了我们的静态分析工具GOANNA[10]和我们开发的检查器语言用于添加新的检查或修改现有的检查根据需要。GOANNA是一个基于模型检查技术的C/C++程序GOANNA主要研究语法程序抽象，即，控制流程图（CFG），其标记有感兴趣的对象，例如，内存被分配、使用或释放的位置，并在此抽象上进行CTL模型检查CTL属性表示语法检查，例如，动态内存在解除分配后是否我们的控制流为中心的检查器语言GPSL/GXSL已被驱动，通过描述典型的检查模式，在一个简单的声明方式。它分为两个部分，针对两个不同的受众：第一个是GPSL，一种高级抽象语言，它是最常见的检查模式的集合，加上一个预先定义的感兴趣对象的大型库这些预定义的对象本身是查询，例如内存分配，使用或释放的位置这种语言面向最终用户，他们喜欢基于使用该库中的对象实例化的模式来定义新的检查第二种语言是GXSL。这是一种低级语言，用于构建预定义对象的库，更适合静态分析工具的开发人员或专家。GXSL是一种允许从程序的抽象语法树（AST）中查询信息的语言，直接进行CTL检查。GXSL的优点是新的语法对象，例如，找到所有声明为静态的程序变量，可以快速定义，更重要的是，统一定义。有几种方法可以定义静态检查和时态逻辑模式。Engler等人定义了元编译语言Metal[8]来指定新的检查。Metal本质上是一个用类C语言编写的状态机，其中某些接受状态表示违反属性。使用C作为底层的规范语言有优点也有缺点：一方面，大多数开发人员已经熟悉这种语言，另一方面，它被认为是容易出错的，它缺乏简单的抽象机制。此外，Metal在单独的程序路径上进行评估，使其类似于LTL而不是CTL检查。Mygcc是一个使用Condate语言进行静态代码分析的研究工具[18]。Condate是一种极简的声明性语言，用于表达用户定义的检查。它不如Metal强大，但支持识别程序中的模式，并定义其上的正则路径表达式。在本质上，声明式方法类似于GPSL/GXSL，但GOANNA使用了更具表达性的CTL公式，并支持GXSL中常见的查询M. Vistein等人理论计算机科学电子笔记254（2009）181183将高级模式编码为CTL公式（或反之亦然）的最突出方法由Dwyer等人提出。[6]。这些模式用于描述反应式系统的常见行为要求。这个想法类 似 于 GPSL ， 但 是 ， 针 对 不 同 的 领 域 ，在 Metal 、 Mygcc 或GPSL/GXSL中，这些模式和程序中的匹配点没有直接联系。一种更通用的构建时态逻辑的方法是属性规范语言（PSL）[1]，用于编写硬件特定检查。PSL使用CTL以及LTL来指定硬件信号的时间关系。PSL以硬件为中心， 不容易应用于其他领域，如静态代码分析。Lam等人选择了一种相当不同的方法[14]。作者结合了一个静态的程序查询语言（PQL）的动态观察者。PQL能够识别程序中感兴趣的语法结构，并为应用程序提供工具，使这些结构的出现对外部可见。在第二步中，在运行时相对于已指定为状态机的预定义模式观察这些事件。虽然与我们的工作有一些相似之处，但PQL主要关注动态行为和运行时验证。总之，对于类CTL规范语言和语法匹配有不同的方法，但GPSL/GSXL是第一个将这些方法结合在一起进行静态程序分析的方法。本文的其余部分组织如下：在第2节中，我们介绍了GOANNA工具及其底层框架，以激发在设计GPSL/GXSL语言时所做的一些选择。语言本身在第3节中有详细的定义。我们在第4节中报告了我们在实际软件中使用GPSL/GXSL的一些经验，并在第5节中给出了我们的结论。2Goanna工具在这项工作中，我们使用一个基于自动机的静态分析框架，在我们的工具GOANNA中实现。与典型的方程求解静态分析的方法，基于自动机的方法[5，12，17，16]定义了属性的时间逻辑表达式的注释图。属性的有效性可以通过图探索技术（如模型检查）自动检查。GOANNA1本身是一个闭源项目，但该方法的技术细节可以在[9，10]中找到。第1http://nicta.com.au/research/projects/goanna184M. Vistein等人理论计算机科学电子笔记254（2009）181图1. (a)示例C程序，和（b）注释的控制流程图（CFG）。为简单起见，每个节点对应于一行代码。2.1源代码分析Goanna方法的基本思想是将C/C++程序映射到其相应的控制流图（CFG），并用感兴趣的语法结构的出现来标记CFGCFG与标签一起可以容易地被映射到模型检查器的输入语言或直接被翻译成用于模型检查的Kripke结构考虑图1中的简单示例程序foo。为了检查变量是否在被读取之前被严格写入，我们在语法上标识读取或写入变量的程序位置。对于图1（a）中的变量res，我们自动将这些节点分别标记为readres和writeres，如图1所示第1段（b）分段。给定这个带注释的CFG，检查res是否总是被初始化就相当于检查下面的CTL公式。(1)A<$readresW（写res）M. Vistein等人理论计算机科学电子笔记254（2009）181185∧¬图2.静态分析C/C++代码的模型检测方法。CTL使用路径量化器A和E， 而时态运算符G、F、X和U。（状态）公式Aφ表示φ必须在所有路径上成立，而Eφ表示φ必须在某条路径上成立;（路径）公式Gφ、Fφ和Xφ分别表示φ在路径的所有状态、某个状态或下一个状态下全局成立。 untilφU≠意味着在满足φ的路径上出现一个状态之前，性质φ必须成立。 我们也使用弱直到φW<$。 它与until的区别在于，要么φ在until保持，要么φ沿着路径全局保持。不要求φ对路径上的任何状态都成立，只要φ处处成立。它也可以用其他运算符来表示，也称为unless运算符。CTL公式（1）意味着变量res不能被读取，除非它已经被写入。 条款（写作res）读取res）排除读写变量的语句，如后递增res++语句。注意，图1（b）中注释的CFG不满足CTL公式（1）。基于自动机的方法的一个优点是，通过改变路径量化器，可以很容易地修改属性以表达更强或更弱的要求，即，改变路径量化器A到E，反之亦然。在上面的例子中，用E替换A将检查变量是否在至少一个路径上初始化这也促使使用CTL而不是LTL。186M. Vistein等人理论计算机科学电子笔记254（2009）1812.2Goanna工具的架构G OANNA使用NuSMV[15]对带注释的模型进行模型检查。为了用NuSMV分析C/C++程序，需要几个步骤将源代码转换成合适的Kripke结构，并生成相关的CTL公式。我们使用两种特定语言来实现这一点。 Goanna属性规范语言（GPSL）用于定义CTL模板和相关的原子命题。另一种语言Goanna语法规范语言（GXSL）用于将原子命题映射到源代码中的位置（更准确地说，在控制流程图中）。这两种语言将在下一节中介绍。自动NuSMV模型创建的架构如图所示二、图2中的左分支读入源代码，并将其解析为抽象语法树（AST）。此AST存储为XML文档。在下一步，从AST中生成控制流程图。CFG可以被看作是一个有限状态机，因此已经非常接近最终的NuSMV模型。除此之外，还需要生成标签（原子命题）和CTL公式本身GPSL属性包含CTL公式的模板。模板将在运行时在AST上用查询结果实例化。例如，在一个示例中，查询所有变量，所有读取和所有写入。这些查询用GXSL表示。此外，用于匹配查询结果的CFG节点随后被用作控制流图中的标签，从而产生带注释的控制流图。在最后一步中，将带注释的控制流程图和CTL规格组合以形成NuSMV的输入模型。NuSMV执行模型检查，并返回所有失败的CTL规范的列表。目前，这种方法支持过程内检查。目前正在开发该工具的扩展以及支持过程间分析的规范语言。3GPSL/GXSL规范语言通常，Goanna中的静态分析检查要求源代码中的某些语句以特定顺序执行。这种属性的一个标准示例是，每当读取一个变量时，它必须在之前被赋值。物业的指定包括两部分：第一，控制流程中若干兴趣点的时间关系。这是由Goanna Properties Specification Language（GPSL）定义的，GPSL是一个用于常用关系的预定义模式库。其次，定义兴趣点，例如函数调用，变量赋值等，将使用Goanna规范语言（GXSL）它允许选择M. Vistein等人理论计算机科学电子笔记254（2009）181187在被检查的程序的抽象语法树上使用查询语言的程序语句。3.1Goanna属性规范语言时间关系通常使用时间逻辑来指定。有几种不同的时态逻辑;常见的是计算树逻辑（CTL）和线性时态逻辑（LTL）。如第2节所述，GOANNA使用CTL。对于静态分析，能够区分不同的可能执行路径是很有帮助的。隐式地覆盖所有可能路径的语句，如在LTL中所做的，通常是不够的。为了静态分析的目的，期望能够量化多组的性质，例如，程序变量例如，对于程序的所有变量，某个CTL本身是不够的，因为它不允许对原子命题集进行量化。例如，在一个示例中，CTL公式（1）仅表示对程序1（a）的变量res的检查。Goanna属性规范语言以这样一种方式扩展CTL，即可以在源代码的语法结构集上量化CTL表达式，如所有变量，所有for循环，所有函数调用等。此外，GPSL提供了一种机制来发布定制的警告消息，以及引用反例中的特定部分，即，错误的可能来源因此，任何GPSL属性都由以下部分组成• 支票的唯一标识符• 对一组对象的量化，• 将使用这些对象实例化的CTL模板，以及• 一个警告条目，包含警告消息和要警告的反例中的位置。我们首先提供一个简单的例子，然后解释不同的方面。3.1.1例如下面的示例显示“uninitialised variable”属性。这个属性检查程序中的变量在使用之前是否已经初始化。GPSL的完整语法包含在附录A.1中。188M. Vistein等人理论计算机科学电子笔记254（2009）181PROPuninitialised_varFORALLvarIN var_decl（）始终在读取（var）之前写入（var）WARN LINElast（read（var））WITH“变量””变量名（var）“”可能未初始化”表1：检查未初始化变量PROP关键字标记新属性的开始，后跟属性的名称。下面的行量化了程序源代码中所有变量的后续指定关系（参见第3.1.2节）。该关系是使用时间模式指定的，在本例中，...就在...模式应用。 的详细情况第3.1.3节解释了不同的模式。该方案指出，必须使用GXSL函数指定时间关系（也请参见第3.2节）。最后三行指定警告消息。这一行被指定为读取变量的最后一行，消息本身被指定为字符串。第3.1.4节中更详细地解释了警告消息。3.1.2量化GPSL在CTL上的一个重要扩展是量化过度表达的能力。这允许指定一个时态关系，然后在运行时多次使用该时态关系来检查所有指定项的关系（如程序的所有变量）。因此，GPSL计算GXSL函数提取相关的结构，如所有变量的列表，并在新声明的变量中提供此信息，该变量随后可在时间关系中使用。3.1.3模式GPSL提供了一系列预先定义的模式来指定属性。这些模式定义了静态程序分析中一些最常用的时间关系，部分基于Dwyer等人的思想。[7，6]。每个模式被映射到表达所需关系的CTL公式。模式包含变量a、b等，它们必须引用GXSL函数，如read（var）或write（var）（参见3.2节）。控制流程图将根据这些函数调用的结果进行标记下面的列表包含一些在他们的故事，有一个共同的故事，一个共同的故事，一个共同的故事M. Vistein等人理论计算机科学电子笔记254（2009）181189→→燕鸥• 从来没有，（CTL：AG！a）、这种模式要求没有可以到达的标记为a的节点。该模式可以用于实施编码标准，例如，一般禁止某些功能、语句等。• 最终a，（CTL：EFa）此模式要求至少有一个可达节点标记为。此模式的一个使用示例也是编码标准的强制执行。它允许设计一个检查某些语句（例如日志记录）是否在每个函数中至少出现一次• 总是 在b之前，（CTL：A [！B Wa]）在所有可能的执行路径上，如果有一个节点标记为b，那么之前一定有一个节点标记为a如果不存在标记为b的节点，则也不需要标记为a的节点。这个模式可以用STRICTLY关键字来扩展，它检查第一个标记为a的节点与标记为b的节点是否是同一个节点。它由CTL公式A [！bW（a&！b）]。这种模式的一个应用例子是检查未初始化的变量（参见第3.1.1节）。• 后 ALWAYSb，（CTL：AG（aAFb））如果有一个节点标记为a，那么从这一点开始的所有可能的执行路径必须至少有一个节点标记为b。此模式可用于资源管理，例如，保证分配的资源最终被释放。这种模式的一个例子可以在3.3节中看到。• 后 一些b，（CTL：AG（aEFb））如果有一个节点标记为a，那么从这一点开始的至少一个可能的执行路径必须至少有一个节点标记为b。此模式是AFTERaALWAYSb模式的一种较弱形式，它也允许条件b只发生在某些可能的执行路径上的程序。前面解释的模式只是所有可用模式的一小部分。 本文的示例中使用了其中一些模式，因此选择了更详细的解释。目前，支持超过20种不同的模式，并且库正在不断发展190M. Vistein等人理论计算机科学电子笔记254（2009）1813.1.4警告消息如果违反属性，则必须向开发人员显示警告消息。GPSL提供了指定警告消息的方法，该警告消息可以用变量名和行号实例化，在反例中的某个位置。 这个位置将由该反例中某个节点的出现来确定。通常，使用第一个或最后一个这样的出现就足够了。3.2Goanna规范语言为了实例化具有相关节点的GPSL模式，我们使用GXSL语言。第3.1.1节中的示例已经包含了返回节点位置的GXSL函数调用，如read（var）和write（var）语句的识别可以在程序的抽象语法树上执行。[3]语言非常适合在树形数据上表达查询，比如抽象语法树。但是，XML查询本身通常只是静态字符串。对于每个不同的程序，这些字符串必须根据变量名、函数调用或函数参数动态应用。 这些名称在设计查询时通常是未知的GXSL语言用函数和变量扩展了XML。GXSL函数是返回控制流图的一组节点的函数，其被标记为2。由于GOANNA生成的标签在控制流图中必须是唯一的，因此每个GXSL函数也必须有一个唯一的标识符可以包含在标签名称中。GXSL函数可以具有可以用于实例化通用XML查询的参数（例如，读（var）示例中的var）。该参数被指定为CFG的节点，这允许GPSL语言使用无参数的GXSL函数来量化时间关系，并使用结果集的单个项作为进一步GXSL函数的参数。除了参数化的XML查询和唯一标识符之外，GXSL还添加了一个类型系统。GXSL属性由以下部分组成• 函数名，可能带有参数，• 期望的输入类型以及输出类型，• 用于标记节点的唯一标识符，以及• 查询本身。2虽然GXSL函数在抽象语法树上工作，但在GPSL属性中使用的相关信息是控制流程图的节点抽象语法树中的每一项都可以映射到控制流程图M. Vistein等人理论计算机科学电子笔记254（2009）1811913.2.1例如下面的例子定义了write函数。此函数返回已写入变量的所有节点的集合。GXSL语言的完整语法可以在附录A.2中找到。FUN写入（节点）EXPdeclRETwritevarIDENTIFIER @id（node）NODESET“//Op2[@op表2：GXSL函数write，它选择写入某个变量的所有节点。关键字“FUN“开始一个新的“write“函数需要一个它返回已写入变量的“writevar“类型的节点唯一标识符被定义为声明节点的id属性（它总是唯一的）。最后一部分是XML查询，它使用变量node进行参数化。该查询搜索作为修改操作的每个二进制操作对于所有这些操作，左边的子变量（被赋予新值的变量）都要与GXSL函数应该查找的写节 点 的 变 量进 行 比 较 。 该 查 询 由 两 个 字 符 串指 定 ， 它 们 与参 数“node“的“id“属性连接在一起查询的这一部分在运行时被计算为字符串。3.3GPSL和GXSL的特定于域的示例下面的清单显示了一个更复杂的、特定于域的GPSL属性和必要的GXSL函数。 该属性的目标是检查是否已正确关闭所有数据库连接。两个GXSL函数对于这个规范是必要的。第一个函数（第二个GXSL函数（FUNconnections（）RETdbconn192M. Vistein等人理论计算机科学电子笔记254（2009）181NODESET“//Op2[@op='Modif']/Var[@role='op1' and ../FnEval[ @name =FUNclose（conn）EXPdbconnRET dbcloseNODESET“//FnEval[@name =@id（conn）GPSL属性使用“after . . .总是. . .“模式。这种模式确保，如果某个事件发生，另一个事件最终会在所有可能的执行路径上发生。PROPclosedbFORALLconnIN connections（）AFTERconnALWAYS close（conn）WARN LINEconnWITH“数据库连接未关闭”“closedb”属性检查每个连接句柄的连接是否最终被关闭（close方法已经用适当的句柄调用）。 如果违反此属性，则上次访问的行号 将显示“数据库连接未关闭”消息4经验在本节中，我们简要报告了我们使用GPSL/GXSL语言定义新检查的经验及其对GOANNA可扩展性的影响以声明的方式而不是作为操作状态机来编写静态分析检查有几个优点和缺点：首先，状态机更容易画在纸上，因此，一个更好的讨论参考。然而，它们需要更多的算法思维，即“if-then-else”，而不是直接表达属性。在这种程度上，声明性检查要简洁得多。此外，声明性要求很容易适应，例如，一个属性是应该在所有路径上保持，还是至少在一个路径上保持。这极大地帮助了快速创建各种不同强度的检查。一般来说，使用GPSL语言学习和开发检查对于使用该语言的程序员来说已经被证明是简单的。另一方面，GXSL的学习曲线被证明是陡峭的。我们看到 这有两个原因：一方面，GXSL要求开发人员M. Vistein等人理论计算机科学电子笔记254（2009）1811933503002502001501000 2 4 6 8 10 12 14 16启用的检查图3.可扩展性，以增加检查次数对古安娜的产品相当熟悉要编写从AST中准确选择正确节点的SQL查询，并考虑到C/C++的许多微妙之处，需要随着时间的推移积累足够的经验。另一方面，我们目前还没有很好的GXSL调试机制。这意味着，一旦节点被查询和组合，就没有显示即时查询结果和所选节点的直接调试功能/输出。这当然需要解决，使GPSL更加用户友好。使用GPSL/GXSL的一个积极结果是，它可以显著减少新检查的开发时间。通常，新的属性在几分钟内就可以编写完成，这对于一般的GOANNA工具开发来说是一个很大的不同。虽然可以在[10]中找到GOANNA的一些一般性能指标，但在这里我们关注检查的可扩展性，即，运行时性能的增加数量的检查。图3描述了一个典型的可伸缩性结果。我们观察运行时相对于不同数量的检查对于给定的软件包。 运行GOANNA而不进行任何检查，即，仅仅是GOANNA的标准编译和解析就花了大约200秒，一个包含大约3500个功能的软件包添加更多检查只是适度地增加了运行时间。值得一提的是，不同的检查具有不同的复杂性，如前所述，单个检查应该被视为一类检查，因为它有时涉及数十个甚至数百个不同的程序变量。然而，可以看出，增加16类检查甚至不会使总运行增加一倍运行时间（秒）194M. Vistein等人理论计算机科学电子笔记254（2009）181时间和它增长次线性整体。后者的原因是某些对象，例如对变量的写入或读取被许多检查共享，并且发生了一些优化效应。一般来说，GPSL/GXSL已被证明不比手工优化的硬编码检查差。事实上，在许多情况下，GPSL/GXSL被证明是更优越的，因为它具有更高效的缓存和对查询对象的重用。GXSL函数的结果会自动缓存，开发人员无需关心保存结果和查找以前的数据。有了这个缓存，使用同一组节点的其他属性（例如，也需要写入变量的节点的属性）立即受益于不必再次执行可能耗时的节点查找5结论本文提出了一种方法来指定用户定义的检查。它允许方便，自动，用户定义的标签程序和指定复杂的时间关系很容易在这些标签使用一组表达预 定义 的 模式 。 这 种规 范 化方 法 已成 功 集成 到 现 代静 态 分析 工 具（GOANNA）中，现在是该工具的标准组件。尽管如此，特定语言本身是独立于工具和编程语言的。未来的工作是减少语言的一些限制，并将其扩展到非控制特定需求。有一个数字-GOANNA工具中未与当前GPSL/GXSL语言，例如：过程间检查、别名或数据反悬垂数组值分析。希望以这样一种方式扩展当前语言，使其可以使用非控制特定检查器的结果和功能。确认我们要感谢威廉·冯·罗森伯格对这项工作的贡献。NICTA由澳大利亚政府资助，由宽带，通信和数字经济发展局和澳大利亚研究委员会通过ICT卓越中心计划代表。M. Vistein等人理论计算机科学电子笔记254（2009）181195引用[1] Accellera，http://www.eda.org/vfv/docs/PSL-v1.1.pdf网站。[2] Astr'ee，TheAstr'eeStaticCodeAnalyzer，Website，http://www.astree.ens.fr/;visitedon25 February 2009.[3] 克拉克，J.和S.DeRose，网址http://www.w3.org/TR/xpath[4] Coverity，Prevent，Website，http://www.coverity.com/html/prevent-for-c-c++.html; 2009年2月25日访问[5] Dams，D.和K. Namjoshi，Orion：C和C++程序，贝尔实验室技术。Mem. ITD-04-45263Z，Lucent Technologies（2004）。[6] 德怀尔，M.，G. Avrunin和J. Corbett，Patterns in Property Specifications for Finite-StateVerification，Proc.International Conference on Software Engineering，1999，pp. 411-420[7] Dwyer，M. B、G. S.阿夫鲁宁和J.C. Corbett，Property Specification Patterns for Finite-StateVerification，FMSP7比15[8] Engler，D.，B. Chelf，A. Chou和S. Hallem，Checking system rules using system-specific，programmer-written compiler extensions ， in ： Proceedings of the Fourth Symposium onOperatingSystems Design and Implementation，San Diego，CA，2000.[9] Fehnker ， A. ， R. Huuck ， P.Jayet ， M.Lussenburg 和 F.Rauch ， Goanna-a static modelchecker ， in ： L. 布 里 姆 湾 R. Haverkort ， M. Leucker and J. van de Pol ， editors ，FMICS/PDMC，Lecture Notes in Computer Science4346（2006），pp.297-300[10] Fehnker，A.，R. Huuck，P. Jayet，M. Lussenburg和F. Rauch，Model checking software atcompile time ， in ： Proc. First Joint IEEE/IFIP Symposium on Theoretical Aspects ofSoftware Engineering TASE45比56[11] Grammatech，Codesurfer，网站，http://www.grammatech.com/products/codesurfer/overview.html; 2009年2月25日访问。[12] Holzmann，G.，用户定义属性的静态源代码检查，见：Proc. IDPT 2002，Pasadena，CA，USA，2002年。[13] Klocwork，Insight，网站，http://www.klocwork.com/products/insight.asp; 2009年2月25日访问。[14] Martin，M.，B. Livshits和M.S. Lam，Finding application errors and security aws usingpql：a program query language ，in：OOSLA '05 ：Proceedings of the 20th annual ACMSIGPLAN conference on Object-oriented programming，systems，languages，and applications（2005），pp. 365-383.[15] NuSMV，一个新的符号模型检查器，网站，http://nusmv.irst.itc.it/; 2009年2月25日访问。[16] 施密特，D。一、数据流分析是抽象解释的模型检查，在：POPL38比48[17] 施 密 特 ， D 。 A. 和 B.Ste Escheren ， Program analysis as model checking of abstractinterpretation，in：Static Analysis Symposium，1998，pp.351-380.[18] Volanschi ， N. ， A portable compiler-integrated approach to permanent checking ， in ：ASE103-112196M. Vistein等人理论计算机科学电子笔记254（2009）181A语言语法本节提供了GPSL和GXSL语言的完整语法，这些语法在当前版本的GOANNA静态分析工具中实现A.1GPSL语法本附录提供了GPSL语言的完整语法。语法以扩展的巴科斯范式显示gpsl = PROP名称表达式。name = ident [comment].comment = string.expression = FORALL ident IN_函数表达式| 模式警告。pattern= NEVER l_function| 最终l_function| 对于每个l_function HOLDSl_function| 对于某些l_function HOLDSl_function| 始终在l_function之前执行l_function|始终在l_function之前严格执行l_function| l_function之前的一些l_function|严格在l_function之前的一些l_function| AFTER l_function ALWAYSl_function| 在l_function之后始终在l_function之前| 在l_function之后l_function严格在l_function之前| 在l_function之前始终具有l_function| 在l_function之后始终在l_function之前严格具有l_function| AFTER l_function SOMEl_function| 在l_function之后某些l_function之前l_function| 在l_function之后某些l_function严格在l_function之前| 在l_function之前有一些l_function| 在l_function之后严格在l_function之前有一些l_function|在l_function之前一些l_function之后l_function| 在l_function之前一些l_function严格在l_function之后| CTLstr_function| CTLR str_function.l_function =函数| l_function与l_function| l_function或l_function| “（”l_function“）”。function = ident ['（' [ ident ] '）' ] .warning = WARN LINE LINE WITHstr_function.string_function = string| 功能| str_function '函数'str_function.line = ident| 第一次|最后| （第一次）|LAST）“ （ ” f u n c t i o n “ ） ” 。ident = idents identn*.idents=“a”|“b”|......这是什么？ |Z|“你……”|“_”。identn=“a”|“b”|......这是什么？ |Z|“你……”|“……”|“0”|......这是什么？ |“9”。string= '"'（identn|““）*"”。M. Vistein等人理论计算机科学电子笔记254（2009）181197A.2GXSL语法本附录提供了GXSL语言的完整语法。语法以扩展的巴科斯范式显示gxsl = FUN func types id expr.func = ident“（“[ ident ]“）”。types = [ EXPstrlist ] RET strlist。id= IDENTIFIER（attribute_ref|字符串）。expr = FORALL ident IN func expr| NODESETxpath| SELECT选择。xpath =字符串|属性引用| xpath“”xpath.select = func WHEREident“=”attribute_ref.attribute_ref=“@”ident“（“ident“）”。strlist= ident| strlist“，”strlist.ident = idents identn*.idents=“a”|“b”|......这是什么？ |Z|“你……”|“_”。identn=“a”|“b”|......这是什么？ |Z|“你……”|“……”|“0”|......这是什么？ |“9”。string= '"'（identn|““）*"”。