In continuous integration development environments, software engineers frequently integrate new or changed code with the mainline codebase. This can reduce the amount of code rework that is needed as systems evolve and speed up development time. While continuous integration processes traditionally require that extensive testing be performed following the actual submission of code to the codebase, it is also important to ensure that enough testing is performed prior to code submission to avoid breaking builds and delaying the fast feedback that makes continuous integration desirable. In this work, we present algorithms that make continuous integration processes more cost-effective. In an initial pre-submit phase of testing, developers specify modules to be tested, and we use regression test selection techniques to select a subset of the test suites for those modules that render that phase more cost-effective. In a subsequent post-submit phase of testing, where dependent modules as well as changed modules are tested, we use test case prioritization techniques to ensure that failures are reported more quickly. In both cases, the techniques we utilize are novel, involving algorithms that are relatively inexpensive and do not rely on code coverage information -- two requirements for conducting testing cost-effectively in this context. To evaluate our approach, we conducted an empirical study on a large data set from Google that we make publicly available. The results of our study show that our selection and prioritization techniques can each lead to cost-effectiveness improvements in the continuous integration process.

Software Engineers are horrible customers for software tools. If they don't like your tools, they will just write their own. If your tool wastes a few minutes of a developer's day, good luck getting them to ever try your tool again. And if, after years of effort, you manage to develop tools they actually like, you are really in trouble. This is when they start building systems on top of your tools. No API? No problem! They will hack and scrape as needed to get their job done. In this talk I'll go through a number of examples of successes, non-successes and over-successes from the past 8 years of evolving the developer infrastructure at Google. I'll highlight the challenges we faced, our attempts to address the challenges and share our lessons learned.

Software Engineering in practice deals with scale in a variety of dimensions. We build large scale systems operating on vast amount of data. We have millions of customers with billions of queries and transactions. We have distributed teams making thousands of changes, running millions of tests and releasing multiple times per day. These dimensions of scale interact to provide challenges for software development tools and processes. The panelists will describe the challenging aspects of scale in their specific problem domains and discuss which software engineering methods work and which leave room for improvement.

Software development at Google is big and fast. The code base receives 20+ code changes per minute and 50% of the files change every month! Each product is developed and released from head relying on automated tests verifying the product behavior. Release frequency varies from multiple times per day to once every few weeks, depending on the product team. With such a huge, fast-moving codebase, it is possible for teams to get stuck spending a lot of time just keeping their build green. A continuous integration system should help by providing the exact change at which a test started failing, instead of a range of suspect changes or doing a lengthy binary-search for the offending change. We have built a system that uses dependency analysis to determine all the tests a change transitively affects and then runs only those tests for every change. The system is built on top of Googles cloud computing infrastructure enabling many builds to be executed concurrently, allowing the system to run affected tests as soon as a change is submitted. The use of smart tools and cloud computing infrastructure in the continuous integration system enables quick, effective feedback to development teams.

Static analysis tools report software defects that may or may not be detected by other verification methods. Two challenges complicating the adoption of these tools are spurious false positive warnings and legitimate warnings that are not acted on. This paper reports automated support to help address these challenges using logistic regression models that predict the foregoing types of warnings from signals in the warnings and implicated code. Because examining many potential signaling factors in large software development settings can be expensive, we use a screening methodology to quickly discard factors with low predictive power and cost-effectively build predictive models. Our empirical evaluation indicates that these models can achieve high accuracy in predicting accurate and actionable static analysis warnings, and suggests that the models are competitive with alternative models built without screening.

Static analysis tools for software defect detection are becoming widely used in practice. However, there is little public information regarding the experimental evaluation of the accuracy and value of the warnings these tools report. In this paper, we discuss the warnings found by FindBugs, a static analysis tool that finds defects in Java programs. We discuss the kinds of warnings generated and the classification of warnings into false positives, trivial bugs and serious bugs. We also provide some insight into why static analysis tools often detect true but trivial bugs, and some information about defect warnings across the development lifetime of software release. We report data on the defect warnings in Sun's Java 6 JRE, in Sun's Glassfish JEE server, and in portions of Google's Java codebase. Finally, we report on some experiences from incorporating static analysis into the software development process at Google.

