《程序验证和自动分析工具研讨会20053上海ppt课件》由会员分享，可在线阅读，更多相关《程序验证和自动分析工具研讨会20053上海ppt课件（55页珍藏版）》请在金锄头文库上搜索。
1、程序验证与自动分析工具研讨会 2019.3 上海 郝克刚 西北大学计算机科学系 软件工程研究所论有穷状态验证方法(Finite State Verification)的局限性 提纲 1.引言2.程序有穷状态验证方法及其局限性分析3.程序有穷路径验证方法4.程序路径测试方法5.结束语1, 引言nLori A. Clarke: Finite State Verification: An Emerging Technology for Validating Software Systems. Clarke 教授 2019 在上海的演讲。iturls/Expert/exp-Lori.aspnLori
2、A. Clarke, : FLAVERS:A Finite State Verification Approach for Software Systems. Clarke 教授 2019.10 在西北大学的演讲。mainpage.nwu.edu/hkg/docs/Professor Lori A. Clarke Department of Computer Science , University of Massachusetts, Amherst.程序有穷状态验证方法n是介于程序验证和程序测试之间的一种方法。Ad-hoc TestingSystematic TestingTheorem P
3、rovingFinite State VerificationArbitrary testcasesReqts based test planningRequirements captured as propertiesProperties guaranteed on all possible executionsSpectrum of Difficulty有穷状态验证方法的局限性及突破的尝试n有穷状态验证方法有很大的局限性，它要求所论证的性质是由有穷自动机所接受的事件序列的集合。n本文讨论了这种局限性。尝试提出了一种新的方法，称为“有穷路径验证法”。表示所论证的性质的自动机可以推广到使用任何
4、一类自动机。作为代价，限制描写系统的模型是无环的。n对于有环的描写系统的模型，本文提出了 “路径测试的方法。与一般的程序测试不同的是这里的测试是相对于性质和模型的路径，而不执行实际的程序。2, 程序有穷状态验证方法简介及其局限性分析nFLAVERS (FLow Analysis for VERification of Systems)是美国麻省Amherst大学先进软件工程研究实验室研发的支持有穷状态验证方法的工具有穷状态验证方法验证过程结构图FLAVERS 验证过程结构图有穷状态验证方法验证过程结构图性质自动机、约束自动机：用带量词的正则表达式或有穷状态自动机FSA (finite-stat
5、e automaton)来表达性质和约束。 An Example :Elevator PropertyThe elevator does not move while its doors are open.L(P) is the set of all strings accepted by property automaton P1 12 23 3closecloseopenopenmovemovecloseclosemovemoveopenopenopenopencloseclosemovemoveproperty automaton有穷状态验证方法验证过程结构图根据所分析的系统的每个并行任
6、务的程序，建立标注的控制流图CFG (control-flow graph)，用以表示相关事件在系统中所有的执行序列 。Simple Sequential ExampleA:A:if (stopped) thenif (stopped) thenB:B:open;open;end if;end if;C:C:if (stopped) thenif (stopped) thenD:D:close;close;end if;end if;E:E:move;move;A: ifA: ifB: openB: openC: ifC: ifD: closeD: closeE: moveE: move控制流
7、图CFG有穷状态验证方法验证过程结构图由性质和约束确定了所关心的事件，它的名字决定了分析问题的字母表。 有穷状态验证方法验证过程结构图然后按照字母表将其精化为精化控制流图RCFG (refined CFG)。 有穷状态验证方法验证过程结构图把这些RCFGs组合起来，添加上反映任务间的同步和通信的节点和边，以及并行动作可能顺序的有向边，最后经过优化构成：追踪流图 TFG (trace-flow graph) task t1 body is begin u; t2.synch; v; w;end t1;task t2 body is begin x; accept synch; y; z;end
8、t2;TFG Constructionx xy yz zu uv vw waccept synchaccept syncht2.syncht2.synchsynchsynch有穷状态验证方法验证过程结构图FLAVERS的核心是它的状态传播算法，为TFG每个节点确定出所有到此节点的路径对应的性质自动机所可能到达的状态。 State Propagation1 12 23 3closecloseopenopenmovemovecloseclosemovemoveopenopenopenopencloseclosemovemoveB: openB: openD: closeD: closeE: mov
9、eE: moveC: ifC: ifA: ifA: ifWorklist: B, CWorklist: B, C, D, E, D, E111122111,21,21,21,2111,21,21,31,31,21,2有穷状态验证方法验证过程结构图假设 TFG 的终止节点对应的所有状态都是性质自动机的终止状态，则可以得出肯定的验证结论： 系统具有所要求的性质。 有穷状态验证方法验证过程结构图如果算法分析的结果是非肯定的结论，即与TFG的终止节点对应的状态并非所有都是有穷状态自动机的终止状态，则有两种可能：1，提供了系统可能不具有所要求的性质的反例的信息，或者2，说明系统的模型不够精确。 有穷状态
10、验证方法验证过程结构图 TFG只是一种近似，它也可能包含某些实际上不可能出现的序列。如果是这种序列导致了有穷状态自动机的非终止状态，则不能断定系统不具有该性质。 在这种情况下需要引入约束，删除掉这些实际上不可能出现的序列，最后再判断能否得出肯定的分析结果。 有穷状态验证方法验证过程结构图 约束由有穷自动机定义。约束自动机中有一个状态称为违背状态。凡是到达违背状态的事件序列都是实际上不可能出现的序列，应从分析中删除。 约束有各种类型，如变量、义务、环境和界面等类型的约束 。 = is a predicate= is assignmentViolS=trueS=trueS=trueS=trueS=
11、trueS=falseS=falseS=falseS=true S=trueS=false S=falseS=falseS=falseS=falseS=trueTrueFalseUnknown Boolean Variable ConstraintS: stoppedBoolean Variable Constraint1 12 23 3closecloseopenopenmovemovecloseclosemovemoveopenopenopenopencloseclosemovemoveB: openB: openD: closeD: closeE: moveE: moveC: ifC:
12、ifA: ifA: if111122111,21,21,21,2111,21,21,31,31,21,2Boolean Variable ConstraintB: openB: openD: closeD: closeE: moveE: moveC: ifC: ifA: ifA: if111122111,21,21,21,2111,21,21,31,31,21,2UTVA:A:if (stopped) thenif (stopped) thenB:B:open;open;end if;end if;C:C:if (stopped) thenif (stopped) thenD:D:close;
13、close;end if;end if;E:E:move;move;X有穷状态验证方法的局限性n首先，它所验证的是系统是否满足定义的行为性质Behavioral Properties），而不是断定系统是否满足定义的规约Specification）。n其次，它要求所论证的性质是表现为程序执行中某些关心的事件出现序列的集合，而且限定是能由有穷自动机所接受的事件序列表示的的集合，或等价地说该性质能表示成为正则表达式。n众所周知，有穷自动机所能接受的语言类，按Chomsky字的集合的分类是很小的类。n于是就产生了问题：能否找出新的验证方法，突破这种关于有穷自动机的限制？下面是我们所作的尝试。3, 程序
14、有穷路径验证方法n我们先从一个例子说起。假定我们编了一个程序，在程序中用了一个栈，要分别使用put和get调用这个栈进行“进栈和“退栈的动作。n为了验证程序的正确性，我们想验证put和get调用的序列是合适的，即验证程序是否满足如下性质：put和get的调用严格配对。n也就是说，要求栈在程序开始和终止时为空，get必须在栈不空时调用。例如下述序列就满足此性质：nput get put put put get get put put get get get突破程序有穷验证方法局限性n熟悉自动机理论的读者肯定知道，满足这样性质的序列集合是不可能用有穷自动机接受的。它是由如下文法生成的语言： S |
15、 put S get | S Sn接受这种语言的至少是下推自动机，可见用有穷验证方法是验证不了这种性质的。n为了突破程序有穷验证方法局限性，我们尝试提出了一种新的方法，称为“有穷路径验证法”。在这种方法中，表示所论证的性质的自动机可以推广到使用任何一类自动机，如下推自动机、线性有界自动机甚至图灵机等。 有穷路径验证方法性质的自动机 推广到可以使用任何一类自动机，如下推自动机、线性有界自动机甚至图灵机等。 路径的产生和验证有穷路径验证方法n 作为代价，限制描写系统各并行系统的模型 RCFGs 是无环的，n 可以证明，对于无环的基本有向图，所有路径都是无重复节点的路径。 路径的产生和验证基本有向图
16、n定义定义3.1 我们称一个有向图是基本有向图，如果我们称一个有向图是基本有向图，如果它仅有一个始点和一个终点，而且对图中任何节它仅有一个始点和一个终点，而且对图中任何节点，都有从始点到此节点的路径和从此节点到终点，都有从始点到此节点的路径和从此节点到终点的路径。所谓始点是指无入边的节点，终点是点的路径。所谓始点是指无入边的节点，终点是指无出边的节点。指无出边的节点。n定理定理3.1. 对于基本有向图，从始点到终点的所有对于基本有向图，从始点到终点的所有路径都是无重复节点的必要充分条件是此有向图路径都是无重复节点的必要充分条件是此有向图是无环的。是无环的。有穷路径验证方法n 这些RCFGs的无
17、环性并不能保证由它们组合起来TFG是无环的。n 为描述并行动作可能形成的顺序而添加的有向边可能在TFG形成环，但是实际上由此而生成的有重复节点的路径，在并行系统地执行中却是实际不存在的。n 所以从理论上讲，反映系统中相关的事件的执行序列的是TFG的无重复节点的路径。 路径的产生和验证x xy yu uv vw wsynchsynchz ztask t1 body is begin u; t2.synch; v; w;end t1;task t2 body is begin x; accept synch; y; z;end t2;TFG Constructionn 为描述并行动作可能形成的顺序
18、而添加的有向边可能在TFG形成环，但是实际上由此而生成的有重复节点的路径，在并行系统地执行中却是实际不存在的。n 所以从理论上讲，反映系统中相关的事件的执行序列的是TFG的无重复节点的路径。 定理定理3.2.n定理定理3.2. 对于基本有向图，从始点到终点的对于基本有向图，从始点到终点的所有不同的无重复节点的路径的个数是有穷所有不同的无重复节点的路径的个数是有穷的。的。n证明证明 对于由有穷节点组成的有向图，它的对于由有穷节点组成的有向图，它的任何无重复节点的路径的长度肯定是有穷的任何无重复节点的路径的长度肯定是有穷的 （小于节点个数）。所以，从始点到终点的（小于节点个数）。所以，从始点到终点
19、的所有不同的无重复节点的路径的个数是有穷所有不同的无重复节点的路径的个数是有穷的。的。有穷路径验证方法路径的产生和验证n求出 TFG 中从始点到终点的所有无重复节点路径。n对此所有路径，用性质自动机来判断验证。求从始点到终点所有无重复节点路径的算法n算法算法3.1 算法对基本有向图算法对基本有向图T中所有节点中所有节点 Ni，求出从始点到达此点，求出从始点到达此点 Ni 所有可能的无重所有可能的无重复节点的路径集合复节点的路径集合 L(Ni)。n对于终点对于终点Z，L(Z) 即是即是T中从始点到终点的中从始点到终点的所有不同的无重复节点的路径的集合。所有不同的无重复节点的路径的集合。算法算法3
20、.1续）续）1.算法开始时，令T中所有节点Ni上的所求的路径集合为空集合L(Ni)= 。2.令始点S的路径集合L(S)=S。3.对图中所有的由有向边连接的节点Q和H，其中Q是前节点，H是后节点，作如下动作。 如果有路径 L(Q) 满足条件： 节点H 不在 中出现，而且 路径H不包含在H 的路径集合L(H) 中， 则将路径H 加入到L(H) 中，即令 L(H) = L(H) U H4.重复动作3，直至所有的由有向边连接的节点Q和H，L(Q) 中没有满足上述条件的路径。L(H)L(Q)QHA: put ifA: put ifB: putB: putC: ifC: ifD: getD: getE:
21、getE: getA:A: put put if (stopped) then if (stopped) thenB:B:put;put;end if;end if;C:C:if (stopped) thenif (stopped) thenD:D:get;get;end if;end if;E:E: get; get;求从始点到终点所有无重复节点路径A: put ifA: put ifB: putB: putC: ifC: ifD: getD: getE: getE: get求从始点到终点所有无重复节点路径L(A)= A L(B)= AB L(C)= ABC,AC L(D)= ABCD,AC
22、DL(E)=ABCDE,ACDE,ABCE,ACE 有穷路径验证方法路径的产生和验证n求出 TFG 中从始点到终点的所有无重复节点路径。n对所有这些路径，用性质自动机来判断。n如果所有路经皆被性质自动机所接受，则通过验证，证明系统满足此性质。有穷路径验证方法路径的产生和验证 如果有路径不被性质自动机所接受，同有穷状态验证一样，有两种可能： 增加约束，提高模型的近似度，删掉不现实的路径，继续验证过程。 如果该路经是现实的，则提供信息帮助找到系统违背性质的反例。 A: put ifA: put ifB: putB: putC: ifC: ifD: getD: getE: getE: get增加约束
23、，提高模型的近似度，删掉不现实的路径L(E)=ABCDE,ACDE,ABCE,ACE UTVUVFV 如果有路径不被性质自动机所接受，同有穷状态验证一样，有两种可能： 增加约束，提高模型的近似度，删掉不现实的路径，继续验证过程。 如果该路经是现实的，则提供信息帮助找到系统违背性质的反例。 有穷路径验证方法n这种方法突破了有穷验证方法的限制，所论证的性质表示可以推广到使用任何一类自动机。n作为代价，描写系统的模型限制是无环的，而且在较复杂的情况下，算法的复杂度会增加，但是仍不失为一种有效的验证方法。n对于有环的描写系统的模型，本文提出了一种称之为“路径测试的方法。与一般的程序测试方法不同的是这里
24、的测试相对于性质和模型的路径，而不执行实际的程序。 4，程序路径测试方法路径的产生和测试 对于RCFG 有环 的情况，路径可能有重复的节点，而且这种路径的个数一般是无穷的。所以，用穷尽所有路径的方法进行验证是不可能的。4，程序路径测试方法路径的产生和测试 n 不过，我们可以用路径是否被性质自动机所接受来测试所关心的性质是否对此路径成立。n 当然，用这种方法通过某些路径的测试不能正面地验证程序的正确性。n 可是，如果对某路径通不过测试，则能像一般的程序测试方法那样，帮你发现反例，找出程序的错误。路径测试方法的关键是产生测试路径。n定义定义4.1 对基本有向图的某节点对基本有向图的某节点N，我们称
25、路径，我们称路径为节点为节点N的小环路经，如果的小环路经，如果以以N为第一个和最后一个节点，而为第一个和最后一个节点，而且除此以外无重复节点的路径。如果某节点且除此以外无重复节点的路径。如果某节点N有小环路经，有小环路经，则称此节点为环节点。则称此节点为环节点。n算法算法 4.1求小环路经集合的算法假设有基本有向图求小环路经集合的算法假设有基本有向图T和他的某个节点和他的某个节点N。对。对T中所有节点中所有节点Ni ，本算法求出从节，本算法求出从节点点N到达此点到达此点Ni所有可能的无重复节点的路径集合所有可能的无重复节点的路径集合X(Ni) （只有在（只有在Ni =N的情况下，允许路径的首和
26、尾是的情况下，允许路径的首和尾是N是重复是重复的）的） 。对于节点。对于节点N，X(N) 即是节点即是节点N的所有的小环路径的所有的小环路径的集合。如果的集合。如果X(N)不空，则节点不空，则节点N是环节点。是环节点。 ABDCEX(B)=BX(D)=BCDX(C)=BCX(E)=BCE求节点 B 的小环路径的集合ABDCE求节点 B 的小环路径的集合X(B)=B，BCDBX(D)=BCDX(C)=BCX(E)=BCEABDCE求节点 B 的小环路径的集合X(B)= BCDB 路径的加环操作n定义定义4.2 假设有基本有向图假设有基本有向图T的某路径的某路径，如果，如果中有一个节点中有一个节点
27、N是环节点，是环节点，是节点是节点N的某小环路的某小环路经，我们把由经，我们把由，将其中节点，将其中节点N替换为替换为生成的路生成的路径称为由径称为由加环生成的路径。加环生成的路径。n定理定理4.1 若若是基本有向图是基本有向图T的路径，则由的路径，则由加环加环生成的路径都是图生成的路径都是图T的路径。的路径。n定理定理4.2 基本有向图基本有向图T的任何路径，都可以由的任何路径，都可以由T的的某从始点到终点的无重复路径，经过有穷次的加某从始点到终点的无重复路径，经过有穷次的加环操作而生成。环操作而生成。ABDCE任何路径，都可以由某从始点到终点的无重复路径，经过有穷次的加环操作而生成。X(B
28、)= BCDB ABCEA BCDB CEA BCD BCDB CE 4，程序路径测试方法路径的产生和测试 n 对产生的路径，用性质自动机来测试所关心的性质是否对此路径成立。n 路径通过测试不能正面地验证程序的正确性。n 可是，如果对某路径通不过测试，则能像一般的程序测试方法那样，可能帮你发现反例，找出程序的错误。5，结束语n本文讨论了程序的有穷状态验证方法的局限性，并尝试突破性质自动机只能使用有穷自动机的限制，提出了“有穷路径验证法”。在这种方法中，所论证的性质表示可以推广到使用任何一类自动机。作为代价，描写系统的模型限制是无环的，而且在较复杂的情况下，算法的复杂度会增加，但是仍不失为一种有
29、效的验证方法。n对于有环的描写系统的模型，本文提出了 “路径测试法” 。与一般的程序测试方法不同的是这里的测试相对于性质和模型的路径，而不执行实际的程序。5，结束语续）n这只是初步研究工作的报告，对于该方法的进一步研究，特别是有关理论方面、实际应用方面和支持工具的研发方面还将继续。n本工作受国家863计划“软件评测平台的研究与应用课题2019AA115090的资助。课题背景说明： 软件评测平台的研究与应用课题旨在进一步完善西安863软件专业孵化器软件评测平台的服务功能，提升西安863软件专业孵化器为软件企业提供软件开发、质量管理、软件评测及专业技术培训等服务的能力。研究内容主要包括软件测试理论的研究、测试工具和测试管理工具的研发、软件BUG管理与度量工具的开发等。详细内容可参阅：葛 玮，龚晓庆，郝克刚： “论有穷状态验证方法的局限性”， 西北大学计算机科学系 软件工程研究所研究报告，2019.3 。mainpage.nwu.edu/hkg/docs/西北大学 软件工程研究所 所长计算机科学系软件专业 教授、博导hkgnwu.edumainpage.nwu.edu/hkg/home/
