论有穷状态验证方法的局限性.doc

论有穷状态验证方法的局限性( 葛 玮 龚晓庆 郝克刚 （西北大学 计算机科学系 软件工程研究所 西安 710069） 摘要 程序有穷状态验证方法是介于程序验证和程序测试之间的一种方法,一方面它如同程序验证一样可以证明某程序具有某些要求的性质，或找出反例证明该程序不具有所要求的性质。另一方面它又不像程序验证那样复杂，要求验证人员具有较高的形式化推理的专业理论和数学水平。但是，现有的有穷状态验证方法有很大的局限性，它要求所论证的性质是有穷自动机所接受的事件序列的集合，或等价地说该性质能表示成为正则表达式。众所周知，有穷自动机所能接受的语言类，按Chomsky字的集合的分类是很小的类。本文讨论了这种局限性，并尝试突破只能使用有穷自动机的限制，提出了一种新的验证方法--有穷路径验证法。在这种方法中，所论证的性质表示可以推广到使用任何一类自动机。作为代价，描写系统的模型限制是无环的。对于有环的描写系统的模型，本文提出了一种称之为“有穷路径测试”的方法。同一般的程序测试一样，用这种方法通过测试不能正面地验证程序的正确性，可是如果通不过测试，则能帮你发现反例，找出程序的错误。与一般的程序测试不同的是这里的测试是相对于模型的路径，而不执行实际的程序。 关键词 程序验证、程序测试、有穷自动机、有穷状态验证、有穷路径验证。 引言 程序有穷状态验证方法是介于程序验证和程序测试之间的一种方法,一方面它如同程序验证一样可以证明某程序具有用户定义的某些性质，或找出反例证明该程序不具有所要求的性质。另一方面它又不像程序验证那样复杂，要求验证人员具有较高的形式化推理的专业理论和数学水平[1-5]。但是，有穷状态验证方法有很大的局限性，它要求所论证的性质是由有穷自动机所接受的事件序列的集合，或等价地说该性质能表示成为正则表达式。众所周知，有穷自动机所能接受的语言类，按Chomsky字的集合的分类是很小的类，比它大的类还有上下文无关语言、上下文有感语言和图灵机所接受递归可枚举集等。本文讨论了这种局限性。尝试突破程序有穷验证方法局限性，提出了一种新的方法，称为“有穷路径验证法”。在这种方法中，表示所论证的性质的自动机可以推广到使用任何一类自动机，如下推自动机、线性有界自动机甚至图灵机等。作为代价，限制描写系统的模型是无环的。对于有环的CFGs描写系统的模型，本文提出了一种称之为“有穷路径测试”的方法。同一般的程序测试一样，用这种方法通过测试不能正面地验证程序的正确性，可是如果通不过测试，则能帮你发现反例，找出程序的错误。与一般的程序测试不同的是这里的测试是相对于性质和模型的路径，而不执行实际的程序。 本文首先简单介绍程序有穷状态验证方法和分析它的局限性，然后给出尝试突破程序有穷验证方法局限性的方法--有穷路径验证法，最后讨论有穷路径测试法。 程序有穷状态验证方法及其局限性分析 FLAVERS (FLow Analysis for VERification of Systems)是美国麻省Amherst大学先进软件工程研究实验室研发的支持有穷状态验证方法的工具[1,3]。它使用数据流分析技术验证并行系统的基于事件的行为性质。分析人员首先定义一组所论证的事件和以这些事件的出现顺序的形式规约并行系统的性质，然后使用FLAVERS自动创建系统的模型，明确地表示并行任务间的通讯、同步和事件的顺序，而不必穷举整个状态空间。FLAVERS的核心是一个多项式时间的流分析算法，确定系统是否满足给定的性质。如果不满足，则给出违反此性质的反例。 图1. FLAVERS结构 FLAVERS的工作过程如图1所示。分析人员用带量词（这里用的量词有全称量词all和非存在量词no）的正则表达式QRE(quantified regular expression)或有穷状态自动机FSA (finite-state automaton)来表达性质和约束。所关心的事件是由性质和约束得到的，它决定了分析问题的字母表。为了论述系统所有可能的执行，FLAVERS构建了一种能简洁地表示所有对应于系统执行中相关事件的序列的模型—追踪流图TFG (trace-flow graph)。首先根据所分析的系统的每个并行任务的程序，建立标注的控制流图CFG (control-flow graph)，然后按照字母表将其精化为精化控制流图RCFG (refined CFG)。在按字母表精化后，把这些RCFGs组合起来，添加上反映任务间的同步和通信的节点和边，以及并行动作可能顺序的有向边，最后经过优化构成TFG（注：这里用添加有向边的方法来描述并行动作的顺序，并不一定好。可考虑采用并行字的办法[6-7]）。从理论上讲，同TFG的路径相联系的事件序列决定了性质自动机的状态转移序列。F