Model Checking Software

Concolic testing is a method for test input generation where a given program is executed both concretely and symbolically at the same time. This paper introduces the LIME Concolic Tester (LCT), an open source concolic testing tool for sequential Java programs. It discusses the design choices behind LCT as well as its use in automated unit test generation for the JUnit testing framework. As the main experimental contribution we report on an empirical evaluation of LCT for testing smart card Java applets. In particular, we focus on the problem of differential testing, where a Java class implementation is tested against a reference implementation. Two different concolic unit test generation approaches are presented and their effectiveness is compared with random testing. The experiments show that concolic testing is able to find significantly more bugs than random testing in the testing domain at hand.

This paper presents an approach to integrate the analysis capabilities of the Spin model checker and the ns-2 network simulator into a single framework. The traffic-oriented model of the protocols is managed by ns-2, while Spin automatically generates the most suitable configurations of each ns-2 run in order to meet some designer requirements. These requirements are specified with assertions and with an annotated temporal logic that can be translated into Spin’s Büchi automata. Spin verification algorithms help us to automatically discard those ns-2 configurations that do not satisfy the expected requirements. With this approach we can automatically obtain the suitable values of parameters like buffer size, timeout to retransmit and window size, to optimize the performance of a protocol implementation in a given scenario. The paper presents the architecture for this integration, the modified temporal logic and its successful application to obtain optimized versions of protocols for videostreaming in wireless networks.

When applying model checking to the design models of the embedded systems, it is necessary to model not only the behavior of the target system but also that of the environment interacting with the system. In this paper, we present a method to model the environment and to automatically generate all possible environments from the model. In our method, we can flexibly model the structural variation of the environment and the sequences of the function calls using a class model and statechart models. We also present a tool to generate Promela scripts of SPIN from the environment model. As a practical experiment, we applied our tool to the verification of an OSEK/VDX RTOS design model.

The increasing popularity of model-based development tools and the growing power of model checkers are making it practical to use formal methods for verification of avionics software. This paper describes a translator framework that enables model checking tools to be easily integrated into a model-based development environment to increase assurance, reduce cost, and satisfy certification objectives. In particular, we describe how formal methods can be used to satisfy certification objectives of DO-178C/ED-12C, the soon-to-be-published guidance document for software aspects of certification for commercial aircraft.

We accelerate state space exploration for explicit-state model checking by executing complex operations on the graphics processing unit (GPU). In contrast to existing approaches enhancing model checking through performing parallel matrix operations on the GPU, we parallelize the breadth-first layered construction of the state space graph. For efficient processing, the input model is translated to the reverse Polish notation, resulting in a representation as an integer vector. The proposed GPU exploration algorithm then divides into two parallel stages. In the first stage, each state is replaced with a Boolean vector to denote which transitions are enabled. In the second stage, pairs consisting of replicated states and enabled transition IDs are copied to the GPU then all transitions are applied in parallel to produce the successors. Bitstate hashing is used as a Bloom filter to remove duplicates from the set of successors in RAM. The experiments show speed-ups of about one order of magnitude. Compared to state-of-the-art in multi-core model checking software, still advances remain visible.

SpinJa is a model checker for promela, implemented in Java. SpinJa is designed to behave similarly to Spin, but to be more easily extendible and reusable. Despite the fact that SpinJa uses a layered object-oriented design and is written in Java, SpinJa’s performance is reasonable: benchmark experiments have shown that, in exhaustive mode, SpinJa is about five times slower than the highly optimized Spin. For bitstate verification runs the difference is only a factor of two.

Explicit-state model checkers like SPIN, which verify systems against properties stated in linear-time temporal logic (LTL), rely on efficient LTL-to-Büchi translators. A difficult design decision in such constructions is to trade time spent on minimizing the Büchi automaton versus time spent on model checking against an unnecessarily large automaton. Standard reduction methods like simulation quotienting are fast but often miss optimization opportunities. We propose a new technique that achieves significant further reductions when more time can be invested in the minimization of the automaton. The additional effort is often justified, for example, when the properties are known in advance, or when the same property is used in multiple model checking runs. We use a modified SAT solver to perform bounded language inclusion checks on partial solutions. SAT solving allows us to prune large parts of the search space for smaller automata already in the early solving stages. The bound allows us to fine-tune the algorithm to run in limited time. Our experimental results show that, on standard LTL-to-Büchi benchmarks, our prototype implementation achieves a significant further size reduction on automata obtained by the best currently available LTL-to-Büchi translators.

