（计算机软件与理论专业论文）面向对象并发程序切片技术及其在程序验证中的应用.pdf

面向对象并发程序切片技术及其在程序验证中的应用中文摘要 中文摘要 程序切片是一种重要的程序分析技术，它通过提取程序中直接或间接影响某个特 定程序点变量值的语句达到分解程序的目的。随着对程序切片技术研究的深入，其应 用领域由软件调试、测试、软件维护扩展到逆向工程、再工程和程序验证等。 面向对象技术仍是目前软件开发方法的主流，其中封装、继承、多态、并发等特 征都为程序的理解与分析提出了新的问题。本文针对面向对象程序的并发机制，介绍 了程序的图形化表示方法面向对象并发系统依赖图，提出利用变量缓存表分析程 序语句间依赖关系的方法，根据分析结果构造面向对象并发系统依赖图，并在此基础 上采用改进的两步遍历图可达性算法计算动态切片。 程序验证面临的主要问题是由于程序规模的增大，尤其是并发分量的增加，所带 来的状态空间爆炸问题。程序切片可以将程序中不影响待验证性质的语句删除以减小 针对该程序抽象出的模型的复杂性，从而缩减其对应的状态空间，在一定程度上缓解 状态空间爆炸问题。本文提出一种从待验证的线性时序逻辑( l t l ) 性质中提取出切 片准则对程序进行切片的方法，切片后的程序与原程序关于待验证的l t l 性质具有 相同的可满足性，而其对应的状态转换图中的状态个数明显减少。 随着i n t e m e t 技术和w w w 技术的发展，w e b 应用涉及的范围越来越广，程序规 模在不断扩大，其复杂性也越来越高。针对j a v aw e b 开发中关键技术的实现机制， 把程序切片技术引入到w e b 应用程序的分析中，定义了w e b 应用程序中存在的依赖 关系，提出了一种构造w r e b 程序系统依赖图并计算程序切片的方法。 在以上工作的基础上，本文以j a v a 语言实现的典型并发程序为例对以上提出的 方法在实际开发中的应用进行了说明、分析。 关键字：程序切片；面向对象并发程序；程序验证；w e b 应用 作者：何志学 指导老师：张广泉 a b s t r a c t p r o g r a ms l i c i n gi sap r o g r a ma n a l y s i st e c h n i q u ew h i c he x t r a c t st h ee l e m e n t so fa p r o g r a mr e l a t e dt oap a r t i c u l a rc o m p u t a t i o n ap r o g r a ms l i c ec o n s i s t so ft h ep a r t so r c o m p o n e n t so fap r o g r a mt h a t ( p o t e n t i a l l y ) a f f e c tt h ev a l u e sc o m p u t e da ts o m ep o i n t so f i n t e r e s t ，r e f e r r e dt oa sas l i c i n gc r i t e r i o n s l i c i n gh a sb e e nw i d e l yu s e di nt e s t i n ga n d d e b u g g i n g , p r o g r a mc o m p r e h e n s i o n a n ds o f t w a r em a i n t e n a n c e ，e t c n o w ,w i t hi t s d e v e l o p m e n t ，t h ea r e ai se x t e n d e dt ot h er e e n g i n e e r i n g ，p r o g r a mv e r i f i c a t i o n ，e t c o b j e c t - o r i e n t e dp r o g r a ms t y l ei sb e c o m i n gt h en o r m s l i c i n go b j e c t - o r i e n t e dp r o g r a m s p r e s e n t sn e wc h a l l e n g e sw h i c ha r en o te n c o u n t e ri nt r a d i t i o n a lp r o g r a ms l i c i n g t o s l i c ea n o b j e c t o r i e n t e dp r o g r a m ，f e a t u r e ss u c ha se n c a p s u l a t i o n ，i n h e r i t a n c e ，p o l y m o r p h i s ma n d c o n c u r r e n c yn e e d e dt ob ec o n s i d e r e dc a r e f u l l y t h i sp a p e rp r e s e n t s an e wm e t h o dt o s l i c i n gc o n c u r r e n t j a v ap r o g r a m s w ei n t r o d u c ec o n c u r r e n to b j e c t - o r i e n t e ds y s t e m d e p e n d e n c eg r a p h ( c o s d g ) a st h ei n t e r m e d i a t ep r o g r a mr e p r e s e n t a t i o n o u rm e t h o d a p p l i e sv a r i a b l ec a c h et a b l e ( v c t ) t oa n a l y z et h ed e p e n d e n c i e si np r o g r a m sa n dt h e nt o c o n s t r u c tc o s d go ft h eg i v e np r o g r a m ，b u td o e sn o tu s ea n yt r a c ef i l et os t o r et h e e x e c u t i o nh i s t o r y b a s e do nt h i sm o d e l ，w eu s et h et w o - p a s ss l i c i n ga l g o r i t h mt oc o m p u t e a c c u r a t ed y n a m i cs l i c e so fac o n c u r r e n tj a v ap r o g r a m p r o g r a mv e r i f i c a t i o ni sa ni m p o r t a n tm e t h o di na s s u r i n gt h ec o r r e c t n e s sa n dr e l i a b i l i t y o fc o m p u t e rh a r d w a r ea n ds o f t w a r e o n eo ft h em a j o rp r o b l e m si ss p a c e - e x p l o s i o ni nt h e a p p l i c a t i o no ft h i sm e t h o dt oc o n c u r r e n ts o f t w a r es y s t e m s ：s t a t es p a c eg r o w se x p o n e n t i a l l y i nt h en u m b e ro fc o n c u r r e n tc o m p o n e n t s i nf a c t ，i ti so f t e nt h ec a s et h a ts o m eo ft h e s t a t e m e n t so ft h ep r o g r a ma r ei r r e l e v a n tt ot h ev e r i f i e dp r o p e r t ya n dc a nb ed e l e t e d i nt h i s p a p e r , w ep r e s e n ta na p p r o a c hf o rs l i c i n gc o n c u r r e n to b j e c t o r i e n t e dp r o g r a m st or e d u c e t h es t a t es p a c ei nt h ep r o c e s so fp r o g r a mv e r i f i c a t i o n t h es a t i s f a c t i o no ft h ev e r i f i e d p r o p e r t yi sg u a r a n t e e df o rb o t hp r o g r a m sb e f o r ea n d a f t e rs l i c i n g ，a n dt h en u m b e ro fs t a t e s i nt h es t a t et r a n s i t i o ng r a p hi sd e c r e a s e d w i t ht h ed e v e l o p m e n to fi n t e m e ta n dw w wt e c h n i q u e s ，w e ba p p l i c a t i o ni sw i d e l y u s e di nm a n ye - b u s i n e s sa r e a s a tt h es a m et i m e ，t h ef a c tt h a tl a r g e ra n dc o m p l e xw e b l i c o n c u r r e n to b j e c t o r i e n t e dp r o g r a ms l i c i n ga n di t sa p p l i c a t i o ni np r o g r a mv e r i f i c a t i o n a b s t r a c t a p p l i c a t i o np r o g r a m sb e c o m ei n c r e a s i n g l yam a i n s t r e a m ，i sc h a l l e n g i n gt h ep r o c e s so f d e v e l o p m e n t w ep r o p o s eam e t h o df o rs l i c i n gw e ba p p l i c a t i o np r o g r a mt oa n a l y z ea n d u n d e r s t a n dt h eb e h a v i o r so ft h ep r o g r a m b a s e do na l lt h e s ew o r k s ，w eg i v es o m et y p i c a le x a m p l e st oi l l u s t r a t eh o wt oa p p l yt h e m e t h o di n t op r a c t i c et h r o u g hj a v ac o n c u r r e n tp r o g r a m s k e y w o r d s ：p r o g r a ms l i c i n g ；c o n c u r r e n to b j e c t - o r i e n t e dp r o g r a m ；p r o g r a mv e r i f i c a t i o n ； w e b a p p l i c a t i o n i i i w r i t t e nb yh ez h i - x u e s u p e r v i s e db yz h a n gg u a n g q u a n 图表索弓 面向对象并发程序切片技术及其在程序验证中的应用 图表索引 图2 1c f g 例子程序8 图2 2c f g 示例8 图2 3 例子程序的程序依赖图1 0 图2 4 系统依赖图例子程序1 1 图2 5 系统依赖图1 1 图2 - 6 无定形切片例子程序1 4 图2 7 无定形切片1 4 图3 1 类例子程序1 6 图3 2 类依赖图1 6 图3 3 继承关系17 图3 - 4 多态方法实现程序1 7 图3 5 多态选择边1 8 图3 - 6v c t 例子程序2 3 图4 1 客户端和服务器端交互过程3 2 图4 2 客户端j s p 页面程序3 3 图4 3 服务器端s e r v l e t 程序3 5 图4 4w e b 应用程序系统依赖图3 6 图4 5k r i p k e 结构的有向图表示3 8 图4 - 6 满足a l - l t p 、e u t p 、彳卿酌缈的计算树4 0 图4 7 两条s t u t t e r i n g 等价路径4 3 图5 1 生产者一消费者问题j a v a 程序实现4 6 图5 - 2 生产者一消费者程序的t d g 和c o s d g 4 9 图5 3 简化的生产者一消费者j a v a 程序5 0 图5 - 4 简化生产者一消费者程序的并发系统依赖图5 1 图5 5 切片前例子程序的状态转换图5 2 图5 - 6 切片后例子程序的状态转换图5 2 表3 - 1 例子程序的v c t 2 3 表5 - 1 生产者一消费者程序的v c t 4 7 i v 苏州大学学位论文独创性声明及使用授权的声明 学位论文独创性声明 本人郑重声明：所提交的学位论文是本人在导师的指导下，独立进 行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不含 其他个人或集体己经发表或撰写过的研究成果，也不含为获得苏州大学 或其它教育机构的学位证书而使用过的材料。对本文的研究作出重要贡 献的个人和集体，均已在文中以明确方式标明。本人承担本声明的法律 责任。 研究生签名： 珥麦霍 日 期：趔监垒迎 学位论文使用授权声明 苏州大学、中国科学技术信息研究所、国家图书馆、清华大学论文 合作部、中国社科院文献信息情报中心有权保留本人所送交学位论文的 复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本 人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文 外，允许论文被查阅和借阅，可以公布( 包括刊登) 论文的全部或部分 内容。论文的公布 s i , s 2 e s ，且语句s l 执行之后，s 2 可能成为下一条 执行语句) ；路竹表示程序的入口节点；s e x i t 表示程序的出口节点。如果一个程序有 多个返回语句，则可以在图中设置一个虚拟节点，将其作为所有返回语句的后继节点， 从而保证控制流图的完整性。 定义2 2 直接前驱和后继：在c f g 中，若勺l ，s 2 e e ，那么称s l 是眈的直接前 驱，记作p r e ( s l ，s 9 ，相应的称3 2 是s l 的直接后继；语句s 的所有直接前驱的集合称 为s 的直接前驱集，并记作p r e d ( s ) 。s 的所有直接后继组成的集合称为j 的直接后继 集，记作s u c c ( s ) 。 定义2 3 可执行路径：设语句序列勺l ，观，s n 记作p a t h ，p a t h 是一条可执行路 径，当且仅当p r e ( s i ，8 i + 1 ) 对于户1 ，2 ，e e n 1 时均满足。 定义2 4 前驱和后继：在c f g 中，若j l ，8 2 之间存在一条可执行路径，且s l ： 3 2 ，则称s l 是s 2 的前驱，记为p r e * ( s l ，眈) ；反之，称j 2 是s l 的后继，记为s u e t 幸o l ，s 2 ) 。 定义2 5 后必经节点：在c f g 中，在程序入口到程序出口的任意一条可执行路 径上，如果存在两个节点s l 、3 2 ，每条经过j l 到程序出口的路径都要经过眈，那么称 眈是s l 的后必经节点。 在图2 1 例子程序中实现了取得两个正整数中的较大者，其对应的c f g 如图2 2 所示，& m 为程序的入v i 节点，即方法的头部；x i 。为程序的出口节点，即方法的返 回语句；节点2 为节点3 的直接前驱；铒枷，2 ，3 ，4 ，9 ，s e x i t 为一条可执行路径，在该 路径上，节点2 是节点9 的前驱，节点9 是节点2 的后必经节点，而节点4 不是节点 2 的后必经节点，因为从节点2 到节点& x i t 同时存在b t r v ，2 ，3 ，7 ，9 ，i t 这样一条可 执行路径。 7 第二章程序切片技术及其相关概念面向对象并发程序切片技术及其在程序验证中的应用 2 2 2 依赖关系 图2 1c f g 例子程序 图2 - 2c f g 示僻 程序切片技术的基础是依赖性分析，程序中语句间主要存在由访问变量引起的数 据依赖和由控制条件引起的控制依赖。 设对于语句s ，其定义集d e f ( s ) = 扛lx 是语句s 处定义或改变的变量) ，引用集r e f ( s ) = 缸lx 是语句s 处引用的变量) ，则设m 和刀为给定程序中两条不同的语句，如果有 一条从m 到，z 的执行路径，同时存在一个在m 处定义、刀处引用的变量，且该变量 在从m 到力的执行路径上的其他位置没有被重新定义，则称n 数据依赖于m 。 定义2 6 数据依赖：语句，2 数据依赖于语句m ，记作m 与n ，当且仅当： ( 1 ) 存在由m 到以的路径尸：s 1 = 研，s 2 ，驴刀，且存在一个变量v ，满足，d e j ( m 1 n r e a n ) ； 面向对象并发程序切片技术及其在程序验证中的应用第二章程序切片技术及其相关概念 ( 2 ) 对于路径p 上的其他语句s 尸一劬，疗) ，v 诺d e f ( s ) 。 设m 与以为给定程序中两条不同的语句，如果从m 至少可以引出两条执行路径， 其中一条导致刀的执行，而另一条可能导致，2 不执行，则称p , 控制依赖于m 。 定义2 7 控制依赖：语句, 控制依赖于语句所，记作m 与聆，当且仅当： ( 1 ) 存在由m 到1 , 的路径p ：s l = 聊，s 2 ，岛邗，对于路径p 上的其他语句 s 。p 一 加，刀，刀是j 的后必经节点； ( 2 ) 力不是m 的后必经节点。 在程序设计中，有三种主要的控制结构，分别为顺序结构，判断结构与循环结构。 顺序结构的语句在执行过程中依次执行，而控制依赖主要是由于控制结构改变程序流 向所引起的，在分析控制依赖的过程中，可以将顺序结构的语句简单看成一个程序节 点而不予考虑，因此只考虑判断结构、循环结构等会影响程序流程的语句。除此之外 还有其他的一些原因会引起控制依赖，例如过程调用、异常处理等。 2 2 3 程序依赖图与系统依赖图 为了分析程序语句间存在的依赖关系，需要对其进行抽象，本文采用基于图论的 图形化表示方法。对于含有单个方法的程序而言，可以用程序依赖图表示；对于实际 应用中具有多个过程的程序而言，可以用系统依赖图来表示。 程序依赖图( p r o g r a md e p e n d e n c eg r a p h ，p d g ) 由控制流图、控制依赖图( c o n t r o l d e p e n d e n c eg r a p h ，c d g ) 和数据依赖图( d a t ed e p e n d e n c eg r a p h ，d d g ) 组成。其中 控制流图如定义2 1 所述，它描述了一个程序中的控制流；控制依赖图包含了程序中 的控制依赖关系，其中的语句节点表示程序中的语句，谓词节点表示程序中的循环或 分支条件；数据依赖图是一个程序中语句间的数据依赖关系的集合【3 5 1 。 定义2 8 控制依赖图：控制依赖图c d g 是一个有向图 c ) ，其中节点集s 是程 序中所有语句对应的节点集合；如果有语句眈直接控制依赖于语句s l ，也就是有 墨与是，则把边岛寸岛加入到边集c 中。 定义2 9 数据依赖图：数据依赖图d d g 是一个有向图( sd ) ，其中节点集s 是程 序中所有语句对应的节点集合，如果有语句娩数据依赖于语句j l ，也就是有 墨蔓b j ，则把边墨寸s ，加入到边集d 中。 定义2 1 0 程序依赖图：程序依赖图p d g 是一个二元组岱，e ) ，g = s 是对应语 9 第二章程序切片技术及其相关概念面向对象并发程序切片技术及其在程序验证中的应用 句的节点集合，边集e = e l ue 2 u 工其中：e l = is l 与j 2 ) 为控制 依赖边；e 2 = ls 。与s ： 为数据依赖边；x 表示程序中的其他依赖关系。 对于程序p 中的两个语句s l ，s 2 ，若有s l 与j 2 或者j l 丝专s 2 成立，则称8 1 直接依赖于眈，记作d e p ( s l ，s 2 ) 。 根据以上性质，我们可以定义传递依赖关系如下： 对于方法m 中的三个语句s l 、鼢s 3 ，s 1 传递依赖于s 3 ，记为d e p + ( s l ，s 3 ) ，当且 仅当下面两个条件之一成立： ( 1 ) d e p ( s 1 s 3 ) ( 2 ) 了s 2 ( d e p ( s l ，s 2 ) ad e p 。( s 2 ，s g ) 图2 3 是图2 1 中例子程序对应的p d g ，其中控制依赖关系为 3 与4 ， 3 堕专7 ) ，数据依赖关系为 2 丝专9 ，4 堂专9 ，7 鱼0 9 ) 。 _ _ - _ _ _ 卜 c o n t r o ld e p e n d e n c e 一 d a t ad e p e n d e n c e 图2 3 例子程序的程序依赖图 在实际的应用中，一个程序往往有多个过程相互调用来实现其功能。h o r w i t s 等 人引入了系统依赖图【3 l ( s y s t e md e p e n d e n c eg r a p h ，s d g ) 的概念来表示具有多个过程 的程序依赖图。一个s d g 是由一组过程间控制依赖边和流控制依赖边连接起来的过 程依赖图( p r d g ) 组成，p r d g 类似于p d g ，但它还包括表示由于调用而形成的调用语 句、参数传递、可传递流依赖的节点和边。一个调用语句用一个调用节点( c a l lv e a e x ) 表示，用四种参数表示参数传递：在调用处，用a c t u a li n 和a c t u a lo u t 表示实际输入 参数和输出参数，它们控制依赖于调用节点；在被调用过程中，用f o r m a li n 和 f o r m a lo u t 表示形式输入参数和输出参数，它们控制依赖于过程入口节点。 可传递的依赖边，又称s u m m a r y 边，加到a c t u a li n 节点和a c t u a lo u t 节点之间来 表示由于调用过程而形成的可传递流依赖。如果在被调用过程中相应的f o r m a li n 节 点和f o r m a lo u t 节点之间存在一条控制路径、流边或s u m m a r y 边，则在a c t u a li n 和 1 0 面向对象并发程序切片技术及其在程序验证中的应用第二章程序切片技术及其相关概念 a c t u a lo u t 之间加入一条s u m m a r y 边。 使用三种类型的边把过程依赖图( p r d g ) 连接起来形成s d g 。 ( 1 ) 调用边( c a l le d g e ) ：在每个调用位置节点和相应的过程入v 1 节点之间加入 调用边。 ( 2 ) 参数输入边( p a r a m e t e ri n ) ：在调用位置的每个a c t u a li n 节点到被调用过 程相应的f o r m a li n 节点之间加入参数输入边。 ( 3 ) 参数输出边( p a r a m e t e ro u t ) ：从被调用过程的f o r m a lo u t 节点加一条边到 相应的调用位置的a c t u a lo u t 节点。 例如对于图2 - 4 中的程序，其对应的系统依赖图如图2 5 所示，其中在语句3 处 调用了过程a v g ，语句3 和语句5 之间加入调用依赖边；实参彳、b 与形参，、j 之 间加入参数输入边；过程a v g 返回值，与输出语句间加入参数输出边；在语句7 中， 变量j 依赖于自身和五所以a c t u a l i n a 、a c t u a l i nb 与a c t u a l o u t a 之间加入s u m m a r y 边。 图2 4 系统依赖图例子程序 图2 5 系统依赖图 第二章程序切片技术及其相关概念 面向对象并发程序切片技术及其在程序验证中的应用 2 3 程序切片的分类 从程序切片概念的最初提出到现在，切片技术一直随着软件设计、开发方法和程 序设计语言的发展而不断发展。以下从两个不同的角度介绍程序切片的分类。 按照切片过程中在程序依赖图中遍历方向的不同对其分类如下： ( 1 ) 后向切片 给定程序p ，语句s 和该语句处的变量v ，根据切片准贝t j ，其 中j 为欲切片程序中的一条语句，v 为s 处定义或引用的变量，矗为程序中某一个输 入变量的具体值。如果精确到s 语句的某一次出现，则切片准则可扩展为勺，1 ，i o ， f n ，胗其中n 代表在计算切片时考虑的是语句s 在程序执行过程中的第刀次出现。例如 在图2 1 中，对于动态切片准贝j j ，其中4 和7 分别代表x 和j ，的输入值， 则切片后的程序为 1 ，2 ，3 ，7 ，9 。而在计算切片准则 对应的静态切片时，切 片后的程序为 l ，2 ，3 ，4 ，7 ，9 ) 。可以看出，与静态切片相比，动态切片减