Techniques and applications of computation slicing

Writing correct distributed programs is hard. In spite of extensive testing and debugging, software faults persist even in commercial grade software. Many distributed systems should be able to operate properly even in the presence of software faults. Monitoring the execution of a distributed system, and, on detecting a fault, initiating the appropriate corrective action is an important way to tolerate such faults. This gives rise to the predicate detection problem which requires finding whether there exists a consistent cut of a given computation that satisfies a given global predicate.Detecting a predicate in a computation is, however, an NP-complete problem in general. In order to ameliorate the associated combinatorial explosion problem, we introduce the notion of computation slice. Formally, the slice of a computation with respect to a predicate is a (sub)computation with the least number of consistent cuts that contains all consistent cuts of the computation satisfying the predicate. Intuitively, slice is a concise representation of those consistent cuts of a computation that satisfy a certain condition. To detect a predicate, rather than searching the state-space of the computation, it is much more efficient to search the state-space of the slice.We prove that the slice of a computation is uniquely defined for all predicates. We also present efficient algorithms for computing the slice for several useful classes of predicates. For an arbitrary predicate, we establish that the problem of computing the slice is NP-complete in general. Nonetheless, for such a predicate, we develop an efficient heuristic algorithm for computing an approximate slice. Our experimental results demonstrate that slicing can lead to an exponential improvement over existing techniques for predicate detection in terms of time and space.Received: 19 November 2003, Revised: 29 July 2004, Published online: 7 February 2005Vijay K. Garg: Supported in part by the NSF Grants ECS-9907213, CCR-9988225, Texas Education Board Grant ARP-320, an Engineering Foundation Fellowship, and an IBM grant.Parts of this paper have appeared earlier in conference proceedings [GM01,MG01a,MG03a].     

The effect of uncontrolled concurrency on model checking

Correctness of concurrent software is usually checked by techniques such as peer code reviews or code walkthroughs and testing. These techniques, however, are subject to human error, and thus do not achieve an in‐depth verification of correctness. Model‐checking techniques, which can systematically identify and verify every state that a system can enter, are a powerful alternative method for verifying concurrent systems. However, the usefulness of model checking is limited because the number of states for concurrent models grows exponentially with the number of processes in the system. This is often referred to as the ‘state explosion problem.’ Some processes are a central part of the software operation and must be included in the model. However, we have found that some exponential complexity results due to uncontrolled concurrency introduced by the programmer rather than due to the intrinsic characteristics of the software being modeled. We have performed tests on multimedia synchronization to show the effect of abstraction as well as uncontrolled concurrency using the Promela/SPIN model checker. We begin with a sequential model not expected to have exponential complexity but that results in exponential complexity. In this paper, we provide alternative designs and explain how uncontrolled concurrency can be removed from the code. Copyright © 2007 John Wiley & Sons, Ltd.     

Solving Computation Slicing Using Predicate Detection

Given a distributed computation and a global predicate, predicate detection involves determining whether there exists at least one consistent cut (or global state) of the computation that satisfies the predicate. On the other hand, computation slicing is concerned with computing the smallest subcomputation (with the least number of consistent cuts) that contains all consistent cuts of the computation satisfying the predicate. In this paper, we investigate the relationship between predicate detection and computation slicing and show that the two problems are actually equivalent. Specifically, given an algorithm to detect a predicate b in a computation C, we derive an algorithm to compute the slice of C with respect to b. The time complexity of the (derived) slicing algorithm is O(n|E|T), where n is the number of processes, E is the set of events, and O(T) is the time complexity of the detection algorithm. We discuss how the "equivalence" result of this paper can be utilized to derive a faster algorithm for solving the general predicate detection problem in many cases. Slicing algorithms described in our earlier papers are all offline in nature. In this paper, we also present two online algorithms for computing the slice. The first algorithm can be used to compute the slice for a general predicate. Its amortized time complexity is O(n(c + n)T) per event, where c is the average concurrency in the computation and O(T) is the time complexity of the detection algorithm. The second algorithm can be used to compute the slice for a regular predicate. Its amortized time complexity is only O(n²) per event.     

Data decision diagrams for Promela systems analysis

In this paper, we show how to verify computation tree logic (CTL) properties, using symbolic methods, on systems described in Promela. Symbolic representation is based on data decision diagrams (DDDs) which are n-valued Shared Decision Trees designed to represent dynamic systems with integer domain variables. We describe principal components used for the verification of Promela systems (DDD, representation of Promela programs with DDD, the transposition of the execution of Promela instructions into DDD). Then we compare and contrast our method with the model checker SPIN or classical binary decision diagram (BDD) techniques to highlight as to which system classes SPIN or our tool is more relevant.     

Partial Order Reduction for Probabilistic Branching Time

In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper presents partial order reduction criteria for Markov decision processes and branching time properties, such as formulas of probabilistic computation tree logic. Moreover, we provide a comparison of the results established so far about reduction conditions for Markov decision processes.     

The Design of a Multicore Extension of the SPIN Model Checker

We describe an extension of the SPIN model checker for use on multicore shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can, in some cases, be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multicore algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code and are compatible with most existing verification modes such as partial order reduction, the verification of temporal logic formulas, bitstate hashing, and hash-compact compression.     

一种基于LTL性质的面向对象并发程序切片方法

为了缩减程序验证的状态空间,针对面向对象程序的并发机制,定义了程序中存在的依赖关系,提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法。切片后的程序与原程序对待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。     

