Three-way merge tools play crucial roles in modern software development, where a developer forks a branch to make local modifications and requests it to be merged into the main branch via a "pull request." Despite its importance, the task has traditionally been defined in an intuitive manner, and the results of merge tools are often accepted without scrutiny. In this paper, we present a new structural merge tool in comparison with existing tools based on the syntactic criteria we propose for evaluating the merge results. We require the merge result to be both parsable and universal. Being parsable means that the result is syntactically valid according to the grammar of the programming language. Being universal means that the result incorporates all and only the edit operations occurring in each branch while ensuring that edits common to both branches are applied only once. This requirement can be precisely defined using the notion of pushouts in category theory. In a large-scale experiment involving 43,774 file merge scenarios from 76 open-source Java projects, we found a number of incorrect results reported by existing tools such as the Git companion merge tool, whereas our tool reports none. We further compared d3j’s results with 2,582 developer-resolved merges and with 2,459 merge scenarios involving 21 refactoring types. These experiments revealed both the strengths and current limitations of structural merge, and underscore the importance of clear correctness criteria. We expect that the proposed criterion will provide a foundation for developing more reliable and principled merge tools.

In this paper, we apply techniques from phylogenetics for uncovering evolutionary dependencies among software versions. Phylogenetics is a part of computational molecular biology that addresses the inference of evolution among organisms based on differences/similarities in DNA sequences and morphology. We apply a tree differencing technique to abstract syntax trees to calculate a distance matrix, which is then used by a distance-based phylogenetic algorithm to infer an evolution network. Such a network allows us to identify merging and branching among versions without manually looking into the details of the source code. Experiments on ancient versions of the Emacs editor and the open source 3D printer firmware show that we can reproduce the evolution of the software and identify code import/merging across different lineages. We also discuss how the techniques identify the feature models among software variations. To the best of our knowledge, this paper is the first to report on a reticulate phylogenetic analysis of the software. It may offer a helpful method for gaining information on the evolution of the software.

We present the design and fail-safety analysis of a sparsely synchronized N-modular redundant architecture for fail-safe computing that can be built on unreliable commercial off-the-shelf (COTS) components. Though the main intended audience is railway operators, the architecture is expected to be useful for general fail-safe computations. Traditional bus-synchronized fail-safe processors have had difficulty catching up with the performance and cost improvements of COTS processors because frequent involvement of the voter needed specialized design that slowed down computations. The proposed architecture alleviates this problem by comparing data much less frequently, only when the data leaves the fail-safe processor altogether. This allows the voter to be vastly simplified, becoming easy to harden against errors. We show empirically the use of COTS hardware barely affects the reliability of the overall architecture, making it as reliable as the simple voting circuitry, with acceptable runtime overhead.

This is an experience report on applying program analysis tools and program monitors to a real-world humanoid robot in simulated and real environments. Humanoid robots, and cyber-physical systems in general, present unique challenges to testing and validation: they have realtime constraints, their runs are typically irreproducible, their tasks are high-level and preclude formal specification, and their software tends to be large and complex. In practice, bugs do cause robots to fail, and methods for analyzing such software has been wanting. This paper presents a case study, in which we find that traditional software bugs like memory errors do cause failures of robots in practice. Dynamic error detectors can be successfully employed to identify such errors - to an extent defined by realtime constraints. Static analysis tools, in their current form, are comparatively of limited use.

Delta debugging (DD) is an approach to automating the debugging activities based on systematic testing. DD algorithms find the cause of a regression of a program by minimizing the changes applied between a working version and a faulty version of the program. However, it is still an open problem to minimize a huge set of changes while avoiding any invalid subsets that do not result in testable programs, especially in case that no software configuration management system is available. In this paper, we propose a rule-based approach to syntactic and semantic decomposition of changes into independent components to facilitate DD on source code changes, and hence to extract patches automatically. For analyzing changes, we make use of tree differencing on abstract syntax trees instead of common differencing on plain texts. We have developed an experimental implementation for Java programs and applied it to 194 bug fixes from Defects4J and 8 real-life regression bugs from 6 open source Java projects. Compared to a DD tool based on plain text differencing, it extracted patches whose size is reduced by 50% at the cost of 5% more test executions for the former dataset and by 73% at the cost of 40% more test executions for the latter, both on average.

Modbat makes testing easier by providing a user-friendly modeling language to describe the behavior of systems, from such a model, test cases are generated and executed. Modbat's domain-specific language is based on Scala, its features include probabilistic and non-deterministic transitions, component models with inheritance, and exceptions. We demonstrate the versatility of Modbat by finding a confirmed defect in the currently latest version of Java, and by testing SAT solvers.

This paper presents a comprehensive method for identifying fine-grained change patterns in the source code of large-scale software projects. Source code changes are computed by differencing abstract syntax trees of adjacent versions and transferred to a set of logical statements called a factbase. A factbase contains information for tracking and relating source code entities across versions and can be used to integrate analysis results of other tools such as call graphs and control flows. Users can obtain a list of change pattern instances by querying the factbase. Experiments conducted on the Linux-2.6 kernel, which involve more than 4 billions of facts, are reported to demonstrate capability of the method.

This article proposes a unified methodology for designing asynchronous SOA (Service-Oriented Architecture) based on the asynchronous messaging models and patterns. Conventional SOA focuses on synchronous messaging. Although asynchronous messaging provides much efficient and productive way to coordinate services, design of aSOA (asynchronous SOA) is far more complicated due to the variety of messaging and architecture while assuring behavioral consistency of architecture. This paper proposes a model-driven design methodology for aSOA. The methodology is based on aMEPs (Asynchronous Message Exchange Patterns) identified by classifying the messaging in terms of behavioral concerns. Based on the meta-model of aSOA, a set of aSOA patterns is generated by composing aMEPs. Then, an aSOA pattern is selected and transformed to a platform specific aSOA on top of Web services standards. We successfully implemented an aSOA on Apache Axis, which enables to asynchronous messaging of SOAP over SMTP. We demonstrated that conventional methods are subsets of the proposed methodology, which is the major contribution of this work.

We present a tool for analysis and detection of malicious mobile code such as computer viruses and internet worms based on the combined use of code simulation, static code analysis, and OS execution emulation. Unlike traditional anti-virus methods, the tool directly inspects the code and identifies commonly found malicious behaviors such as mass mailing, self duplication, and registry overwrite without relying on ``pattern files'' that contain ``signatures'' of previously captured samples. The prohibited behaviors are defined separately as security policies at the level of API library function calls in a state-transition like language. The tool also features data flow analysis based on static single assignment forms, which are useful in tracing various values stored in registers and memory locations. The current tool targets at Win32 binary programs on Intel IA32 architectures and can detect most email virusesslash worms that had spread in the wild in recent years.

This paper describes some tools to support formal methods, and conversely some formal methods for developing such tools. We focus on distributed cooperative proving over the web. Our tools include a proof editor/assistant, servers for remote proof execution, a distributed truth protocol, an editor generator; and a new method for interface design called algebraic semiotics, which combines semiotics with algebraic specification. Some examples are given.