用Z形式化描述程序切片

程序切片是一种重要技术,已广泛地应用于软件工程的各个领域,如程序理解、维护、调试、测试、复用、度量等.虽然,越来越多的研究者致力于程序切片工作,然而由于缺少形式化方面的工作导致程序切片可能存在不一致性和模糊性.本文尝试着用Z语言来形式化描述程序切片,考虑了程序切片中诸如程序依赖图和程序切片算法等常用的方面.该形式化描述不仅能帮助人们正确地理解程序切片的含义,而且还能够从比较严格的意义上明确程序切片的应用领域.     

Memory-efficient algorithms for the verification of temporal properties

This article addresses the problem of designing memory-efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are modeled as automata on infinite words (Büchi automata). Verification is then reduced to checking the emptiness of the automaton resulting from the product of the program and the property. This problem is usually solved by computing the strongly connected components of the graph representing the product automaton. Here, we present algorithms that solve the emptiness problem without explicitly constructing the strongly connected components of the product graph. By allowing the algorithms to err with some probability, we can implement them with a randomly accessed memory of size O(n) bits, where n is the number of states of the graph, instead of O(n log n) bits that the presently known algorithms require.     

一种C++程序切片系统的设计与实现

程序切片是一种程序分析技术,它主要应用在程序的调试和逆向工程。文中介绍了笔者设计并实现的一个C 程序切片系统。其中包括系统的总体框架,系统中使用的数据结构以及切片生成算法。本系统已经成功应用到了X型导弹指挥软件的故障诊断中。     

Slicing, Chopping, and Path Conditions with Barriers

One of the critiques on program slicing is that slices presented to the user are hard to understand. This is mainly related to the problem that slicing dumps the results onto the user without any explanation. This work will present an approach that can be used to filter slices. This approach basically introduces barriers which are not allowed to be passed during slice computation. An earlier filtering approach is chopping which is also extended to obey such a barrier. The barrier variants of slicing and chopping provide filtering possibilities for smaller slices and better comprehensibility. The concept of barriers is then applied to path conditions, which provide necessary conditions under which an influence between the source and target criterion exists. Barriers make those conditions more precise.     

Web Application Slicing in Presence of Dynamic Code Generation

The computation of program slices on Web applications may be useful during debugging, when the amount of code to be inspected can be reduced, and during understanding, since the search for a given functionality can be better focused. The system dependence graph is an appropriate data structure for slice computation, in that it explicitly represents all dependences that have to be taken into account in slice determination.Construction of the system dependence graph for Web applications is complicated by the presence of dynamically generated code. In fact, a Web application builds the HTML code to be transmitted to the browser at run time. Knowledge of such code is essential for slicing. In this paper an algorithm for the static approximation of the dynamically generated HTML code is proposed. The concatenations of constant strings and variables are propagated according to special purpose flow equations, allowing the estimation of the generated code and the refinement of the system dependence graph.     

软件的变量完整性测试方法

由于软件测试用例的输出部分很难确定,而通过测试变量自身的定义域和变量间的一致性约束关系,只需要确定输出值的范围而不用知道其确切的值,就可以提高了错误检测的效率．同时,检测的范围不局限于程序最后的输出结果,而是散布在程序中的各个有意义的变量,正如调试过程中设置断点观察的那些变量,使得检测错误更加精准．     

A stubborn attack on state explosion

This article presents theLTL-preserving stubborn set method for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear-time temporal logic specifications. The method facilitates the generation ofreduced state spaces such that the truth values of linear temporal logic formulas are the same in the ordinary and reduced state spaces. The only restrictions posed by the method are 1) the formulas must be known before the reduced state-space generation is commenced; 2) the use of the temporal operator next state is prohibited; and 3) the (reduced) state space of the system must be finite. The method cuts down the number of states by utilizing the fact that in concurrent systems the net result of the occurrence of two events is often independent of the order of occurrence.     

一种面向对象程序的过程间切片算法

程序切片是一种程序分析技术，它通过把程序减少到只包含与某个特定计算相关的那些语句来分析程序，过程间切片作为图形可达性问题时，需要扩展过程内切片所用的程序依赖图（PDG）成系统依赖图（SDG），然后利用两阶段图形可达性算法计算比较精确的切片，目前程序切片技术的研究以面向对象程序切片为主，文中讨论了一种合适面向对象程序的分层切片方法，并综合分层切片方法和两阶段图形可达性算法提出了一种简化的计算面向对象程序过程间切片的算法。     

并发程序的切片模型检验方法

提出了一种对并发程序进行切片以缩减模型检验状态空间的方法,首先针对并发程序中的同步与通信定义了一组依赖关系,包括并发分支与接合．非确定性,信道,共享变量等特征,对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准,文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片,可以证明得到的切片与原程序对于该性质具有相同的可满足性。     

A Model for Slicing JAVA Programs Hierarchically