Completed design and implementation are often regarded as prerequisites of any verification. While recent development methods establish testability as a design criterion, there is no corresponding design support for other verification methods like model checking and static analysis. Since these methods have inherent scalability problems, their application becomes more difficult where it is most needed - for complex systems. Our design-for-verification (D4V) approach attempts to close this gap using a variety of techniques, such as design patterns, APIs and source annotations. This paper presents a overview of D4V, and introduces dynamic assertions as one of the proposed D4V techniques. Dynamic assertions are dedicated, non-intrusive check objects that are dynamically activated, evaluated and deactivated via assertions of their target objects. Since these check objects can have their own state, they can be used to verify a broad range of properties. Properties can be expressed in the target programming language, and checked in a testing environment. In addition, dynamic assertions can be configured via call contexts, making them suitable for connector-specific verification of component based systems

Previous work on domain-specific deductive program synthesis described the Amphion/NAIF system for generating Fortran code from high-level graphical specifications describing problems in space system geometry. Amphion/NAIF specifications describe input-output functions that compute geometric quantities (e.g., the distance between two planets at a point in time, or the time when a radio communication path between a spacecraft and earth is occluded) by composing together Fortran subroutines from the NAIF subroutine library developed at the Jet Propulsion Laboratory. In essence, Amphion/NAIF synthesizes code for glueing together the NAIF components in a way such that the generated code implements the specification, with a concurrently generated proof that this implementation is correct. Amphion/NAIF demonstrated the success of domain-specific deductive program synthesis and is still in use today within the space science community. However, a number of questions remained open that we will attempt to answer in this paper.

The paper documents an application of the finite state model checker SPIN to formally analyze a multithreaded plan execution module. The plan execution module is one component of NASA's New Millennium Remote Agent, an artificial intelligence-based spacecraft control system architecture which launched in October of 1998 as part of the DEEP SPACE 1 mission. The bottom layer of the plan execution module architecture is a domain specific language, named ESL (Executive Support Language), implemented as an extension to multithreaded COMMON LISP. ESL supports the construction of reactive control mechanisms for autonomous robots and spacecraft. For the case study, we translated the ESL services for managing interacting parallel goal-and-event driven processes into the PROMELA input language of SPIN. A total of five previously undiscovered concurrency errors were identified within the implementation of ESL. According to the Remote Agent programming team, the effort has had a major impact, locating errors that would not have been located otherwise and, in one case, identifying a major design flaw. In fact, in a different part of the system, a concurrency bug identical to one discovered by this study escaped testing and caused a deadlock during an in-flight experiment, 96 million kilometers from Earth. The work additionally motivated the introduction of procedural abstraction in terms of inline procedures into SPIN.

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. To conduct the experiment, a core slice of the DEOS scheduling kernel was first translated without abstraction from C++ into Promela (the input language for Spin). We constructed an abstract “test-driver” environment and carefully introduced several abstractions into the system to support verification. Several experiments were run to attempt to verify that the system implementation adhered to the critical time partitioning requirements. During these experiments, the known error was rediscovered in the time partitioning implementation. We believe this case study provides several insights into how to develop cost-effective methods and tools to support the software design and implementation review process.

Program analysis, testing and verification are key techniques for building confidence in and increasing the quality of software systems. Such activities typically cost upwards of 50% of total development costs. Automation aims to allow both reduced costs and more thorough analysis, testing and verification and is vital to keep pace with increasing software complexity.

Describes the application of the Rebound (REuse Based On UNDerstanding) framework to synthesize event-based software architectures. Within Rebound, deductive techniques are used to select components and wrap them for integration. The framework guides the selection of wrappers based on the problem specification and the components that are available for reuse. The wrapper specifications are used to generate matching conditions for component retrieval, creating a "retrieval for adaptation" scenario. The output of the synthesis activity is mapped to an event-based JavaBeans architecture.

Scaling formal methods to large, complex systems requires methods of modeling systems at high levels of abstraction. In this paper, we describe such a method for specifying system requirements at the software architecture level. An architecture represents a way breaking down a system into a set of interconnected components. We use architecture theories to specify the behavior of a system in terms of the behavior of its components via a collection of axioms. The axioms describe the effects and limits of component variation and the assumptions a component can make about the environment provided by the architecture. As a result of the method the verification of the basic architecture can be separated from the verification of the individual component instantiations. We present an example of using architecture theories to model the task coordination architecture of a multi-threaded plan execution system.