FATES-RV on Wednesday, August 16th

Session 5: Invited Talk (09:30‑10:30)

09:30‑10:30

Oege de Moor (Oxford University, GB) Aspects for Trace Monitoring [pdf] A “trace monitor” observes the sequence of events in a system, and takes appropriate action when a given pattern occurs in that sequence. Aspect-oriented programming provides a convenient framework for writing such trace monitors. We provide a brief introduction to aspect-oriented programming in AspectJ. AspectJ only provides support for triggering extra code with single events, and we present a new language feature (named “tracematches”) that allows one to directly express patterns that range over the whole current trace. Implementing this feature efficiently is challenging, and we report on our work towards that goal. Another drawback of AspectJ is the highly syntactic nature of the event patterns, often requiring the programmer to list all methods that have a certain property, rather than specifying that property itself. We argue that Datalog provides an appropriate notation for describing such properties. Furthermore, all of the existing patterns in AspectJ can be reduced to Datalog via simple rewrite rules. This research is carried out with “abc”, an extensible optimising compiler for AspectJ, which is freely available for download. See tool website.

Break (10:30‑11:00)

Session 6 (11:00‑12:30)

11:00‑11:30	Moez Krichen (VERIMAG) Stavros Tripakis (VERIMAG) State-Identification Problems for Finite-State Transducers A well-established theory exists for testing finite-state machines, in particular Moore and Mealy machines. A fundamental class of problems handled by this theory is state identification: we are given a machine with known state space and transition relation but unknown initial state, and we are asked to find experiments which permit to identify the initial or final state of the machine, called distinguishing and homing experiments, respectively. In this paper, we study state-identification for finite-state transducers. The latter are a generalization of Mealy machines where outputs are sequences rather than symbols. Transducers permit to model systems where inputs and outputs are not synchronous, as is the case in Mealy machines. It is well-known that every deterministic and minimal Mealy machine admits a homing experiment. We show that this property fails for transducers, even when the latter are deterministic and minimal. We also provide answers to the decidability question, namely, checking whether a given transducer admits a particular type of experiment. First, we show how the standard successor-tree algorithm for Mealy machines can be turned into a semi-algorithm for transducers. Second, we show that the state-identification problems are undecidable for finite-state transducers in general. Finally, we identify a sub-class of transducers for which these problems are decidable. A transducer in this sub-class can be transformed into a Mealy machine, to which existing methods apply.
11:30‑12:00	Roy Armoni (-) Dmitry Korchemny (Intel) Andreas Tiemeyer (Intel) Moshe Y. Vardi (Rice University and Microsoft Research) Yael Zbar (Intel) Deterministic Dynamic Monitors for Linear-Time Assertions 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.
12:00‑12:30	Georgios Fainekos (University of Pennsylvania) George Pappas (University of Pennsylvania) Robustness of Temporal Logic Specifications 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, epsilon, from unsatisfiability. We prove that any other timed trace which remains epsilon-close to the initial one also satisfies the same MTL specification with the usual Boolean semantics. We derive a computational procedure for determining the robustness degree epsilon of the specification with respect to a given finite timed trace. Our approach can be used for robust system simulation and testing, as well as form the basis for simulation-based verification.

Lunch break (12:30‑14:00)

Session 7 (14:00‑15:30)

14:00‑14:30	Tayfun Elmas (Koc University) Shaz Qadeer (Microsoft) Serdar Tasiran (Koç University) Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets We present a new lockset-based algorithm, called 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 the Eraser lockset algorithm.
14:30‑15:00	Cormac Flanagan (Univ of California Santa Cruz) Stephen N. Freund (Williams College) Dynamic Architecture Extraction Object models capture key properties of object-oriented architectures, and can highlight how types are related, where sharing occurs, 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 combining 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.
15:00‑15:30	Fabrice Bouquet (LIFC - Universite de Franche-Comte) Frederic Dadeau (LIFC - Universite de Franche-Comte) Julien Groslambert (LIFC - Universite de Franche-Comte) Jacques Julliand (LIFC - Universite de Franche-Comte) Safety Property Driven Test Generation from JML Specifications 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.

Break (15:30‑16:00)

Session 9 (16:00‑16:30)

16:00‑16:30

Margus Veanes (Microsoft Research) Pritam Roy (University of California) Colin Campbell (Microsoft Research) Online Testing with Reinforcement Learning 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 1/2 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.

Session 10: Tool Demos (16:30‑17:30)