Efficient explicit-state model checking for programs with dynamically allocated data

ABSTRACT

Despite the technological advances in languages and tools to support program development, programmers still deliver software with lots of errors. Software testing has been the dominant approach in industry to improve the quality of software at code level. Testing software is not cheap though. A study done in 2002 by the National Institute of Standards and Technology (NIST) [NIS02] reports that between 70% and 80% of development costs is due to testing. We believe that automation of software testing can help to reduce this cost; automation can assist the programmer to test the code under development in a more systematic way.

Software model checkers are becoming increasingly popular to assist in the automation of software testing. Model checkers are tools that systematically explore the state space of a model to demonstrate the presence of errors or to confirm their absence. For example, a model checker can report a test whenever it finds an "interesting" state, i.e., a state which violates a user-defined assertion or a state that makes execution throw a runtime exception.

This dissertation focuses on software model checkers that operate directly on code. Model checking programs is becoming very popular, as it enables the discovery of errors in the implementation as opposed to errors in a system design.

However, model checking programs poses particular challenges. It is the implementation that defines the model, not the design. As a consequence, a deterministic step of the exploration can be potentially more expensive as it may require the execution of a complex fragment of sequential code. In addition, the states that the model defines are potentially larger, making important operations that depend on the size of the state potentially slower.

While state-space explosion has been traditionally the key issue in model checking, time efficiency becomes more relevant with the increasing appearance of model checkers that operate on programs. Our goal is to improve time efficiency for model checking programs that allocate dynamic data. Such programs are pervasive nowadays with the wide use of object-oriented languages.

To that end, this dissertation presents Mixed execution and ΔExecution. Mixed execution speeds up the execution of deterministic steps in model checkers that use a special representation of state. Such representation can be convenient to perform some model checking operations but sacrifices the execution of deterministic steps (i.e., fragments of sequential code). ΔExecution uses sets of states to perform state-space exploration. The use of sets enables the model checker to take advantage of overlappings (of state and paths) that exist in a systematic exploration of state, speeding up several operations in software model checking.

We implemented mixed execution in Java PathFinder (JPF), a model checker for Java programs. We evaluate mixed execution on seven simple subject programs and one large case study. The experimental results on the seven smaller programs show that mixed execution can improve the overall time for state exploration in JPF from 1.01x to 1.73x (with median 1.13x). The experimental results on a larger case study show that the exploration time on this experiment reduces from 1.14x to 1.41x (with median 1.23x).

We implemented Delta Execution in two model checkers, JPF (Java PathFinder) and BOX (Bounded Object eXploration) to evaluate the effectiveness of this technique in model checkers with different designs. The results show that ΔExecution improves the overall exploration in both tools, but the improvements are due to different factors. We evaluate ΔExecution on ten simple subject programs and a larger case study. The results show that ΔExecution improves the exploration time for the smaller programs from 0.88x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX, while takingfrom 0.46x to 11.50x (with median 1.48x) less memory in JPF and from 0.18x to 2.71x (with median 1.18x) memory in BOX. The experimental results on one larger case study show that ΔExecution improves the exploration time from 0.88x to 2.04x (with median 1.72x). Note that a ratio smaller than 1 means a slow down or use of more memory. Such ratios can arise in the exploration of small state-spaces.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Algorithms, Design, Performance, Verification