节点文献

面向对象并发程序切片技术及其在程序验证中的应用

Concurrent Object-oriented Program Slicing and Its Application in Program Verification

【作者】 何志学

【导师】 张广泉;

【作者基本信息】 苏州大学 , 计算机软件与理论, 2008, 硕士

【摘要】 程序切片是一种重要的程序分析技术,它通过提取程序中直接或间接影响某个特定程序点变量值的语句达到分解程序的目的。随着对程序切片技术研究的深入,其应用领域由软件调试、测试、软件维护扩展到逆向工程、再工程和程序验证等。面向对象技术仍是目前软件开发方法的主流,其中封装、继承、多态、并发等特征都为程序的理解与分析提出了新的问题。本文针对面向对象程序的并发机制,介绍了程序的图形化表示方法——面向对象并发系统依赖图,提出利用变量缓存表分析程序语句间依赖关系的方法,根据分析结果构造面向对象并发系统依赖图,并在此基础上采用改进的两步遍历图可达性算法计算动态切片。程序验证面临的主要问题是由于程序规模的增大,尤其是并发分量的增加,所带来的状态空间爆炸问题。程序切片可以将程序中不影响待验证性质的语句删除以减小针对该程序抽象出的模型的复杂性,从而缩减其对应的状态空间,在一定程度上缓解状态空间爆炸问题。本文提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法,切片后的程序与原程序关于待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。随着Internet技术和WWW技术的发展,Web应用涉及的范围越来越广,程序规模在不断扩大,其复杂性也越来越高。针对Java Web开发中关键技术的实现机制,把程序切片技术引入到Web应用程序的分析中,定义了Web应用程序中存在的依赖关系,提出了一种构造Web程序系统依赖图并计算程序切片的方法。在以上工作的基础上,本文以Java语言实现的典型并发程序为例对以上提出的方法在实际开发中的应用进行了说明、分析。

【Abstract】 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.

  • 【网络出版投稿人】 苏州大学
  • 【网络出版年期】2008年 11期
  • 【分类号】TP311.11
  • 【被引频次】4
  • 【下载频次】240
节点文献中: