程序验证与自动分析工具研讨会2005.3上海..ppt

程序验证与自动分析工具研讨会 2005.3 上海 郝克刚 西北大学计算机科学系 软件工程研究所 提纲 引言 程序有穷状态验证方法及其局限性分析 程序有穷路径验证方法 程序路径测试方法 结束语 1, 引言 Lori A. Clarke: Finite State Verification: An Emerging Technology for Validating Software Systems. Clarke 教授 2003 在上海的演讲。/Expert/exp-Lori.asp Lori A. Clarke, : FLAVERS:A Finite State Verification Approach for Software Systems. Clarke 教授 2004.10 在西北大学的演讲。/hkg/docs/ 程序有穷状态验证方法 是介于程序验证和程序测试之间的一种方法。 2, 程序有穷状态验证方法简介及其局限性分析 FLAVERS (FLow Analysis for VERification of Systems)是美国麻省Amherst大学先进软件工程研究实验室研发的支持有穷状态验证方法的工具 有穷状态验证方法的局限性 首先，它所验证的是系统是否满足定义的行为性质（Behavioral Properties），而不是断定系统是否满足定义的规约（Specification）。 其次，它要求所论证的性质是表现为程序执行中某些关心的事件出现序列的集合，而且限定是能由有穷自动机所接受的事件序列表示的的集合，或等价地说该性质能表示成为正则表达式。 众所周知，有穷自动机所能接受的语言类，按Chomsky字的集合的分类是很小的类。 于是就产生了问题：能否找出新的验证方法，突破这种关于有穷自动机的限制？下面是我们所作的尝试。 3, 程序有穷路径验证方法 我们先从一个例子说起。假定我们编了一个程序，在程序中用了一个栈，要分别使用put和get调用这个栈进行“进栈”和“退栈”的动作。 为了验证程序的正确性，我们想验证put和get调用的序列是合适的，即验证程序是否满足如下性质：put和get的调用严格配对。 也就是说，要求栈在程序开始和终止时为空，get必须在栈不空时调用。例如下述序列就满足此性质： put get put put put get get put put get get get 突破程序有穷验证方法局限性 熟悉自动机理论的读者肯定知道，满足这样性质的序列集合是不可能用有穷自动机接受的。它是由如下文法生成的语言： S ? ε | put S get | S S 接受这种语言的至少是下推自动机，可见用有穷验证方法是验证不了这种性质的。 为了突破程序有穷验证方法局限性，我们尝试提出了一种新的方法，称为“有穷路径验证法”。在这种方法中，表示所论证的性质的自动机可以推广到使用任何一类自动机，如下推自动机、线性有界自动机甚至图灵机等。 基本有向图 定义3.1 我们称一个有向图是基本有向图，如果它仅有一个始点和一个终点，而且对图中任何节点，都有从始点到此节点的路径和从此节点到终点的路径。所谓始点是指无入边的节点，终点是指无出边的节点。 定理3.1. 对于基本有向图，从始点到终点的所有路径都是无重复节点的必要充分条件是此有向图是无环的。 定理3.2. 定理3.2. 对于基本有向图，从始点到终点的所有不同的无重复节点的路径的个数是有穷的。 证明 对于由有穷节点组成的有向图，它的任何无重复节点的路径的长度肯定是有穷的 （小于节点个数）。所以，从始点到终点的所有不同的无重复节点的路径的个数是有穷的。 求从始点到终点所有无重复节点路径的算法 算法3.1 算法对基本有向图T中所有节点 Ni，求出从始点到达此点 Ni 所有可能的无重复节点的路径集合 L(Ni)。 对于终点Z，L(Z) 即是T中从始点到终点的所有不同的无重复节点的路径的集合。 有穷路径验证方法 这种方法突破了有穷验证方法的限制，所论证的性质表示可以推广到使用任何一类自动机。 作为代价，描写系统的模型限制是无环的，而且在较复杂的情况下，算法的复杂度会增加，但是仍不失为一种有效的验证方法。 对于有环的描写系统的模型，本文提出了一种称之为“路径测试”的方法。与一般的程序测试方法不同的是这里的测试相对于性质和模型的路径，而不执行实际的程序。 路径测试方法的关键是产生测试路径。 定义4.1 对