面向对象并发程序切片技术及其在程序验证中的应用
|
摘要
程序切片是一种重要的程序分析技术,它通过提取程序中直接或间接影响某个特定程序点变量值的语句达到分解程序的目的。随着对程序切片技术研究的深入,其应用领域由软件调试、测试、软件维护扩展到逆向工程、再工程和程序验证等。
面向对象技术仍是目前软件开发方法的主流,其中封装、继承、多态、并发等特征都为程序的理解与分析提出了新的问题。本文针对面向对象程序的并发机制,介绍了程序的图形化表示方法——面向对象并发系统依赖图,提出利用变量缓存表分析程序语句间依赖关系的方法,根据分析结果构造面向对象并发系统依赖图,并在此基础上采用改进的两步遍历图可达性算法计算动态切片。
程序验证面临的主要问题是由于程序规模的增大,尤其是并发分量的增加,所带来的状态空间爆炸问题。程序切片可以将程序中不影响待验证性质的语句删除以减小针对该程序抽象出的模型的复杂性,从而缩减其对应的状态空间,在一定程度上缓解状态空间爆炸问题。本文提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法,切片后的程序与原程序关于待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。
随着Internet技术和WWW技术的发展,Web应用涉及的范围越来越广,程序规模在不断扩大,其复杂性也越来越高。针对Java Web开发中关键技术的实现机制,把程序切片技术引入到Web应用程序的分析中,定义了Web应用程序中存在的依赖关系,提出了一种构造Web程序系统依赖图并计算程序切片的方法。
在以上工作的基础上,本文以Java语言实现的典型并发程序为例对以上提出的方法在实际开发中的应用进行了说明、分析。
Program slicing is a program analysis technique which extracts the elements of a program related to a particular computation. A program slice consists of the parts or components of a program that (potentially) affect the values computed at some points of interest, referred to as a slicing criterion. Slicing has been widely used in testing and debugging, program comprehension and software maintenance, etc. Now, with its development, the area is extended to the re-engineering, program verification, etc.
Object-oriented program style is becoming the norm. Slicing object-oriented programs presents new challenges which are not encounter in traditional program slicing. To slice an object-oriented program, features such as encapsulation, inheritance, polymorphism and concurrency needed to be considered carefully. This paper presents a new method to slicing concurrent Java programs. We introduce concurrent object-oriented system dependence graph (COSDG) as the intermediate program representation. Our method applies variable cache table (VCT) to analyze the dependencies in programs and then to construct COSDG of the given program, but does not use any trace file to store the execution history. Based on this model, we use the two-pass slicing algorithm to compute accurate dynamic slices of a concurrent Java program.
Program verification is an important method in assuring the correctness and reliability of computer hardware and software. One of the major problems is space-explosion in the application of this method to concurrent software systems: state space grows exponentially in the number of concurrent components. In fact, it is often the case that some of the statements of the program are irrelevant to the verified property and can be deleted. In this paper, we present an approach for slicing concurrent object-oriented programs to reduce the state space in the process of program verification. The satisfaction of the verified property is guaranteed for both programs before and after slicing, and the number of states in the state transition graph is decreased.
With the development of Internet and WWW techniques, Web application is widely used in many e-business areas. At the same time, the fact that larger and complex Web application programs become increasingly a mainstream, is challenging the process of development. We propose a method for slicing Web application program to analyze and understand the behaviors of the program.
Based on all these works, we give some typical examples to illustrate how to apply the method into practice through Java concurrent programs.
面向对象技术仍是目前软件开发方法的主流,其中封装、继承、多态、并发等特征都为程序的理解与分析提出了新的问题。本文针对面向对象程序的并发机制,介绍了程序的图形化表示方法——面向对象并发系统依赖图,提出利用变量缓存表分析程序语句间依赖关系的方法,根据分析结果构造面向对象并发系统依赖图,并在此基础上采用改进的两步遍历图可达性算法计算动态切片。
程序验证面临的主要问题是由于程序规模的增大,尤其是并发分量的增加,所带来的状态空间爆炸问题。程序切片可以将程序中不影响待验证性质的语句删除以减小针对该程序抽象出的模型的复杂性,从而缩减其对应的状态空间,在一定程度上缓解状态空间爆炸问题。本文提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法,切片后的程序与原程序关于待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。
随着Internet技术和WWW技术的发展,Web应用涉及的范围越来越广,程序规模在不断扩大,其复杂性也越来越高。针对Java Web开发中关键技术的实现机制,把程序切片技术引入到Web应用程序的分析中,定义了Web应用程序中存在的依赖关系,提出了一种构造Web程序系统依赖图并计算程序切片的方法。
在以上工作的基础上,本文以Java语言实现的典型并发程序为例对以上提出的方法在实际开发中的应用进行了说明、分析。
Program slicing is a program analysis technique which extracts the elements of a program related to a particular computation. A program slice consists of the parts or components of a program that (potentially) affect the values computed at some points of interest, referred to as a slicing criterion. Slicing has been widely used in testing and debugging, program comprehension and software maintenance, etc. Now, with its development, the area is extended to the re-engineering, program verification, etc.
Object-oriented program style is becoming the norm. Slicing object-oriented programs presents new challenges which are not encounter in traditional program slicing. To slice an object-oriented program, features such as encapsulation, inheritance, polymorphism and concurrency needed to be considered carefully. This paper presents a new method to slicing concurrent Java programs. We introduce concurrent object-oriented system dependence graph (COSDG) as the intermediate program representation. Our method applies variable cache table (VCT) to analyze the dependencies in programs and then to construct COSDG of the given program, but does not use any trace file to store the execution history. Based on this model, we use the two-pass slicing algorithm to compute accurate dynamic slices of a concurrent Java program.
Program verification is an important method in assuring the correctness and reliability of computer hardware and software. One of the major problems is space-explosion in the application of this method to concurrent software systems: state space grows exponentially in the number of concurrent components. In fact, it is often the case that some of the statements of the program are irrelevant to the verified property and can be deleted. In this paper, we present an approach for slicing concurrent object-oriented programs to reduce the state space in the process of program verification. The satisfaction of the verified property is guaranteed for both programs before and after slicing, and the number of states in the state transition graph is decreased.
With the development of Internet and WWW techniques, Web application is widely used in many e-business areas. At the same time, the fact that larger and complex Web application programs become increasingly a mainstream, is challenging the process of development. We propose a method for slicing Web application program to analyze and understand the behaviors of the program.
Based on all these works, we give some typical examples to illustrate how to apply the method into practice through Java concurrent programs.
引文
[1]Weiser M. Program slicing. IEEE Transaction on Software Engineering, 1984, 10(4): 352-357.
[2]李必信, 郑国梁, 李宣东, 等. 一种分析和理解程序的方法——程序切片. 计算机研究与发展, 2000, 37(3): 284-291.
[3]Horwitz S, Teps T, Binkley D. Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems, 1990, 12(1): 26-61.
[4]Frrante J, Ottenstein K, Warren J. The program dependence graph and its use in optimization. ACM Transaction on Programming Languages and System, 1987, 9 (3): 319-349.
[5]Krishnaswamy A. Program slicing: An application of object-oriented program dependency graphs. Technical report, Department of computer Science, Clemson University, 1994.
[6]Larson L, Harrold M J. Slicing object-oriented software. In Proceedings of the 18th International Conference of Software Engineering, 1996: 495-505.
[7]Cheng J. Slicing concurrent programs – a graph theoretical approach. In Automated and Algorithmic Debugging, AADEBUG’93, LNCS, Springer-Verlag, 1993: 223- 240.
[8]Krinke J. Static slicing of threaded programs. In proceedings of ACM SIGPLAN /SIGFSOFT Workshop on program Analysis for Software Tools and Engineering, 1998, 33(7): 35-42.
[9]Krinke J. Context-sensitive slicing of concurrent programs. In Proceedings of ACM SIGSOFT Software Engineering Notes, 2003: 178-187.
[10]Nanda M G, Ramesh S. Slicing concurrent programs. Software Engineering Notes, 2000, 25(5): 180-190.
[11]Chen Z, Xu B. Slicing concurrent Java programs. ACM SIGPLAN Notices, 2001, 36 (4): 41-47.
[12]Chen Z, Xu B, Zhao J, et al. Slicing larger programs partially. In Proceedings of 2003 International Conference on Software Engineering Research and Practice, 2003.
[13]Chen Z, Xu B. Slicing object-oriented Java programs. ACM SIGPLAN Notices, 2001, 36(4): 33-40.
[14]Xu B, Qian J, Zhang X, et al. A brief survey of program slicing. ACM SIGSOFT Software Engineering Notes, 2005, 30(2): 1-36.
[15]陈振强, 徐宝文. 一种基于依赖性分析的类内聚度量方法. 软件学报, 2003, 14 (11): 1894-1856.
[16]陈振强, 徐宝文. 一种并发程序依赖性分析方法. 计算机研究与发展, 2002, 39 (2): 159-164.
[17]张迎周, 徐宝文. 一种新型形式化程序切片方法. 中国科学 E 辑 信息科学, 2008, 38(2): 161-176.
[18]张迎周, 徐宝文. 一种基于模块单子语义的动态程序切片方法. 计算机学报, 2006, 29(4): 526-534.
[19]李必信, 李宣东, 郑国梁. 一种系统依赖图的面向对象扩充方案. 软件学报, 2001, 12(2): 241-248.
[20]Li B, Zhao J. Dependence based representation for concurrent Java programs and it’s application to slicing. In Proceedings of ISFST, 2004: 105-112.
[21]李必信, 李宣东, 郑国梁, 等. 一种基于切片技术度量 Java 耦合性的框架. 计算机学报, 2001, 24(3): 259-265.
[22]李必信, 李宣东, 郑国梁, 等. 基于数据切片度量 Java 内聚性. 软件学报, 2001, 12(12): 1851-1858.
[23]Zhao J, Cheng J, Ushijima K A. dependence-based representation for concurrent object-oriented software maintenance. In Proceedings of 2nd Euromicro Conference on Software Maintenance and Reengineering, 1998: 60-66.
[24]Zhao J. Slicing concurrent Java programs. In Proceedings of the 7th IEEE International Workshop on Program Comprehension, 1999: 126-133.
[25]Zhao J. Slicing Aspect-Oriented Software. In Proceedings of the 10th IEEE International Workshop on Program Comprehension, 2002: 251-260.
[26]Zhao J, Yang H, Xiang L, et al. Change impact analysis to support architectural evolution. Journal of software maintenance and evolution: research and practice, 2002, 14(5): 317-333.
[27]Korel B, Rilling J. Dynamic program slicing methods. Information and Software Technology, 1998, 40: 647-659.
[28]Canfora G, Cimitile A, Lucia A. Conditioned program slicing. Information and Software Technology, 1998, 40(11-12): 595-607.
[29]Harman M, Danicic S. Amorphous program slicing. IEEE International Workshop on Program Comprehension, 1997: 70-79.
[30]Lyle J, Weiser M. Automatic program bug location by program slicing. In Proceedings of the 2th International Conference on Computers and Applications, 1987: 877-883.
[31]Jackson D, Rollins E. A new model of program dependences for reverse engineering. In Proceedings of the SIGSOFT Conference on Foundations of Software Engineering, 1994.
[32]Tip F. A survey of program slicing techniques. Journal of Program Languages, 1995, 3(3): 121-189.
[33]Harman M, Hierons R M. An overview of program slicing. Software Focus, 2001, 2 (3): 85-92.
[34]Mohapatra D, Mall R, Kumar R. An overview of slicing techniques for object- oriented programs. Informatica, 2006, 30: 253-277.
[35]李必信. 程序切片技术及其应用. 北京:科学出版社, 2006.
[36]Malloy B A, McGregor J D, Krishnaswamy A. An extensible program representation for object-oriented software. In Proceedings of ISFST, 2004: 105-112.
[37]李必信, 王云峰, 郑国梁, 等. 基于简化系统依赖图的静态粗粒度切片方法. 软件学报, 2001, 12(2): 204-211.
[38]陈振强. 基于依赖性分析的程序切片技术研究. 博士学位论文, 东南大学, 2003.
[39]Takada T, Ohata F, Inoue K. Dependence-cache slicing: a program slicing method using lightweight dynamic information. In Proceedings of the 10th International Workshop on Program Comprehension, 2002: 169-177.
[40]Mohapatra D P, Mall R, Kumar R. Computing dynamic slices of concurrent object- oriented programs. Information and software technology, 2005, 47(12): 805-817.
[41]戚晓芳, 徐宝文, 周晓宇. 一种基于程序可达图的并发程序依赖性分析方法. 电子学报, 2007, 35(2): 287-291.
[42]Ricca F, Tonella P. Construction of the system dependence graph for Web application slicing. In Proceedings of the 2th IEEE International Workshop on Source Code Analysis and Manipulation, 2002: 123-132.
[43]Tonella P, Ricca F. Web application slicing in presence of dynamic code generation. Automated Software Engineering, 2005, 12(2): 259-288.
[44]Wu J, Xu B, Jiang J. Slicing web application based on hyper graph. In Proceedings of the 3th International Conference on Cyberworlds, 2004: 177-181.
[45]Xu L, Xu B, Chen Z, et al. Regression test for web applications based on slicing. In Proceedings of the 27th Annual International Computer Software Applications Conference, 2003: 652-656.
[46]张健, 蒋昌俊, 徐宝文. 软件的测试、分析与验证.中国计算机科学技术发展报告, 2005: 45-58.
[47]张健. 关于程序验证的新运动.信息技术快报, 2006, 4(2): 1-3.
[48]戎玫, 张广泉. 模型检测新技术研究. 计算机科学, 2003, 30(5): 102-104.
[49]林惠民, 张文辉. 模型检测:理论、方法与应用. 电子学报, 2002, 30(增刊): 1907- 1913.
[50]古天龙. 软件开发的形式化方法. 北京:高等教育出版社, 2005: 141-142.
[51]Clarke E M, Grumberg JR O, Peled D A. Model Checking. Cambridge, Massachusetts: The MIT Press, 1999: 146-147.
[52]Millett L I, Teitelbaum T. Issues in slicing Promela and its application to model checking, protocol understanding, and simlation. International Journal on Software Tools for Technology Transfer, 2000, 2(4): 343-349.
[53]Hatcliff J, Dwyer M B, Zheng H. Slicing software for model construction. Higher- order and Symbolic Computation, 2000, 13(4): 315-353.
[54]Dwyer M B, Hatcliff J, Hoosier M, et al. Evaluating the effective of slicing for model reduction of concurrent object-oriented programs. LNCS 3920, Springer-Verlag, 2006: 73-89.
[55]董威, 王戟, 齐治昌. 并发程序的切片模型检验方法. 计算机学报, 2003, 26(3): 266-274.
[56]Wang J, Dong W, Qi Z. Slicing hierarchical automata for model checking UML statecharts. In Proceedings of the 4th International Conference on Formal Engineering Methods, 2002: 435-446.
[2]李必信, 郑国梁, 李宣东, 等. 一种分析和理解程序的方法——程序切片. 计算机研究与发展, 2000, 37(3): 284-291.
[3]Horwitz S, Teps T, Binkley D. Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems, 1990, 12(1): 26-61.
[4]Frrante J, Ottenstein K, Warren J. The program dependence graph and its use in optimization. ACM Transaction on Programming Languages and System, 1987, 9 (3): 319-349.
[5]Krishnaswamy A. Program slicing: An application of object-oriented program dependency graphs. Technical report, Department of computer Science, Clemson University, 1994.
[6]Larson L, Harrold M J. Slicing object-oriented software. In Proceedings of the 18th International Conference of Software Engineering, 1996: 495-505.
[7]Cheng J. Slicing concurrent programs – a graph theoretical approach. In Automated and Algorithmic Debugging, AADEBUG’93, LNCS, Springer-Verlag, 1993: 223- 240.
[8]Krinke J. Static slicing of threaded programs. In proceedings of ACM SIGPLAN /SIGFSOFT Workshop on program Analysis for Software Tools and Engineering, 1998, 33(7): 35-42.
[9]Krinke J. Context-sensitive slicing of concurrent programs. In Proceedings of ACM SIGSOFT Software Engineering Notes, 2003: 178-187.
[10]Nanda M G, Ramesh S. Slicing concurrent programs. Software Engineering Notes, 2000, 25(5): 180-190.
[11]Chen Z, Xu B. Slicing concurrent Java programs. ACM SIGPLAN Notices, 2001, 36 (4): 41-47.
[12]Chen Z, Xu B, Zhao J, et al. Slicing larger programs partially. In Proceedings of 2003 International Conference on Software Engineering Research and Practice, 2003.
[13]Chen Z, Xu B. Slicing object-oriented Java programs. ACM SIGPLAN Notices, 2001, 36(4): 33-40.
[14]Xu B, Qian J, Zhang X, et al. A brief survey of program slicing. ACM SIGSOFT Software Engineering Notes, 2005, 30(2): 1-36.
[15]陈振强, 徐宝文. 一种基于依赖性分析的类内聚度量方法. 软件学报, 2003, 14 (11): 1894-1856.
[16]陈振强, 徐宝文. 一种并发程序依赖性分析方法. 计算机研究与发展, 2002, 39 (2): 159-164.
[17]张迎周, 徐宝文. 一种新型形式化程序切片方法. 中国科学 E 辑 信息科学, 2008, 38(2): 161-176.
[18]张迎周, 徐宝文. 一种基于模块单子语义的动态程序切片方法. 计算机学报, 2006, 29(4): 526-534.
[19]李必信, 李宣东, 郑国梁. 一种系统依赖图的面向对象扩充方案. 软件学报, 2001, 12(2): 241-248.
[20]Li B, Zhao J. Dependence based representation for concurrent Java programs and it’s application to slicing. In Proceedings of ISFST, 2004: 105-112.
[21]李必信, 李宣东, 郑国梁, 等. 一种基于切片技术度量 Java 耦合性的框架. 计算机学报, 2001, 24(3): 259-265.
[22]李必信, 李宣东, 郑国梁, 等. 基于数据切片度量 Java 内聚性. 软件学报, 2001, 12(12): 1851-1858.
[23]Zhao J, Cheng J, Ushijima K A. dependence-based representation for concurrent object-oriented software maintenance. In Proceedings of 2nd Euromicro Conference on Software Maintenance and Reengineering, 1998: 60-66.
[24]Zhao J. Slicing concurrent Java programs. In Proceedings of the 7th IEEE International Workshop on Program Comprehension, 1999: 126-133.
[25]Zhao J. Slicing Aspect-Oriented Software. In Proceedings of the 10th IEEE International Workshop on Program Comprehension, 2002: 251-260.
[26]Zhao J, Yang H, Xiang L, et al. Change impact analysis to support architectural evolution. Journal of software maintenance and evolution: research and practice, 2002, 14(5): 317-333.
[27]Korel B, Rilling J. Dynamic program slicing methods. Information and Software Technology, 1998, 40: 647-659.
[28]Canfora G, Cimitile A, Lucia A. Conditioned program slicing. Information and Software Technology, 1998, 40(11-12): 595-607.
[29]Harman M, Danicic S. Amorphous program slicing. IEEE International Workshop on Program Comprehension, 1997: 70-79.
[30]Lyle J, Weiser M. Automatic program bug location by program slicing. In Proceedings of the 2th International Conference on Computers and Applications, 1987: 877-883.
[31]Jackson D, Rollins E. A new model of program dependences for reverse engineering. In Proceedings of the SIGSOFT Conference on Foundations of Software Engineering, 1994.
[32]Tip F. A survey of program slicing techniques. Journal of Program Languages, 1995, 3(3): 121-189.
[33]Harman M, Hierons R M. An overview of program slicing. Software Focus, 2001, 2 (3): 85-92.
[34]Mohapatra D, Mall R, Kumar R. An overview of slicing techniques for object- oriented programs. Informatica, 2006, 30: 253-277.
[35]李必信. 程序切片技术及其应用. 北京:科学出版社, 2006.
[36]Malloy B A, McGregor J D, Krishnaswamy A. An extensible program representation for object-oriented software. In Proceedings of ISFST, 2004: 105-112.
[37]李必信, 王云峰, 郑国梁, 等. 基于简化系统依赖图的静态粗粒度切片方法. 软件学报, 2001, 12(2): 204-211.
[38]陈振强. 基于依赖性分析的程序切片技术研究. 博士学位论文, 东南大学, 2003.
[39]Takada T, Ohata F, Inoue K. Dependence-cache slicing: a program slicing method using lightweight dynamic information. In Proceedings of the 10th International Workshop on Program Comprehension, 2002: 169-177.
[40]Mohapatra D P, Mall R, Kumar R. Computing dynamic slices of concurrent object- oriented programs. Information and software technology, 2005, 47(12): 805-817.
[41]戚晓芳, 徐宝文, 周晓宇. 一种基于程序可达图的并发程序依赖性分析方法. 电子学报, 2007, 35(2): 287-291.
[42]Ricca F, Tonella P. Construction of the system dependence graph for Web application slicing. In Proceedings of the 2th IEEE International Workshop on Source Code Analysis and Manipulation, 2002: 123-132.
[43]Tonella P, Ricca F. Web application slicing in presence of dynamic code generation. Automated Software Engineering, 2005, 12(2): 259-288.
[44]Wu J, Xu B, Jiang J. Slicing web application based on hyper graph. In Proceedings of the 3th International Conference on Cyberworlds, 2004: 177-181.
[45]Xu L, Xu B, Chen Z, et al. Regression test for web applications based on slicing. In Proceedings of the 27th Annual International Computer Software Applications Conference, 2003: 652-656.
[46]张健, 蒋昌俊, 徐宝文. 软件的测试、分析与验证.中国计算机科学技术发展报告, 2005: 45-58.
[47]张健. 关于程序验证的新运动.信息技术快报, 2006, 4(2): 1-3.
[48]戎玫, 张广泉. 模型检测新技术研究. 计算机科学, 2003, 30(5): 102-104.
[49]林惠民, 张文辉. 模型检测:理论、方法与应用. 电子学报, 2002, 30(增刊): 1907- 1913.
[50]古天龙. 软件开发的形式化方法. 北京:高等教育出版社, 2005: 141-142.
[51]Clarke E M, Grumberg JR O, Peled D A. Model Checking. Cambridge, Massachusetts: The MIT Press, 1999: 146-147.
[52]Millett L I, Teitelbaum T. Issues in slicing Promela and its application to model checking, protocol understanding, and simlation. International Journal on Software Tools for Technology Transfer, 2000, 2(4): 343-349.
[53]Hatcliff J, Dwyer M B, Zheng H. Slicing software for model construction. Higher- order and Symbolic Computation, 2000, 13(4): 315-353.
[54]Dwyer M B, Hatcliff J, Hoosier M, et al. Evaluating the effective of slicing for model reduction of concurrent object-oriented programs. LNCS 3920, Springer-Verlag, 2006: 73-89.
[55]董威, 王戟, 齐治昌. 并发程序的切片模型检验方法. 计算机学报, 2003, 26(3): 266-274.
[56]Wang J, Dong W, Qi Z. Slicing hierarchical automata for model checking UML statecharts. In Proceedings of the 4th International Conference on Formal Engineering Methods, 2002: 435-446.