Competent predicate abstraction in model checking

The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counterexample-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the app...     

Boolean and Cartesian abstraction for model checking C programs

We show how to attack the problem of model checking a C program with recursive procedures using an abstraction that we formally define as the composition of the Boolean and the Cartesian abstractions. It is implemented through a source-to-source transformation into a Boolean C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.     

Combining predicate and numeric abstraction for software model checking

Predicate (PA) and numeric (NA) abstractions are the two principal techniques for software analysis. In this paper, we develop an approach to couple the two techniques tightly into a unified framework via a single abstract domain called NumPredDom. In particular, we develop and evaluate four data structures that implement NumPredDom but differ in their expressivity and internal representation and algorithms. All our data structures combine BDDs (for efficient propositional reasoning) with data structures for representing numerical constraints. Our technique is distinguished by its support for complex transfer functions that allow two-way interaction between predicate and numeric information during state transformation. We have implemented a general framework for reachability analysis of C programs on top of our four data structures. Our experiments on non-trivial examples show that our proposed combination of PA and NA is more powerful and more efficient than either technique alone.     

Combining search space partition and abstraction for LTL model checking

The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the integration of search space partition and abstraction improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.     

Towards model checking executable UML specifications in mCRL2

We describe a translation of a subset of executable UML (xUML) into the process algebraic specification language mCRL2. This subset includes class diagrams with class generalisations, and state machines with signal and change events. The choice of these xUML constructs is dictated by their use in the modelling of railway interlocking systems. The long-term goal is to verify safety properties of interlockings modelled in xUML using the mCRL2 and LTSmin toolsets. Initial verification of an interlocking toy example demonstrates that the safety properties of model instances depend crucially on the run-to-completion assumptions.     

Checking JML specifications using an extensible software model checking framework

The use of assertions to express correctness properties of programs is growing in practice. Assertions provide a form of lightweight checkable specification that can be very effective in finding defects in programs and in guiding developers to the cause of a problem. A wide variety of assertion languages and associated validation techniques have been developed, but run-time monitoring is commonly thought to be the only practical solution. In this paper, we describe how specifications written in the Java Modeling Language (JML), a general purpose behavioral specification and assertional language for Java, can be validated using a customized model checker built on top of the Bogor model checking framework. Our experience illustrates the need for customized state-space representations and reduction strategies in model checking frameworks in order to effectively check the kind of strong behavioral specifications that can be written in JML. We discuss the advantages and tradeoffs of model checking relative to other specification validation techniques and present data that suggest that the cost of model checking strong specifications is practical for several real programs. This is an extended version of the paper Checking Strong Specifications Using An Extensible Model Checking Framework that appeared in Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004. This work was supported in part by the U.S. Army Research Office (DAAD190110564), by DARPA/IXO’s PCES program (AFRL Contract F33615-00-C-3044), by NSF (CCR-0306607) by Lockheed Martin, and by Rockwell-Collins.     

Inferring specifications to detect errors in code

A new technique is presented to statically check a given procedure against a user-provided property. The method requires no annotations; it automatically infers a context-dependent specification for each procedure call, so that only as much information about a procedure is used as is needed to analyze its caller. Specifications are inferred iteratively. Empty specifications are initially used to over-approximate the effects of all procedure calls; these are later refined in response to spurious counterexamples. When the analysis terminates, any remaining counterexample is guaranteed to be valid. However, since the heap is finitized, the absence of a counterexample does not guarantee the validity of the given property in general.

Combining search space partition and search Space partition and abstraction for LTL model checking

The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size.Abstraction-based methods have been particularly successful in this regard.This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking.The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the Integration of search space partition and abstraction improves the efficiencyof verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.     

Using model checking to identify errors in intrusion detection signatures

Most intrusion detection systems deployed today apply misuse detection as analysis method. Misuse detection searches for attack traces in the recorded audit data using predefined patterns. The matching rules are called signatures. The definition of signatures is up to now an empirical process based on expert knowledge and experience. The analysis success and accordingly the acceptance of intrusion detection systems in general depend essentially on the topicality of the deployed signatures. Methods for a systematic development of signatures have scarcely been reported yet, so the modeling of a new signature is a time-consuming, cumbersome, and error-prone process. The modeled signatures have to be validated and corrected to improve their quality. So far only signature testing is applied for this. Signature testing is still a rather empirical and time-consuming process to detect modeling errors. In this paper, we present the first approach for verifying signature specifications using the Spin model checker. The signatures are modeled in the specification language EDL, which leans on colored Petri nets. We show how the signature specification is transformed into a Promela model and how characteristic specification errors can be found by Spin.     

Using model checking to assess the dependability of agent-based systems

Model checking and the problem of analyzing the dependability of complex agent-based systems are well matched. Mathematical models of simple agents are relatively straightforward to specify. We can construct a model of the system as a whole from the models of the individual agents, and we can easily express dependability properties in the logical language used in model checking. However, there's one crucial mismatch: the state spaces of complex systems are many orders of magnitude larger than automated model-checking tools can handle. So, the mathematical models of computing systems that we use in model checking must be much simpler than the systems we are modeling. Yet, the models must contain all the detail that's essential to the dependability analysis we are performing, because omitting relevant detail can invalidate the analysis results. To make model checking of agent-based systems feasible and useful, we must answer two crucial questions. Here we describe our current best answers to these questions and how we've applied them to a real-world problem - assessing the UltraLog system.     

Infinite-state invariant checking with IC3 and predicate abstraction

We address the problem of verifying invariant properties on infinite-state systems. We present a novel approach, IC3ia, for generalizing the IC3 invariant checking algorithm from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit Abstraction, a form of predicate abstraction that expresses abstract paths without computing explicitly the abstract system. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike previous SMT generalizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available and are often highly inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improvement, as our experiments demonstrate.     