In our earlier work we proposed using the declarative language DecSerFlow for modeling, analysis and enactment of processes in autonomous web services. DecSerFlow uses constraints specified with Linear Temporal Logic (LTL) to implicitly define possible executions of a model: any execution that satisfies all constraints is possible. Hence, a finite representation of all possible executions is retrieved as an automaton generated from LTL-based constraints. Standard model-checking algorithms for creating Büchi automata from LTL formulas are not applicable because of the requirements posed by the proper execution of DecSerFlow (and LTL-based process engines). On the one hand, LTL handles infinite words where each element of the word can refer to zero or more propositions. On the other hand, each execution of a DecSerFlow model is a finite sequence of single events. In this paper we adopt an existing approach to finite-word semantics of LTL and propose the modifications of LTL and automata generation algorithm needed to handle occurrences of single events. Besides eliminating errors caused by the ‘multiple properties - single events’ mismatch, the proposed adjustments also improve the performance of the automata generation algorithms dramatically.

We propose the nevertrace claim, which is a new construct for specifying the correctness properties that either finite or infinite execution traces (i.e., sequences of transitions) that should never occur. In semantics, it is neither similar to never claim and trace assertion, nor a simple combination of them. Furthermore, the theoretical foundation for checking nevertrace claims, namely the Asynchronous-Composition Büchi Automaton Control System (AC-BAC System), is proposed. The major contributions of the nevertrace claim include: a powerful construct for formalizing properties related to transitions and their labels, and a way for reducing the state space at the design stage.

I briefly review the history of the unfolding approach to model checking.

We develop an algorithm to compute timed reachability probabilities for distributed models which are both probabilistic and nondeterministic. To obtain realistic results we consider the recently introduced class of (strongly) distributed schedulers, for which no analysis techniques are known.

This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers. The proposed approach proceeds by using finite automata to symbolically represent the possible contents of the store buffers. Store, load and commit operations then correspond to operations on these finite automata.

The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways. An experimental implementation has been used to validate the feasibility of the approach.

Context-Bounded Analysis has emerged as a practical automatic formal analysis technique for fine-grained, shared-memory concurrent software. Two recent papers (in CAV 2008 and 2009) have proposed ingenious translation approaches that promise much better scalability, backed by compelling, but differing, theoretical and conceptual advantages. Empirical evidence comparing the translations, however, has been lacking. Furthermore, these papers focused exclusively on Boolean model checking, ignoring the also widely used paradigm of verification-condition checking. In this paper, we undertake a methodical, empirical evaluation of the three main source-to-source translations for context-bounded analysis of concurrent software, in a verification-condition-checking paradigm. We evaluate their scalability under a wide range of experimental conditions. Our results show: (1) The newest, CAV 2009 translation is the clear loser, with the CAV 2008 translation the best in most instances, but the oldest, brute-force translation doing surprisingly well. Clearly, previous results for Boolean model checking do not apply to verification-condition checking. (2) Disturbingly, confounding factors in the experimental design can change the relative performance of the translations, highlighting the importance of extensive and thorough experiments. For example, using a different (slower) SMT solver changes the relative ranking of the translations, potentially misleading researchers and practitioners to use an inferior translation. (3) SMT runtimes grow exponentially with verification-condition length, but different translations and parameters give different exponential curves. This suggests that the practical scalability of a translation scheme might be estimated by combining the size of the queries with an empirical or theoretical measure of the complexity of solving that class of query.

We present a reduction from a concurrent real-time program with priority preemptive scheduling to a sequential program that has the same set of behaviors. Whereas many static analyses of concurrent programs are undecidable, our reduction enables the application of any sequential program analysis to be applied to a concurrent real-time program with priority preemptive scheduling.