Tool Demos

When a software system evolves, its program entities such as classes/methods are also changed. System comprehension, maintenance, and other tasks require the detection of the changed entities between two versions. However, existing differencing tools are file-based and cannot handle well the common cases in which the methods/classes are reordered/moved or even renamed/modified. Moreover, many tools show the program changes at the text line level. In this demo, we present iDiff, a program differencing tool that is able to display the changes to classes/methods between two versions and to track the corresponding classes/methods even they were reordered/moved/renamed and/or modified. The key idea is that during software evolution, an entity could change its location, name, order, and even its internal implementation. However, its interaction with other entities would be more stable. iDiff represents a system at a version as an attributed graph, in which the nodes represent program entities, the edges represent the interactions between the nodes. Entities between two versions are matched via an incremental matching algorithm, which takes into account the similarity of interactions for matching. The differences of two versions of the entire system including its program entities are detected based on the matched entities.

Clone detection provides a scalable and efficient way to detect similar code fragments. But it offers limited explanation of differences of functions performed by clones and variations of control and data flows of clones. We refer to such differences as semantic differences of clones. Understanding these semantic differences is essential to correctly interpret cloning information and perform maintenance tasks on clones. Manual analysis of semantic differences of clones is complicated and error-prone. In the paper, we present our clone analysis tool, called Clone-Differentiator. Our tool automatically characterizes clones returned by a clone detector by differentiating Program Dependence Graphs (PDGs) of clones. CloneDifferentiator is able to provide a precise characterization of semantic differences of clones. It can provide an effective means of analyzing clones in a task oriented manner.

Model-driven development tools built on industry standard platforms, such as the Eclipse Modeling Framework (EMF), heavily use model queries in various use cases, such as model transformation, well-formedness constraint validation and domain-specific model execution. As these queries are executed rather frequently in interactive modeling applications, they have a significant impact on the runtime performance of the tool, and also on the end user experience. However, due to their complexity, they can be time consuming to implement and optimize on a case-by-case basis. To address these shortcomings, we developed the EMF-IncQuery framework for defining declarative queries over EMF models and executing them effectively using a caching mechanism.

In the current paper, we demonstrate how our framework can be easily integrated with other EMF tools. We describe a case study in which EMF-IncQuery is integrated into the open source Papyrus UML environment to provide on-the-fly validation of well-formedness criteria in UML models.

Verification of Graphical User Interface (GUI) applications presents many challenges. GUI applications are open systems that are driven by user events. Verification of such applications by means of model checking therefore requires a user model in order to close the state space. In addition, GUIs rely extensively on complex and inherently concurrent framework libraries such as AWT/Swing, for which the application code merely provides callbacks. Software model checking of GUI applications therefore needs abstractions of such frameworks that faithfully preserve application behavior. This paper presents JPF-AWT, an extension of the Java PathFinder software model checker, which addresses these challenges. JPF-AWT has been successfully applied to a GUI front end of a NASA ground data system.

Pointers are a powerful and widely used programming mechanism, but developing and maintaining correct pointer programs is notoriously hard. Here we describe the CORE system, which supports the development of provably correct pointer programs. The CORE system combines data structure animation with functional correctness. While the animation component allows a programmer to explore and debug their algorithms, the functional correctness component provides a stronger guarantee via formal proof. CORE builds upon two external reasoning tools, i.e. the Smallfoot family of static analysers and the IsaPlanner proof planner. At the heart of the CORE functional correctness capability lies an integration of planning and term synthesis. The planning subsystem bridges the gap between shape analysis, provided by Smallfoot, and functional correctness. Key to this process is the generation of functional invariants, i.e. both loop and frame invariants. We use term synthesis, coupled with IsaPlanner’s capability for reasoning about inductively defined structures, to automate the generation of functional invariants. The formal guarantees constructed by the CORE system take the form of proof tactics.

Programmers often learn how to use an API by studying its usage examples. There are many usage examples scattered in web pages on the Internet. However, it often takes programmers much effort to find out the desired examples from a large number of web pages by web search. This paper proposes a tool named APIExample that can extract usage examples for java APIs from web pages on the Internet and recommend them to programmers. Given a java API, the tool collects its related web pages from the Internet, extracts java code snippets and their surrounding descriptive texts embedded in the pages, then assembles them into usage examples for programmers. Furthermore, in order to help programmers capture more kinds of usages of the target API by browsing fewer examples, our tool clusters and ranks the listed examples based on the target API’s usage. Besides, as a practical tool, APIExample provides multiple aspects of frequently-used information about using the target API in a concise user interface with friendly user experience. Two kinds of user-interaction style, a web search portal and an Eclipse plug-in, are now both publicly available.

We present a tool BEST (Binary instrumentation-based Error-directed Symbolic Testing) for predicting concurrency violations. We automatically infer potential concurrency violations such as atomicity violations from an observed run of a multi-threaded program, and use precise modeling and constraint-based symbolic (non-enumerative) search to find feasible violating schedules in a generalization of the observed run. We specifically focus on tool scalability by devising POR-based simplification steps to reduce the formula and the search space by several orders-of-magnitude. We have successfully applied the tool to several publicly available C/C++/Java programs and found several previously known/unknown concurrency related bugs. The tool also has extensive visual support for debugging.

Variability in software product lines is often expressed through feature models (FMs). To handle the complexity of increasingly larger FMs, we propose semantically meaningful decomposition support through a slicing operator. We describe how the slicing operator is integrated into the FAMILIAR environment and how it can be combined with other operators to support complex tasks over FMs in different case studies.