Using tool abstraction to compose systems

The tool abstraction paradigm, which supports the evolution of large-scale software systems by easing design changes in the system functions, is discussed. Systems that support tool abstraction are structured as a pool of abstract data structures shared by a collection of cooperating `toolies', where each toolie provides a piece of the overall system function. When one toolie updates the shared data, other toolies must be notified: otherwise, cooperating-but-independent toolies may not execute, and the overall system function may be compromised. The KWIC (key word in context) index production system is used to illustrate the idea of tool abstraction. The relationship of tool abstraction to other concepts is examined     

Using probabilistic model checking for dynamic power management

Dynamic power management (DPM) refers to the use of runtime strategies in order to achieve a tradeoff between the performance and power consumption of a system and its components. We present an approach to analysing stochastic DPM strategies using probabilistic model checking as the formal framework. This is a novel application of probabilistic model checking to the area of system design. This approach allows us to obtain performance measures of strategies by automated analytical means without expensive simulations. Moreover, one can formally establish various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy.Received November 2003Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement

The stochastic dynamics of biochemical reaction networks can be modeled using a number of succinct formalisms all of whose semantics are expressed as Continuous Time Markov Chains (CTMC). While some kinetic parameters for such models can be measured experimentally, most are estimated by either fitting to experimental data or by performing ad hoc, and often manual search procedures. We consider an alternative strategy to the problem, and introduce algorithms for automatically synthesizing the set of all kinetic parameters such that the model satisfies a given high-level behavioral specification. Our algorithms, which integrate statistical model checking and abstraction refinement, can also report the infeasibility of the model if no such combination of parameters exists. Behavioral specifications can be given in any finitely monitorable logic for stochastic systems, including the probabilistic and bounded fragments of linear and metric temporal logics. The correctness of our algorithms is established using a novel combination of arguments based on survey sampling and uniform continuity. We prove that the probability of a measurable set of paths is uniformly and jointly continuous with respect to the kinetic parameters. Under a suitable technical condition, we also show that the unbiased statistical estimator for the probability of a measurable set of paths is monotonic in the parameter space. We apply our algorithms to two benchmark models of biochemical signaling, and demonstrate that they can efficiently find parameter regimes satisfying a given high-level behavioral specification. In particular, we show that our algorithms can synthesize up to 6 parameters, simultaneously, which is more than that reported by any other synthesis algorithm for stochastic systems. Moreover, when parameter estimation is desired, as opposed to synthesis, we show that our approach can scale to even higher dimensional spaces, by identifying the single parameter combination that maximizes the probability of the behavior being true in an 11-dimensional system.     

Using function abstraction to understand program behavior

The authors explain how to understand programs by abstracting program function. This abstraction is made possible by the algebraic structure and mathematical properties of structured programs. They describe an abstraction algorithm that provides a basis for a tool for automatic abstraction of program functions. They also explore what the goals of a program-abstraction tool should be. A miniature Cobol program for a banking application is used as an example     

Using formal specifications to support software testing

Formal specifications become more and more important in the development of software, especially but not only in the area of high integrity system design. In this paper it is demonstrated, how, apart from the specification phase, further benefits may be drawn from formal specifications for checking the implementation against the specification. It is shown how the specification can be used for systematically deriving test input data and for automatically evaluating test results. The approach is illustrated using the specification language Z. The same principles may be applied to other specification languages. The approach allows a high degree of automation, drastically improving productivity and quality of the testing process.     

Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard

We examine the application of symbolic CTL model checking to railway interlocking software. We show that the railway interlocking systems examined exhibit the characteristics of robustness and locality, and that these characteristics allow optimizations to the model checking algorithms not possible in the general case. In order to gain a better understanding of robustness and locality, we examine in detail a small railway interlocking. Published online: 9 October 2001     

Using model checking to analyze the system behavior of the LHC production grid

DIRAC (Distributed Infrastructure with Remote Agent Control) is the grid solution designed to support production activities as well as user data analysis for the Large Hadron Collider “beauty” experiment. It consists of cooperating distributed services and a plethora of light-weight agents delivering the workload to the grid resources. Services accept requests from agents and running jobs, while agents actively fulfill specific goals. Services maintain database back-ends to store dynamic state information of entities such as jobs, queues, or requests for data transfer. Agents continuously check for changes in the service states and react to these accordingly. The logic of each agent is rather simple; the main source of complexity lies in their cooperation. These agents run concurrently and communicate using the services’ databases as a shared memory for synchronizing the state transitions. Despite the effort invested in making DIRAC reliable, entities occasionally get into inconsistent states. Tracing and fixing such behaviors is difficult, given the inherent parallelism among the distributed components and the size of the implementation.In this paper we present an analysis of DIRAC with mCRL2, process algebra with data. We have reverse engineered two critical and related DIRAC subsystems, and subsequently modeled their behavior with the mCRL2 toolset. This enabled us to easily locate race conditions and livelocks which were confirmed to occur in the real system. We further formalized and verified several behavioral properties of the two modeled subsystems.     

Using induction and rewriting to verify and complete parameterized specifications

In software engineering there is a growing demand for formal methods for the specification and validation of software systems. The formal development of a system might give rise to many proof obligations. We must prove the completeness of the specification and the validity of some inductive properties. In this framework, many provers have been developed. However they require much user interaction even for simple proof tasks. In this paper, we present new procedures to test sufficient completeness and to prove or disprove inductive properties automatically in para-meterized conditional specifications. The method has been implemented in the prover SPIKE. Computer experiments illustrate the improvements in length and structure of proofs, due to parameterization. Moreover, SPIKE offers facilities to check and complete specifications.