Temporal Semantics for Concurrent M M

Concurrent is a programming language based on the notion of concurrent, communicating objects, where each object directly executes a specification given in temporal logic, and communicates with other objects using asynchronous broadcast message-passing. Thus, Concurrent represents a combination of the direct execution of temporal specifications, together with a novel model of concurrent computation. In contrast to the notions of predicates as processes and stream parallelism seen in concurrent logic languages, Concurrent represents a more coarse-grained approach, where an object consists of a set of logical rules and communication is achieved by the evaluation of certain types of predicate. Representing concurrent systems as groups of such objects provides a powerful tool for modelling complex reactive systems. In order to reason about the behaviour of Concurrent systems, we requir a suitable semantics. Being based upon executable temporal logic, objects in isolation have an intuitive semantics. However, the addition of both operational constraints upon the object's execution and global constraints provided by the asynchronous model of concurrency and communication, complicates the overall semantics of networks of objects. It is this, more complex, semantics that we address here, where temporal semantics for varieties of Concurrent are provided.     

Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths — the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem.     

Granularity-Driven Dynamic Predicate Slicing Algorithms for Message Passing Systems

Program Slicing is a well-known decomposition technique that transforms a large program into a smaller one that contains only statements relevant to the computation of a selected function. In this paper, we present two novel predicate-based dynamic slicing algorithms for message passing programs. Unlike more traditional slicing criteria that focus only on parts of the program that influence a variable of interest at a specific position in the program, a predicate focuses on those parts of the program that influence the predicate. The dynamic predicate slices capture some global requirements or suspected error properties of a distributed program and computes all statements that are relevant. The presented algorithms differ from each other in their computational approaches (forward versus backward) and in the granularity of information they provide. A proof of correctness of these algorithms is provided. Through the introduction of dominant states and dominant events, critical statement executions are identified that change the value of the global predicate. Under this formulation, optimizing dynamic predicate slicing becomes a meaningful goal as well. Finally, we present how predicate slices can be applied to support comprehension tasks for analyzing and maintaining distributed programs.     

Techniques to tackle state explosion in global predicate detection

Global predicate detection, which is an important problem in testing and debugging distributed programs, is very hard due to the combinatorial explosion of the global state space. The paper presents several techniques to tackle the state explosion problem in detecting whether an arbitrary predicate Φ is true at some consistent global state of a distributed system. We present space efficient online algorithms for detecting Φ. We then improve the performance of our algorithms, both in space and time, by increasing the granularity of the execution step from an event to a sequence of events in each process     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

一种C程序断言的全自动静态验证方法

在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足，从而使得验证过程可以终止。实验表明，提出的全自动静态断言验证方法不仅可行，而且验证代价较小，具有较强的实用性。     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

Using SPIN for automated debugging of infinite executions of Java programs

This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking and runtime monitoring. Runtime monitoring is used to transform the Java execution traces into the input for the model checker, the purpose of which is twofold. First, it checks these execution traces against properties written in linear temporal logic (LTL), which represent desirable or undesirable behaviors. Second, it produces several execution traces for a single Java program by generating test inputs and exploring different schedulings in multithreaded programs. As state explosion is the main drawback to model checking, we propose two abstraction approaches to reduce the memory requirements when storing Java states. We also present the formal framework to clarify which kinds of LTL safety and liveness formulas can be correctly analysed with each abstraction for both finite and infinite program executions. A major advantage of our approach comes from the model checker, which stores the trace of each failed execution, allowing the programmer to replay these executions to locate the bugs. Our current implementation, the tool TJT, uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as an Eclipse plug-in and it has been successfully applied to debug complex public Java programs.     

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

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

基于插桩和布尔逻辑的运行时程序验证框架

针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题,提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA。定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL,实现自动化插桩以收集运行时程序状态信息,设计一个支持高效验证的句子调度算法。实验结果表明,结合合适的谓词扩展,RPA可以有效地验证和分析软件逻辑,发现潜在的软件错误。     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes

Mechanical tools have recently been developed that enable computer-aided verification of spatial properties of concurrent systems. To be practical, these tools are expected to deal with the state- space explosion problem. In order to alleviate this problem, we develop partial order reduction for verification of spatial properties of pi-calculus processes. The main issue is that spatial logics are very expressive and some spatial formulas prevent partial order reduction. After discussing this issue, we propose a restricted spatial logic such that partial order reduction holds. Our approach relies on exploiting partially confluent communications and on identifying invisible communications in the pi-calculus, for which we propose a simple syntactic criterion.     

Interpreting Message Flow Graphs

We give a semantics for Message Flow Graphs (MFGs), which play the role for interprocess communication that Program Dependence Graphs play for control flow in parallel processes. MFGs have been used to analyse parallel code, and are closely related to Message Sequence Charts and Time Sequence Diagrams in telecommunications systems. Our requirements are firstly, to determine unambiguously exactly what execution traces are specified by an MFG, and secondly, to use a finite-state interpretation. Our methods function for both asynchronous and synchronous communications. From a set of MFGs, we define a transition system of global states, and from that a Büchi automaton by considering safety and liveness properties of the system. In order easily to describe liveness properties, we interpret the traces of the transition system as a model of Manna-Pnueli temporal logic. Finally, we describe the expressive power of MFGs by mimicking an arbitrary Büchi automaton by means of a set of MFGs.