Catálogo de publicaciones - libros

are frequently used to model abstractions of software programs. They have the advantage that reachability properties are decidable, despite the fact that their stack is not bounded. The enabling technique is of procedure calls. Most model checking tools for Boolean programs use BDDs to represent these summaries, allowing for efficient fix-point detection. However, BDDs are highly sensitive to the number of state variables. We present an approach to over-approximate summaries using Bounded Model Checking. Our technique is based on a SAT solver and requires only few calls to a QBF solver for fix-point detection. Our benchmarks show that our implementation is able handle a larger number of variables than BDD-based algorithms on some examples.

We report here on an experimental investigation of LTL satisfiability checking via a reduction to model checking. By using large LTL formulas, we offer challenging model-checking benchmarks to both explicit and symbolic model checkers. For symbolic model checking, we use both CadenceSMV and NuSMV. For explicit model checking, we use SPIN as the search engine, and we test essentially all publicly available LTL translation tools. Our experiments result in two major findings. First, most LTL translation tools are research prototypes and cannot be considered industrial quality tools. Second, when it comes to LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach.

The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine’s (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker’s , or even C. As added value, it provides efficiently executable operational semantics for modelling languages. Several tools have been built on top of the VM implementation we developed, to evaluate the benefits of the proposed approach.

Recent development in computer hardware has brought more wide-spread emergence of shared-memory, multi-core systems. These architectures offer opportunities to speed up various tasks – among others LTL model checking. In the paper we show a design for a parallel shared-memory LTL model checker, that is based on a distributed-memory algorithm. To achieve good scalability, we have devised and experimentally evaluated several implementation techniques, which we present in the paper.

SystemC has become a standard for the modeling of systems-on-a-chip, at various levels of abstraction, including the so-called (TL). Verifying properties of a TL model requires that SystemC be translated into some formally defined language for which there exist verification back-ends. Since SystemC has no formal semantics, this includes a careful encoding of the SystemC scheduler, which has both synchronous and asynchronous features, and a notion of time. In a previous work, we presented a complete chain from SystemC to a synchronous formalism and its associated verification tools. In this paper, we describe the encoding of the SystemC scheduler into an formalism, namely (the input language for ). We comment on the possible uses for this new encoding.

We present an approach for the verification of spatial properties with . We first extend one of ’s main property specification mechanisms, i.e., the linear-time temporal logic LTL, with spatial connectives that allow us to restrict the reasoning of the behaviour of a system to some components of the system, only. For instance, one can express whether the system can reach a certain state from which a subset of processes can evolve alone until some property is fulfilled. We give a model checking algorithm for the logic and propose how can be minimally extended to include the algorithm. We also discuss potential improvements to mitigate the exponential complexity introduced by spatial connectives. Finally, we present some experiments that compare our extension with a spatial model checker for the -calculus.

One of the most exciting and promising approaches to ensure the correctness of critical systems is , which considers real code, written with standard programming languages like . One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, like . This paper presents the application of the technique to avionics software constructed on top of an application interface () compliant with the 653 specification (), which is widely employed by the manufacturers in the avionics industry. The paper uses techniques to automatically extract models from C source code. These techniques were previously developed by the authors. However, they are now extended to deal with new problems, like real-time aspects and scheduling. In order to close the extracted model during the verification, we built a reusable environment. This environment models the execution engine (i.e. an compliant RTOS) that implements services. Finally, this paper also contains a novel testing method to ensure the correctness of this environment. This testing method uses to execute official 653 test cases.

We present — BEnchmarks for Explicit Model checkers. This benchmark set includes more than 50 parametrized models (300 concrete instances) together with their correctness properties (both safety and liveness). The benchmark set is accompanied by an comprehensive web portal, which provides detailed information about all models. The web portal also includes information about state spaces and facilities for selection of models for experiments.

The address of the web portal is .

This paper describes a set of verification components that open the way to perform on-the-fly software model checking with the toolbox, originally designed for verifying the functional correctness of specifications. Two new tools (named and ) have been added to the toolbox. The approach taken fits well within the existing architecture of which doesn’t need to be altered to enable program verification.

ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement) is a software model checker for C programs in the spirit of Blast [6], F-Soft [7], Magic [5] and Slam [1]. It is based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Its specificity lies in the way it overcomes a problem common to all tools based on this paradigm. The problem arises from creating more and more spurious counterexamples by unfolding the same (while- or for-) loop over and over again; this leads to an infinite or at least too large sequence of refinement steps. The idea behind ACSAR is to abstract not just states but also the state changes induced by structured program statements, including for- and while-statements. The use of the new abstraction allows one to shortcut such a “transfinite” sequence of refinement steps.