Catálogo de publicaciones - libros

Unbounded model checking methods based on Boolean satisfiability (SAT) solvers are proving to be a viable alternative to BDD-based model checking. These methods include, for example, interpolation based and sequential ATPG-based approaches. In this paper, we explore the implications of using abstraction refinement in conjunction with interpolation-based model checking. Based on experiments using a large industrial benchmark set, we conclude that when using interpolation- based model checking, measures must be taken to prevent the overhead of abstraction refinement from dominating runtime. We present two new approaches to this problem. One is a hybrid approach that decides heuristically when to apply abstraction. The other is a very coarse but inexpensive abstraction method based on ideas from ATPG. This approach can produce order-of-magnitude reductions in memory usage, allowing significantly larger designs to be verified.

The analysis of message sequence charts (MSCs) is highly important in preventing common problems in communication protocols. Detecting race conditions, i.e., possible discrepancies in event order, was studied for a single MSC and for MSC graphs (a graph where each node consists of a single MSC, also called HMSC). For the former case, this problem can be solved in quadratic time, while for the latter case it was shown to be undecidable. However, the prevailing real-life situation is that a collection of MSCs, called here an , describing the different possible scenarios of the system behavior, is provided, rather than a single MSC or an MSC graph. For an ensemble of MSCs, a potential race condition in one of its MSCs can be compensated by another MSC in which the events occur in a different order. We provide a polynomial algorithm for detecting races in an ensemble. On the other hand, we show that in order to prevent races, the size of an ensemble may have to grow exponentially with the number of messages. Also, we initiate the formal study of the standard MSC construct, which is used to relax the order among events of a process. We show that by using this construct, we can provide more compact race-free ensembles; however, detecting races becomes NP-complete.

This paper is concerned with bridging the gap between requirements, provided as a set of scenarios, and conforming design models. The novel aspect of our approach is to exploit for the synthesis of design models. In particular, we present a procedure that infers a message-passing automaton (MPA) from a given set of positive and negative scenarios of the system’s behavior provided as message sequence charts (MSCs). The paper investigates which classes of regular MSC languages and corresponding MPA can (not) be learned, and presents a dedicated tool based on the learning library that supports our approach.

We propose and evaluate new algorithms to support the automata-based approach to model-checking: algorithms to solve the universality and language inclusion problems for nondeterministic Büchi automata. To obtain those new algorithms, we establish the existence of pre-orders that can be exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of our new algorithm to check for universality of Büchi automata experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude. This work is an extension to the infinite words case of new algorithms for the finite words case that we and co-authors have presented in a recent paper [DDHR06].

In this paper, we present a tool named GOAL (an acronym derived from “raphical Tool for mega-utomata and ogics”) whose main functions include (1) drawing and testing Büchi automata, (2) checking the language equivalence between two Büchi automata, (3) translating quantified propositional linear temporal logic (QPTL) formulae into equivalent Büchi automata, and (4) exporting Büchi automata as Promela code. The GOAL tool, available at , can be used for educational purposes, helping the user get a better understanding of how Büchi automata work and how they are related to linear temporal logics. It may also be used, as we shall explain below, to construct correct and smaller specification automata, supplementing model checkers that adopt the automata-theoretic approach, such as SPIN [5].

The theory of games is a prominent tool in the controller synthesis problem. The class of -regular games, in particular, offers a clear and robust model of specifications, and present an alternative vision of several logic-related problems. Each -regular condition can be expressed by a combination of safety and liveness conditions. An issue with the classical definition of liveness specifications is that there is no control over the time spent between two successive occurrences of the desired events. Finitary logics were defined to handle this problem, and recently, Chatterjee and Henzinger introduced games based on a finitary notion of liveness. They defined and studied finitary parity and Streett winning conditions. We present here faster algorithms for these games, as well as an improved upper bound on the memory needed by Eve in the Streett case.

We introduce a novel approach to the smart execution of scenario-based models of reactive systems, such as those resulting from the multi-modal inter-object language of live sequence charts (LSCs). Our approach finds multiple execution paths from a given state of the system, and allows the user to interactively traverse them. The method is based on translating the problem of finding a superstep of execution into a problem in the AI planning domain, and issuing a known planning algorithm, which we have had to modify and strengthen for our purposes.

The Tool Environment is a tool to facilitate the transformation, analysis and validation of models. is a modelling language to describe stochastic real-time systems. implements the formal semantics of and is designed to transform and abstract specifications such that analysis can be carried out by third-party tools. For the time being, a fragment of can be model-checked using . The main analytical workhorse behind is discrete-event simulation, which is provided by the performance evaluation environment. We are experimenting with prototypical connections to the real-time model checker .

The IEEE standard Property Specification Language (PSL) allows to express all -regular properties mixing Linear Temporal Logic (LTL) with Sequential Extended Regular Expressions (SEREs), and is increasingly used in many phases of the hardware design cycle, from specification to verification.

In recent works, we propose a modular and symbolic PSL compilation that is extremely fast in conversion time and outperforms by several orders of magnitude translators based on the explicit construction and minimization of automata. Unfortunately, our approach creates rather redundant automata, which result in a penalty in verification time.

In this paper, we propose a set of syntactic simplifications that enable to significantly improve the verification time without paying the price of automata simplifications. A thorough experimental analysis over large sets of paradigmatic properties shows that our approach drastically reduces the overall verification time.

Heterogeneous specification becomes more and more important because complex systems are often specified using multiple viewpoints, involving multiple formalisms (see Fig. 1). Moreover, a formal software development process may lead to a change of formalism during the development.

Some of the current heterogeneous approaches deliberately stay informal, like UML. Current formal integration approaches have the drawback that they are uni-lateral in the sense that typically there is one logic (and one theorem prover) which serves as the central integration device, even if this central logic may not be needed or desired in particular applications.

By contrast, the heterogeneous tool set is a both flexible,multi-lateral and formal (i.e. based on a mathematical semantics) integration tool, providing parsing, static analysis and proof management for heterogeneous multi-logic specifications by combining various tools for individual specification languages. Unlike other tools, it treats logic translations (e.g. codings between logics) as first-class citizens. The architecture of the heterogeneous tool set is shown in Fig. 2. In the sequel, we will explain the details of this figure.