Catálogo de publicaciones - libros

We describe a framework for dynamic verification of temporal assertions based on assertion compilation into deterministic automata. The novelty of our approach is that it allows efficient dynamic verification of general linear temporal formulas written in formal property specification languages such as LTL, ForSpec, PSL, and SVA, while the existing approaches are applicable to limited subsets only. We also show an advantage of the described framework over industrial simulators, which typically use transaction-based verification. Another advantage of our approach is its ability to use deterministic checkers directly for hardware emulation. Finally, we compare the deterministic compilation with the OBDD-based on-the-fly simulation of deterministic automata. We show that although the OBDD-based simulation method is much slower, the two methods may be efficiently combined for hybrid simulation, when the RTL signals in assertions are mixed with symbolic variables.

In this paper, we consider the robust interpretation of metric temporal logic (MTL) formulas over timed sequences of states. For systems whose states are equipped with nontrivial metrics, such as continuous, hybrid, or general metric transition systems, robustness is not only natural, but also a critical measure of system performance. In this paper, we define robust, multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, , from unsatisfiability. We prove that any other timed trace which remains -close to the initial one also satisfies the same MTL specification with the usual Boolean semantics. We derive a computational procedure for determining an under-approximation to the robustness degree of the specification with respect to a given finite timed state sequence. Our approach can be used for robust system simulation and testing, as well as form the basis for simulation-based verification.

We present a new lockset-based algorithm, Goldilocks, for precisely computing the happens-before relation and thereby detecting data-races at runtime. Dynamic race detection algorithms in the literature are based on vector clocks or locksets. Vector-clock-based algorithms precisely compute the happens-before relation but have significantly more overhead. Previous lockset-based race detection algorithms, on the other hand, are imprecise. They check adherence to a particular synchronization discipline, i.e., a sufficient condition for race freedom and may generate false race warnings. Our algorithm, like vector clocks, is precise, yet it is efficient since it is purely lockset based.

We have implemented our algorithm inside the Kaffe Java Virtual Machine. Our implementation incorporates lazy evaluation of locksets and certain “short-circuit checks” which contribute significantly to its efficiency. Experimental results indicate that our algorithm’s overhead is much less than that of the vector-clock algorithm and is very close to our implementation of the Eraser lockset algorithm.

Object models capture key properties of object-oriented architectures, and they can highlight relationships between types, occurrences of sharing, and object encapsulation. We present a dynamic analysis to extract object models from legacy code bases. Our analysis reconstructs each intermediate heap from a log of object allocations and field writes, applies a sequence of abstraction-based operations to each heap, and combines the results into a single object model that conservatively approximates all observed heaps from the program’s execution. The resulting object models reflect many interesting and useful architectural properties.

This paper describes the automated generation of test sequences derived from a JML specification and a safety property written in an ad hoc language, named JTPL. The functional JML model is animated to build the test sequences w.r.t. the safety properties, which represent the test targets. From these properties, we derive strategies that are used to guide the symbolic animation. Moreover, additional JML annotations reinforce the oracle in order to guarantee that the safety properties are not violated during the execution of the test suite. Finally, we illustrate this approach on an industrial JavaCard case study.

Online testing is a practical technique where test derivation and test execution are combined into a single algorithm. In this paper we describe a new online testing algorithm that optimizes the choice of test actions using Reinforcement Learning (RL) techniques. This provides an advantage in covering system behaviors in less time than with a purely random choice of test actions. Online testing with conformance checking is modeled as a 1-player game, or Markov Decision Process (MDP), between the tester as one player and the implementation under test (IUT) as the opponent. Our approach has been implemented in C#, and benchmark results are presented in the paper. The specifications that generate the tests are written as model programs in any .NET language such as C# or VB.