A C++ data model supporting reachability analysis and dead codedetection

A software repository provides a central information source for understanding and reengineering code in a software project. Complex reverse engineering tools can be built by analyzing information stored in the repository without reparsing the original source code. The most critical design aspect of a repository is its data model, which directly affects how effectively the repository supports various analysis tasks. This paper focuses on the design rationales behind a data model for a C++ software repository that supports reachability analysis and dead code detection at the declaration level. These two tasks are frequently needed in large software projects to help remove excess software baggage, select regression tests and support software reuse studies. The language complexity introduced by class inheritance, friendship, and template instantiation in C++ requires a carefully designed model to catch all necessary dependencies for correct reachability analysis. We examine the major design decisions and their consequences in our model and illustrate how future software repositories can be evaluated for completeness at a selected abstraction level. Examples are given to illustrate how our model also supports variants of reachability analysis: impact analysis, class visibility analysis, and dead code detection. Finally, we discuss the implementation and experience of our analysis tools on a few C++ software projects     

Straight line reachability of Roesser model

A new definition of straight line reachability for the Roesser model is presented. Necessary and sufficient conditions for straight line teachability of the Roesser model are established. A relationship between local reachability and straight line reachability of the Roesser model is discussed.     

Competent predicate abstraction in model checking

The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counterexample-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the app...     

A generalized deadlock predicate

Satisfiability of the deadlock predicate constructed by the semaphore invariant method is a necessary condition for total deadlock in PV programs. Clarke (1980) has developed a technique, based on a view of resource invariants as fixed points of a functional, for constructing a deadlock predicate such that satisfiability is a necessary and sufficient condition for total deadlock. We describe a technique for synthesizing a generalized deadlock predicate such that satisfiability is a necessary and sufficient condition for both total and partial deadlock. Our method constructs a strongest resource invariant using Clarke's fixed point functional. We then use this strongest resource invariant and a predicate transformer to construct a generalized deadlock predicate.     

Combining predicate and numeric abstraction for software model checking

Predicate (PA) and numeric (NA) abstractions are the two principal techniques for software analysis. In this paper, we develop an approach to couple the two techniques tightly into a unified framework via a single abstract domain called NumPredDom. In particular, we develop and evaluate four data structures that implement NumPredDom but differ in their expressivity and internal representation and algorithms. All our data structures combine BDDs (for efficient propositional reasoning) with data structures for representing numerical constraints. Our technique is distinguished by its support for complex transfer functions that allow two-way interaction between predicate and numeric information during state transformation. We have implemented a general framework for reachability analysis of C programs on top of our four data structures. Our experiments on non-trivial examples show that our proposed combination of PA and NA is more powerful and more efficient than either technique alone.     

B model slicing and predicate abstraction to generate tests

In a model-based testing approach as well as for the verification of properties, B models provide an interesting modeling solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used. The abstraction is often a domain abstraction of the state variables that requires many proof obligations to be discharged, which can be very time-consuming for real applications. This paper presents a contribution to this problem that complements an approach based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a B event model, in addition to three methods that choose relevant variables according to a test purpose. In this way, we propose a method that computes an abstraction of a source model ${\mathsf{M}}$ according to a set of selected relevant variables. Depending on the method used, the abstraction can be computed as a simulation or as a bisimulation of ${\mathsf{M}}$ . With this approach, the abstraction process produces a finite state system. We apply this abstraction computation to a model-based testing process. We evaluate experimentally the impact of the model simplification by variables' elimination on the size of the models, on the number of proof obligations to discharge, on the precision of the abstraction and on the coverage achieved by the test generation.     

A dynamic associative memory system by adopting an amygdala model

Although several kinds of computational associative memory models and emotion models have been proposed since the last century, the interaction between memory and emotion is almost always neglected in these conventional models. This study constructs a dynamic memory system, named the amygdala-hippocampus model, which intends to realize dynamic auto-association and the mutual association of time-series patterns more naturally by adopting an emotional factor, i.e., the functional model of the amygdala given by Morén and Balkenius. The output of the amygdala is designed to control the recollection state of multiple chaotic neural networks (MCNN) in CA3 of the hippocampus-neocortex model proposed in our early work. The efficiency of the proposed association system is verified by computer simulation using several benchmark time-series patterns. This work was presented in part at the 13th International Symposium on Artificial Life and Robotics, Oita, Japan, January 31–February 2, 2008     

Efficient reduction of finite state model checking to reachability analysis

