Abstracts

Quantitative Regular Expressions for Monitoring Cardiac Arrhythmias (Abbas et al.)

Medical devices offer an ideal test-bed for exploring the applications of formal monitoring methods in system design due to their safety-critical nature that demands predictable operation. In this abstract, we demonstrate the usage of Quantitative Regular Expressions (QREs) for programming Arrhythmia Monitoring Algorithms (AMAs), which are algorithms that continuously monitor the heart rhythm and detect when it is fatal. AMAs run on resource-constrained implantable devices used by millions of patients around the world, like Implantable Cardioverter Debrillators (ICDs) and Insertable Loop Recorders (ILRs).

On the Quantitative Semantics of Regular Expressions over Real-Valued Signals, (Bakhirkin et al.)

Signal regular expressions specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this work, we develop their quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Second, we present an algorithm that computes quantitative semantics of every segment of a given piecewise-constant or piecewise-linear signal relative to an expression. In particular, this shows that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems.

From MITL to timed automata (Ferrère et al.)

Temporal specifications have found their way in the verification activities of cyber-physical systems (CPS), both in academia and industry. Signal Temporal Logic (STL) for instance builds on top of continuous-time temporal logic Metric Interval Temporal Logic (MITL) by adding to it a mild extension in terms of numeric predicates. We present the procedure for translating real-time temporal logic MITL to timed automata. The translation is based on the idea of temporal testers, acausal sequential transducers that allow modular construction of automata from temporal logic specications. We claim that our temporal testers approach improves the understanding of MITL and signicantly simplies the original seminal construction from Alur et al, 1996.

Time-Staging Enhancement of Hybrid System Falsification, (Ernst et al.)

Falsification problem is pursued by an increasing number of researchers for quality assurance of CPS. In this paper, we introduce a heuristic rule that enhances the falsification ability of optimization-based strategy, by searching for the falsifying trace in segments, and using the robustness of earlier segments to guide the search of the next segments. Results demonstrate improvements over other falsification approaches for certain properties.

Falsification of Cyber-Physical Systems with Reinforcement Learning, (Kato et al.)

We propose a novel framework for testing configurable cyber-physical systems over a given specification represented as metric temporal logic formula. Given a system model with configurable properties and a specification, our approach first learns to falsify the model by using reinforcement learning technique under a certain variety of configurations. After the training phase, it is expected that the experienced falsification agent can quickly find an input signal such that the output violates the specification, even though the specific configuration is not known to the agent. Thus we can use this agent again and again when different configurations are investigated for a product family or for trials and errors of configuration design. We performed a preliminary experiment to validate our hypothesis that the reinforcement learning technique can be applied for falsification problems.

Temporal Logic Falsification of Cyber-Physical Systems: An Input-Signal-Space Optimization Approach, (Aerts et al.)

We identify two practical issues in the optimization-based MTL falsification process. Firstly, a fixed time domain of the input-signal space is assumed in this process, which restricts the frequency content of the (generated) input signals. Secondly, the existing process allows for input selection based on a distribution for a single input variable. We address these issues, by firstly, considering multiple time domains for input-signal space. Subsequently, an input-signal-space optimization problem is formally defined and implemented in S-TaLiRo+, an extension of S-TaLiRo (an existing implementation for solving the MTL falsification problem). Secondly, we propose a decoupled scheme that considers the distribution of each input variable independently. The applicability of the proposed solutions are experimentally evaluated on well-known benchmark problems.

Using Valued Booleans to Find Simpler Counterexamples in Random Testing of Cyber-Physical Systems, (Claessen et al.)

In software testing, as in cyber-physical systems testing, test suites are traditionally developed by hand. In this work we consider one framework for putting the computer in charge of the testing instead: constrained random test case generation as supported by the tool QuickCheck. This is implemented by the use of Valued Booleans (VBools). VBools naturally allow for an extension of QuickCheck into cyber-physical systems, which is useful particularly since QuickCheck can perform shrinking of test cases. Shrinking is a technique to make test cases simpler while preserving failure. This work has three main contributions. First, we adapt random testing with QuickCheck to hybrid systems. Second, we define VBools as a way to simplify counterexamples (shrinking) when testing hybrid systems. Finally, we compare random testing and shrinking to existing falsification tools, to illustrate strengths and weaknesses of random testing and the importance of simplifying counterexamples.

Towards Context-Aware Cyber-Physical Systems, (Ivanov et al.)

Due to the complexity of CPS, developing approaches to ensure and verify their safety and security has proven challenging. Standard model-based techniques to verification or anomaly detection cannot be applied because CPS models are rarely known and might often change. In this paper, we provide a discussion on using context as a new class of information that can be used to aid estimation/detection approaches to ensuring the safety and security of modern CPS. These systems typically have access to multiple information sources that cannot be directly related to the system state (e.g., mapping oxygen saturation measurements to the overall blood oxygen content is challenging). At the same time, this information is correlated with the system’s state. Thus, if formalized properly, context can be used in a way similar to standard measurements.

DejaVu: A Monitoring Tool for First-Order Temporal Logic, (Havelund et al.)

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.

MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration, (Waga et al.)

We present a tool MONAA for timed pattern matching. In MONAA , our timed FJS algorithm is implemented. It has the online property (starts monitoring before the entire log of events is given) and enjoys the constant speedup by skipping, typically twice or three times faster than without skipping. MONAA has two interfaces, the command-line interface MONAA and the C++ API libmonaa .

Resilient Control and Safety for Cyber-Physical Systems, (Tiwari et al.)

Many Cyber-Physical Systems (CPSs) are comprised of a multitude of computing entities that can collectively exhibit an emergent behavior. A compelling example of such system is the drone swarm, which are beginning to see increasing application in battlefield surveillance and reconnaissance. The emergent behavior they exhibit is that of flight formation. We demonstrate an MPC-based control algorithm that displays V-formation emergent behavior.

Cyber-Physical Doping Tests, (Biewer et al.)

We are confronted with a growing number of cases where device manufacturers equip their products with embedded software that includes functionalities that are not in the owner’s interest. Examples include customer lock-in strategies in inkjet printers and as a prominent case the diesel emissions scandal in the automotive industry. This software doping phenomenon is turning more widespread as software is embedded in ever more devices of daily use. In this work we present a formal characterization which can distinguish clean and doped reactive programs, based on a contract that is assumed to exist between the end user of a cyber physical device and the manufacturer of the control software embedded therein. We further discuss our current work on combining this characterization with the theory of model-based testing, so as to arrive at a formal basis upon which it will be possible to perform efficient doping tests in practice.

Stimulus Generator for Circuit Model Generation, (Avon et al.)

This work is concerned with the problem of generation of behavioural models for electrical circuits from simulation traces. Model generation can be formulated as a problem of system identification. The models to be generated are parameterized in their nonlinear dynamics. The input signal space of a circuit is often infinite, indeed here we are dealing with input signals represented by continuous functions over continuous time. It is therefore important to determine the stimuli in order to obtain a good coverage of the circuit behaviours. To this end, we first propose a measure for coverage of stimulus signal space and methods to generate a set of stimulus signals with a desired coverage. The stimulus signals should be chosen to satisfy some conditions. First, they must be an admissible input signal, that is it belongs to the input function class describing realistic input signals. Using only admissible stimuli is crucial for assuring realistic scenarios.