Model Driven Development (MDD) is an approach to software development built around the notion of models. One of its implementation is the IBM RSA RTE, which uses the UML-RT modeling language. In this paper we introduce the tool SAUML (Symbolic Analysis of UML-RT Models) that enhances the current practice of MDD with the analyses of UML-RT models. The implemented technique is based on symbolic execution, features modularity and supports the reuse of analysis results. The paper gives an overview of this technique and its implementation in the IBM RSA RTE tool.

This tool paper presents an embodiment of TestEra – a framework developed in previous work for specification-based testing of Java programs. To test a Java method, TestEra uses the method’s pre-condition specification to generate test inputs and the post-condition to check correctness of outputs. TestEra supports specifications written in Alloy – a first-order, declarative language based on relations – and uses the SAT-based back-end of the Alloy tool-set for systematic generation of test suites. Each test case is a JUnit test method, which performs three key steps: (1) initialization of pre-state, i.e., creation of inputs to the method under test; (2) invocation of the method; and (3) checking the correctness of post-state, i.e., checking the method output. The tool supports visualization of inputs and outputs as object graphs for graphical illustration of method behavior. TestEra is available for download to be used as a library or as an Eclipse plug-in.

Mutation analysis is an effective, yet often time-consuming and difficult-to-use method for the evaluation of testing strategies. In response to these and other challenges, this paper presents MAJOR, a fault seeding and mutation analysis tool that is integrated into the Java Standard Edition compiler as a non-invasive enhancement for use in any Java-based development environment. MAJOR reduces the mutant generation time and enables efficient mutation analysis. It has already been successfully applied to large applications with up to 373,000 lines of code and 406,000 mutants. Moreover, MAJOR's domain specific language for specifying and adapting mutation operators also makes it extensible. Due to its ease-of-use, efficiency, and extensibility, MAJOR is an ideal platform for the study and application of mutation analysis.

We are concerned with analyzing software, in particular, with its nature and how developer decisions and behavior impact the quality of the product they produce. This is the domain of empirical software engineering where measurement seeks to capture attributes affecting the product, process, and resources of software development. A well-established means to study software attributes is metrics data mining. But, even though a variety of frameworks have emerged that can distill desired measures from software systems (e.g., JHawk or SonarJ), a systematic approach to collecting measures from large data sets has still eluded us. For this reason, we have developed the Java Code Tomograph (jCT), a novel framework for metrics extraction and processing. jCT offers an extensible measurement infrastructure with built-in support for the curated repositories Qualitas Corpus and Helix. With jCT, large-scale empirical studies of code within the same software system or across different software systems become feasible. In this paper, we provide an overview of jCT's main design features and discuss its operation in relation to the effectiveness of the framework.

Test models are needed to evaluate and benchmark algorithms and tools in model driven development. Most model generators randomly apply graph operations on graph representations of models. This approach leads to test models of poor quality. Some approaches do not guarantee the basic syntactic correctness of the created models. Even if so, it is almost impossible to guarantee, or even control, the creation of complex structures, e.g. a subgraph which implements an association between two classes. Such a subgraph consists of an association node, two association end nodes, and several edges, and is normally created by one user command. This paper presents the SiDiff Model Generator, which can generate models, or sets of models, which are syntactically correct, contain complex structures, and exhibit defined statistical characteristics.

This paper describes a tool to help debug error traces found by the Java Pathfinder model checker in concurrent Java programs. It does this by abstracting out thread interactions and program locations that are not obviously pertinent to the error through control flow or data dependence. The tool then iteratively refines the abstraction by adding thread interactions at critical locations until the error is reachable. The tool visualizes the entire process and enables the user to systematically analyze each abstraction and execution. Such an approach explicitly identifies specific context switch locations and thread interactions needed to debug a concurrent error trace in small to moderate programs that can be managed by the Java Pathfinder Tool.

Distributed embedded systems, such as multi-player smartphone games, training instrumentation systems, and "smart" homes, naturally have complex requirements. These are difficult to elicit, represent, validate, and verify. For high confidence, one demands that the represented requirements reflect realistic uses of the system; however, such uses, often representing human actions in complex environments, can have hundreds to thousands of steps and be impractical to elicit and manage using only declarative or intensional (computed) representations. Non-functional requirements like scalability increase this complexity further. In this paper, I show how one can bootstrap requirements using data captured from initial prototypes deployed in small scale real world tests. Using such *captures* as seeds, I show how a calculus of transformations on captures, from captures to scenarios, among scenarios, and from scenarios back to captures can be used in several requirements engineering tasks. I describe a novel ecosystem of tools and transformations that implement this capture calculus and illustrate its use on data obtained from the domain of multi-player outdoor smartphone games.

BDD-based symbolic model checking is capable of verifying systems with a large number of states. In this work, we report an extensible framework to facilitate symbolic encoding and checking of hierarchical systems. Firstly, a novel library of symbolic encoding functions for compositional operators (e.g., parallel composition, sequential composition, choice operator, etc.) are developed so that users can apply symbolic model checking techniques to hierarchical systems with little low-level knowledge (like BDD or CUDD). Secondly, as the library is language-independent, we build a framework (with a modular design) so that the library can be easily applied to encode and verify different modeling languages. Lastly, the applicability and scalability of our framework are demonstrated by applying the framework in the development of symbolic model checkers for three modeling languages as well as a comparison with the NuSMV model checker.