Two types of temporal properties are usually distinguished: safety and liveness. Recently we have shown how to verify liveness properties of finite state systems using safety checking. In this article we extend the translation scheme to typical combinations of temporal operators. We discuss optimizations that limit the overhead of our translation. Using the notions of predicated diameter and radius we obtain revised bounds for our translation scheme. These notions also give a tight bound on the minimal completeness bound for simple liveness properties. Experimental results show the feasibility of the approach for complex examples. For one example, even an exponential speedup can be observed.     

A predicate spatial logic for mobile processes

A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.     

A work-efficient distributed algorithm for reachability analysis

This work presents a novel distributed symbolic algorithm for reachability analysis that can effectively exploit, as needed, a large number of machines working in parallel. The novelty of the algorithm is in its dynamic allocation and reallocation of processes to tasks and in its mechanism for recovery from local state explosion. As a result, the algorithm is work-efficient: it utilizes only those resources that are actually needed. In addition, its high adaptability makes it suitable for exploiting the resources of very large and heterogeneous distributed, nondedicated environments. Thus, it suitable for verifying very large systems. We implemented our algorithm in a tool called Division. Our experimental results show that the algorithm is indeed work-efficient. Although the goal of this research is to check larger models, the results also indicate that the algorithm can obtain high speedups, because communication overhead is very small.     

A columnar model explaining long-term memory

A hologram provides a useful model for explaining the associative memory of the brain. Recent advances in neuroscience emphasize that single neurons can store complex information and that subtle changes in neurons underlie the process of memorization. Experimental results suggest that memory has a localized character. This finding is inconsistent with the characteristics of holographic memory, because this memory has a delocalized, uniform distribution of refractive index in the recorded medium. The recently proposed columnar memory model has a discrete distribution of refractive index. In this study, we first examined the performance of columnar memory and found that it was comparable to holographic memory. Secondly, we showed that this model could explain the above-mentioned experimental results as well as associative memory.     

A new neural associative memory model

We present a new associative memory model based on the Hamming memory, but where the winner-take-all network part is replaced by a layer of nodes with somewhat complex node functions. This new memory can produce output vectors with individual “don't know” bits. the simulations demonstrate that this memory model works appropriately. © 1992 John Wiley & Sons, Inc.     

A low-level resource allocation in an agent-based Cloud Computing platform

The distribution of computational resources in a Cloud Computing platform is a complex process with several parameters to consider such as the demand for services, available computational resources and service level agreements with end users. Currently, the state-of-the-art presents centralized approaches derived from previous technologies related to cluster of servers. These approaches allocate computational resources by means of the addition/removal of (physical/virtual) computational nodes. However, virtualization technology currently allows for research into new techniques, which makes it possible to allocate at a lower level. In other words, not only is it possible to add/remove nodes, but also to modify the resources of each virtual machine (low level resource allocation). Thus, agent theory is a key technology in this field, allowing decentralized resource allocation. This innovative approach has undeniable improvements such us computational load distribution and reduced computation time. The evaluation was carried out through experiments in a real Cloud environment, thus proving the validity of the proposed approach.     

A specification technique based on predicate transformers

Summary This paper proposes a formal specification technique based on the notion of predicate transformers. Several approaches to showing the completeness are investigated. A method for proving the correctness of an implementation with respect to a formal specification is described.The work presented in this paper was performed while the author was with the University of Hamburg, Germany     

A competitive associative memory model and its dynamics

Conventional associative memory networks perform "noncompetitive recognition" or "competitive recognition in distance". In this paper a "competitive recognition" associative memory model is introduced which simulates the competitive persistence of biological species. Unlike most of the conventional networks, the proposed model takes only the prototype patterns as its equilibrium points, so that the spurious points are effectively excluded. Furthermore, it is shown that, as the competitive parameters vary, the network has a unique stable equilibrium point corresponding to the winner competitive parameter and, in this case, the unique stable equilibrium state can be recalled from any initial key.     

Robot reachability problem: A nonlinear optimization approach

The reachability of a robot manipulator to a target is defined as its ability to move its joints and links in free space in order for its hand to reach the given target. This paper presents a way of testing the reachability of a robot to given target. The target could be a three dimensional object represented by a cuboid, a line or merely a point.The reachability test problem is transformed into a nonlinear optimization problem, which is solved by using the Tunneling Algorithm [1–3].The paradigm of the Tunneling Algorithm is described in detail. Several examples of testing the reachability of two robots to given targets are presented and the results are compared with that of the existing RGRG algorithm [5]. The results of comparisons show that the Tunneling Algorithm is better than the RGRG algorithm. It can always obtain the correct answers of testing, and it is effective and suitable to solve the reachability test problem.This project is partially supported by a grant from Martin Marietta (ORNL) 19x-55902V. Also this project is partially funded by ONR grant N00014-94-1-0343.