Search

Runtime verification is aimed at analyzing execution traces stemming from a running program or system. The traditional purpose is to detect the lack of conformance with respect to a formal specification. Numerous efforts in the field have focused on monitoring parametric specifications, where events carry data, and formulas can refer to such. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of Boolean operators, quantification, and lookup of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this work we explore the use of binary decision diagrams for representing observed data. Our experiments show a substantial improvement in performance compared to related work.

We study the synthesis of control for a system that interacts with a black-box environment, based on deep learning. The goal is to minimize the number of interaction failures. The current state of the environment is unavailable to the controller, hence its operation depends on a limited view of the history. We suggest a reinforcement learning framework of training a Recurrent Neural Network (RNN) to control such a system. We experiment with various parameters: loss function, exploration/exploitation ratio, and size of lookahead. We designed examples that capture various potential control difficulties. We present experiments performed with the toolkit DyNet.

A BDD (Boolean Decision Diagram) is a data structure for the compact representation of a Boolean function. It is equipped with efficient algorithms for minimization and for applying Boolean operators. The use of BDDs for representing Boolean functions, combined with symbolic algorithms, facilitated a leap in the capability of model checking for the verification of systems with a huge number of states. Recently BDDs were considered as an efficient representation of data for Runtime Verification (RV). We review here the basic theory of BDDs and summarize their use in model checking and specifically in runtime verification.

Runtime verification is the topic of analyzing execution traces using formal techniques. It includes monitoring the execution of a system against temporal properties, commonly to detect violations. Not every temporal property is fully monitorable however: in some cases, the correctness of the execution does not depend on any finite prefix. We study the connection between monitorability and Lamport’s classification of properties to safety and liveness and their dual classes. We refine the definition of monitorability and provide algorithms to check which verdicts can be expected, a priori and during runtime verification.

Runtime Verification (RV) consists of analyzing execution traces using formal techniques, e.g., monitoring executions against Linear Temporal Logic (LTL) properties. Propositional LTL is, however, limited in expressiveness, as first shown by Wolper [32]. Several extensions to propositional LTL, which promote the expressive power to that of regular expressions, have therefore been proposed; however, none of which was, by and large, adopted for RV. In addition, for many practical cases, there is a need in RV to monitor properties that carry data. This problem has been addressed by numerous authors, and in previous work we addressed this by providing an algorithm that uses BDDs to represent relations over data elements. We show expressiveness deficiencies of first-order LTL and suggest an extension of (propositional as well as first-order) LTL with rules to address these limitations. We describe how the DejaVu tool is correspondingly extended and provide some experimental results.

Safety-critical systems need to maintain their functionality in the presence of multiple errors caused by component failures or disastrous environment events. We propose a game-theoretic foundation for synthesizing control strategies that maximize the resilience of a software system in defense against a realistic error model. The new control objective of such a game is called $k$ -resilience. In order to be $k$ -resilient, a system needs to rapidly recover from infinitely many waves of a small number of up to $k$ close errors provided that the blocks of up to $k$ errors are separated by short time intervals, which can be used by the system to recover. We first argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We then show how the analysis of $k$ -resilience problems can be formulated as a model-checking problem of a mild extension to the alternating-time $\mu$ -calculus (AMC). The witness for $k$ resilience, which can be provided by the model checker, can be used for providing control strategies that are optimal with respect to resilience. We show that the computational complexity of constructing such optimal control strategies is low and demonstrate the feasibility of our approach through an implementation and experimental results.

The use of genetic programming, in combination of model checking and testing, provides a powerful way to synthesize programs. Whereas classical algorithmic synthesis provides alarming high complexity and undecidability results, the genetic approach provides a surprisingly successful heuristics. We describe several versions of a method for synthesizing sequential and concurrent systems. To cope with the constraints of model checking and of theorem proving, we combine such exhaustive verification methods with testing. We show several examples where we used our approach to synthesize, improve and correct code.

In this paper, we describe our monitoring tool, DejaVu, which implements our algorithm for monitoring first-order past linear-time temporal logic over a sequence of events that carry data. We propose the use of Binary Decision Diagrams (BDDs) for representing and manipulating sets of observed data since (1) BDDs provide highly compact representations, (2) operations overBDDs, in particular complementation, are very efficient, and (3) the monitor construction for the propositional case shown in naturally extends to BDDs. Our experiments show a substantial improvement in performance compared to a related tool.

Synthesis of control for distributed systems is considered to be undecidable problem, under the assumption that control is performed by supervisors syncrhonizing with the original processes and selectively blocking or supporting the enabled transitions. We describe a decidable distributed control problem, where additional communications are allowed between supervisors. In this way, we synthesize control for invariants, reachability, repeated reachability and parity conditions. Special attention is given to reducing the number of added communications.

Randomized testing is a lightweight approach for searching for bugs. It presents a tradeoff between the number of testing experiments performed and the probability to find errors. An important challenge in random testing is when the errors that we try to detect are scattered with very low probability among the different executions, forming a “rare event”. We suggest here the use of a “biasing automaton”, which observes the tested sequence and controls the distribution of the different choices of extending it. By the careful selection of a biasing automaton, we can increase the chance of errors to be found and consequently reduce the number of tests we need to perform. The biasing automaton is constructed through repeated testing of variants of the system under test. We show how to construct biasing automata based on genetic programming.