Program slicing can be effectively used to debug, test, analyze, understand and maintain objectoriented software. In this paper, a new slicing model is proposed to slice Java programs based on their inherent hierarchical feature. The main idea of hierarchical slicing is to slice programs in a stepwise way, from package level, to class level, method level, and finally up to statement level. The stepwise slicing algorithm and the related graph reachability algorithms are presented, the architecture of the Java program Analyzing TOol (JATO) based on hierarchical slicing model is provided, the applications and a small case study are also discussed.     

程序切片技术在并发程序模型检查中的应用

模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则．并把得到的程序切片转化为验证所需的模型。经程序切片处理后,软件模型检查效率得到提高。     

并发程序切片原型系统的设计与实现

并发程序切片是并发程序分析的一种重要手段。针对多线程共享变量通信机制,在通过程序分析工具CodeSurfer获取程序基本信息的基础上构造程序可达图,生成以程序状态和语句二元组为节点的并发程序依赖图,实现了基于程序可达图的并发程序切片原型系统。初步实验结果表明,与传统的切片方法相比,采用基于程序可达图的并发程序切片方法,可有效地解决依赖关系不可传递问题,获得高精度的并发程序切片。     

基于程序切片技术的回归测试方法研究

软件测试是软件开发过程的一个重要组成部分，是进行软件有效性检查、提高软件质量的重要手段。随着软件规模的不断增大、复杂度的不断提高，传统的软件测试技术在处理大规模复杂软件系统时会出现许多问题。程序切片是一种程序分解术，主要是通过寻找程序内部的相关性来分解程序，从而达到快速错误定位或理解程序的目的。主要探讨将程序切片技术引入到软件测试中，尤其是分析在回归测试中切片方法是如何提高效率的。     

基于程序切片技术的回归测试方法研究

软件测试是软件开发过程的一个重要组成部分,是进行软件有效性检查、提高软件质量的重要手段。随着软件规模的不断增大、复杂度的不断提高,传统的软件测试技术在处理大规模复杂软件系统时会出现许多问题。程序切片是一种程序分解术,主要是通过寻找程序内部的相关性来分解程序,从而达到快速错误定位或理解程序的目的。主要探讨将程序切片技术引入到软件测试中,尤其是分析在回归测试中切片方法是如何提高效率的。     

一种用于软件测试的程序结构划分方法

软件测试中的结构性测试是以程序的结构为基础生成测试用例，以测试准则为判定测试的充分性，由于程序结构的复杂性，难于保证对程序进行充分而高效的测试，本文提出了一种基于程序依赖图的程序结构划分的测试方法，即程序块划分法。该方法难过对程序进行结构划分，将复杂的程序分解为若干程序块，并通过程序块间的数据依赖关系导出各程序块的语义，从而使测试可以在程序块的级别的基础上独立进行。     

一种改进的静态程序切片算法

提出了一种改进的静态程序切片算法,并应用到软件逆向工程中。在处理目标程序的过程间调用时,通过建立参数影射关系表,将过程间调用转换为过程内调用,简化了建立程序依赖图的复杂度;在归纳分析目标程序变量类型的基础上,给出了代数运算法则,对程序中的线性运算代码进行等价变换,缩减了切片程序的规模。最后通过具体的切片实例,证明了改进算法的有效性。     

Software Model Checking: The VeriSoft Approach

Verification by state-space exploration, also often referred to as model checking, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communication protocols). Unfortunately, traditional model checking is restricted to the verification of properties of models, i.e., abstractions, of concurrent systems.We discuss in this paper how model checking can be extended to analyze arbitrary software, such as implementations of communication protocols written in programming languages like C or C++. We then introduce a search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code.During the past five years, VeriSoft has been applied successfully for analyzing several software products developed in Lucent Technologies, and has also been licensed to hundreds of users in industry and academia. We discuss applications, strengths and limitations of VeriSoft, and compare it to other approaches to software model checking, analysis and testing.     

一种分析和理解程序的方法--程序切片

程序切片是一种分析和理解程序的技术,是通过对源程序中每个兴趣点分别计算切片来达到对程序的分析和理解。程序中某个兴趣点的程序切片不仅与该点定义和使用变量有关,而且与影响该变量的值的语名和谓词以及受该变量的值影响的语名的谓词有关。文中详细阐述了程序切片技术的研究与进展情况,并对目前存在各种程序切片方法和工具进行了比较;简单介绍了文中提出的面向对象的分层切片方法及其算法的思想;最后分析了程序切片技术目前     

一种JAVA程序静态切片的方法

JAVA语言是目前一种主要的面向对象编程语言,由于JAVA语言复杂的结构,使得对JAVA程序进行程序切片非常困难.本文提出一种层次的构造JAVA系统依赖图的算法,基于JAVA程序本身的层次结构,自顶向下构造系统依赖图,然后基于构造的系统依赖图,用一种改进的两阶段算法得到JAVA程序切片.