Catálogo de publicaciones - libros

Dynamic fault trees (DFTs) are a versatile and common formalism to model and analyze the reliability of computer-based systems. This paper presents a formal semantics of DFTs in terms of input/output interactive Markov chains (I/O-IMCs), which extend continuous-time Markov chains with discrete input, output and internal actions. This semantics provides a rigorous basis for the analysis of DFTs. Our semantics is fully compositional, that is, the semantics of a DFT is expressed in terms of the semantics of its elements (i.e. basic events and gates). This enables an efficient analysis of DFTs through compositional aggregation, which helps to alleviate the state-space explosion problem by incrementally building the DFT state space. We have implemented our methodology by developing a tool, and showed, through four case studies, the feasibility of our approach and its effectiveness in reducing the state space to be analyzed.

Symbolic Trajectory Evaluation (STE) is a powerful technique for hardware model checking. It is based on a 3-valued symbolic simulation, using 0,1 and (”unknown”), where the is used to abstract away values of the circuit nodes.

Most STE tools are BDD-based and use a dual rail representation for the three possible values of circuit nodes. SAT-based STE tools typically use two variables for each circuit node, to comply with the dual rail representation.

In this work we present a novel 3-valued Circuit SAT-based algorithm for STE. The STE problem is translated into a Circuit SAT instance. A solution for this instance implies a contradiction between the circuit and the STE assertion. An unSAT instance implies either that the assertion holds, or that the model is too abstract to be verified. In case of a too abstract model, we propose a refinement automatically.

We implemented our 3-Valued Circuit SAT-based STE algorithm and applied it successfully to several STE examples.

The bounded synthesis problem is to construct an implementation that satisfies a given temporal specification and a given bound on the number of states. We present a solution to the bounded synthesis problem for linear-time temporal logic (LTL), based on a novel emptiness-preserving translation from LTL to safety tree automata. For distributed architectures, where standard unbounded synthesis is in general undecidable, we show that bounded synthesis can be reduced to a SAT problem. As a result, we obtain an effective algorithm for the bounded synthesis from LTL specifications in arbitrary architectures. By iteratively increasing the bound, our construction can also be used as a semi-decision procedure for the unbounded synthesis problem.

One of the prerequisites for information society is and communication among computing systems. Accordingly, network security appliances become key components of infrastructure, not only as security guardians, but also as reliable network components. Thus, for both fault tolerance and high network throughput, multiple security appliances are often deployed together in a group and managed via protocol.

In this paper, we present our experience of formally modeling and verifying the HA protocol used for commercial network security appliances through model checking. In addition, we applied a new debugging technique to detect bugs modifying/fixing the HA model by analyzing all counter examples. Throughout these formal analysis, we could effectively detect several design flaws.

In this paper we extend  (Hypotheses and Observations Testing Logic) to provide a formal framework to test timed systems. The main idea underlying  is to infer whether a set of (i.e., results of test applications) allows to claim that the IUT conforms to the specification a specific set of hypotheses is assumed. In this paper we adapt to cope with the inclusion of time issues. In addition, we show the soundness and completeness of the new framework, that we call , with respect to a general notion of timed conformance.

A fair non-repudiation protocol should guarantee, (1) when a sender sends a message to a receiver, neither the sender nor the receiver can deny having participated in this communication; (2) no principals can obtain evidence while the other principals cannot do so. This paper extends the model in our previous work [12], and gives a sound and complete on-the-fly model checking method for fair non-repudiation protocols under the assumption of a bounded number of sessions. We also implement the method using Maude. Our experiments automatically detect flaws of several fair non-repudiation protocols.

In a companion paper [BPV06], we investigated the expressiveness of Time Petri Nets extended with Priorities and showed that it is very close to that Timed Automata, in terms of weak timed bisimilarity. As a continuation of this work we investigate here the applicability of the available state space abstractions for Bounded Time Petri Nets to Bounded Prioritized Time Petri Nets. We show in particular that a slight extension of the “strong state classes” construction of [BV03] provides a convenient state space abstraction for these nets, preserving markings, states, and formulas. Interestingly, and conversely to Timed Automata, the construction proposed does not require to compute polyhedra differences.

Property classifications and patterns, i.e., high-level abstractions that describe common behavior, have been used to assist practitioners in generating formal specifications that can be used in formal verification techniques. The Specification Pattern System (SPS) provides descriptions of a collection of patterns. Each pattern is associated with a scope that defines the extent of program execution over which a property pattern is considered. Based on a selected pattern, SPS provides a specification for each type of scope in multiple formal languages including Linear Temporal Logic (LTL). The (Prospec) tool extends SPS by introducing the notion of Composite Propositions (CP), which are classifications for defining sequential and concurrent behavior to represent pattern and scope parameters.

In this work, we provide definitions of patterns and scopes when defined using CP classes. In addition, we provide general (template) LTL formulas that can be used to generate LTL specifications for all combinations of pattern, scope, and CP classes.

This paper focuses on using beam search, a heuristic search algorithm, for pruning state spaces while generating. The original beam search is adapted to the state space generation setting and two new search variants are devised. The resulting framework encompasses some known algorithms, such as . We also report on two case studies based on an implementation of beam search in CRL.

Due to the success of the model checking technique in the hardware domain, over the last few years, model checking methods have been applied to the software domain which poses its own challenges, as software tends to be less structured than hardware. Predicate abstraction is widely applied to reduce the state-space by mapping an infinite state-space program to an abstract program of Boolean type. The cost for computation of abstraction and model checking depends on the number of state variables in the abstract model. In this paper, we propose a simple, yet efficient method to minimize the number of predicates for predicate abstraction. Given a spurious counterexample, at least one predicate is assigned at each program location during the refinement process. The computational cost depends proportionally to the number of assigned predicates. In this paper, instead, we search the counterexample to find the conflict predicates that caused this counterexample to be spurious. Then, we assign the necessary predicates to the abstract model. We compare the performance of our technique with the interpolation-based predicate abstraction tool like BLAST. The proposed method presents significantly better experimental results on some examples with large set of predicates.