ABSTRACT. Let us use dynamic tainting to follow the paths of input characters through a program.  We will then see that some input fragments end in some variables, and others in others.  This allows us to decompose the input into individual parts, one per variable, and consequently, to infer the entire structure of the input as a context-free grammar.  In the context of runtime verification, such inferred input grammars have a number of uses.  First, they can be used as test drivers, allowing to cover millions of executions in minutes.  Second, they can serve to derive dynamic invariants, such as pre- or postconditions.  Third, grammars, as well as invariants, can be easily verified dynamically, checking whether inputs and invariants conform to the learned languages.  The AUTOGRAM approach will be demonstrated using examples of real programs and (if time permits) even live coding on stage.

ABSTRACT. We propose a novel passive learning approach TeLEx (temporal logic extractor) to infer signal temporal logic formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. The approach requires two inputs: a set of observed traces and a template signal temporal logic (STL) formula. The unknown parameters in the template include the time-bounds of the temporal operators or the thresholds in the inequality predicates. TeLEx finds the value of the unknown parameters such that the synthesized STL property is satisfied by all the provided traces and it is tight. This requirement of tightness is essential to generating interesting properties when only positive examples are provided. The challenge arises from the absence of negative examples and the inability to actively query the dynamical system in order to discover the boundaries of legal behavior. We propose a novel quantitative semantics for satisfaction of STL properties which enables TeLEx to learn tight STL properties without multidimensional optimization. The proposed new metric is also smooth. This is critical to the use of gradient-based numerical optimization engines and it produces an order of magnitude speed-up with respect to the state-of-art gradient-free optimization. The approach is implemented in a publicly available tool.

ABSTRACT. This paper introduces a new method for clustering time-series signals using their temporal logic properties. Specifically, we propose a hierarchical clustering algorithm for efficiently processing a set of input signals. The input data is unlabeled, that is, no further information about properties of the signals are available to the learning algorithm other than the signals themselves. The algorithm produces a hierarchical structure where the internal nodes test some temporal properties of the data, and each terminal node contains a cluster (i.e., a group of similar signals). Each cluster can be mapped to a Signal Temporal Logic (STL) formula that describes its signals. The obtained formulae can be used directly for monitoring purposes but also, more generally, to acquire knowledge about the system under analysis. We present two case studies to illustrate the characteristics of our proposed algorithm. The first case study is related to a maritime surveillance problem, and the second is a classification problem in an automatic transmission system.

ABSTRACT. Model-checking has a long-standing tradition in software verification. Given a system design it checks whether desired properties are satisfied. Unlike testing, it cannot be applied in a black-box setting. To overcome this limitation Peled et al. introduced black-box checking, a combination of testing, model inference and model checking. The technique requires systems to be fully deterministic. For stochastic systems, statistical techniques are available. However, they cannot be applied to systems with non-deterministic choices. We present a black-box checking technique for stochastic systems that allows both, non-deterministic and probabilistic behaviour. It involves model inference, testing and probabilistic model-checking. Here, we consider reachability checking, i.e., we infer near-optimal input-selection strategies for bounded reachability.

ABSTRACT. We investigate the runtime verification problem of hyperproperties, such as non-interference and observational determinism, given as formulas of the temporal logic HyperLTL. HyperLTL extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. We show that deciding whether a HyperLTL formula is monitorable is PSPACE-complete. For monitorable specifications, we present an efficient monitoring approach. As hyperproperties relate multiple computation traces with each other, it is necessary to store previously seen traces, and to relate new traces to the traces seen so far. If done naively, this causes the monitor to become slower and slower, before it inevitably runs out of memory. In this paper, we present techniques that reduce the set of traces that new traces must be compared against to a minimal subset. Additionally, we exploit properties of specifications such as reflexivity, symmetry, and transitivity, to reduce the number of comparisons. We show that this leads to much more scalable monitoring with, in particular, significantly lower memory consumption.

ABSTRACT. Run-time checking of timed properties requires to monitor events occurring within a specified time interval. In a distributed setting, working with intervals is complicated due to uncertainties about network delays and clock synchronization. Determining that an interval can be closed -- i.e., that all events occurring within the interval have been observed -- cannot be done without a delay. In this paper, we consider how an appropriate delay can be determined based on parameters of a monitoring setup, such as network delay, clock skew and clock rate. We then propose a generic scheme for monitoring time intervals, parameterized by the detection delay, and discuss the use of this monitoring scheme to check different timed specifications, including real-time temporal logics and rate calculations.

ABSTRACT. Linear temporal logic (LTL) and its quantitative extension metric temporal logic (MTL) are standard languages for specifying system behaviors. Regular expressions are an even more expressive formalism in the non-metric setting and several extensions of LTL, including the recently proposed linear dynamic logic (LDL), offer regular-expression-like constructs. We extend LDL with past operators and quantitative features. The resulting metric dynamic logic (MDL) offers the quantitative temporal conveniences of MTL while increasing its expressiveness. We develop and evaluate an online monitoring algorithm for MDL whose space-consumption is almost event-rate independent---a notion that characterizes monitors that scale to high-velocity event streams.