ABSTRACT. In this talk, we present a novel platform for online monitoring of multicore. It gives insight to the system’s behavior without affecting it. This insight is crucial to detect non-deterministic failures as for example caused by race conditions and access to inconsistent data. A system-on-chip is observed using the tracing capabilities available on many modern multi-core processors. They provide highly compressed tracing information over a separate tracing port. From this information our system reconstructs the sequence of instructions executed by the processor, which can then be analyzed online by a reconfigurable monitoring unit. Analyses are described in a high-level temporal stream-based specification language, called TESSLA, that are compiled to configurations of the monitoring unit. To cope with the amount of tracing data generated by modern processors the our system is implemented in hardware using an FPGA. The work presented is carried out within the COEMS project and has re­ceived funding from the Euro­pean Union’s Hori­zon 2020 research and innovation pro­gram under grant agreement no. 732016.

ABSTRACT. The online evaluation of real-time data streams is a ubiquitous part of modern IT systems. Applications range from collecting statistics on data-driven platforms to monitoring safety-critical real-time systems. We present RTLola, a specification and monitoring framework for stream-based real-time properties. RTLola’s stream processing engine translates input streams, which contain sensor readings and other data collected at runtime, into output streams, which contain aggregated statistics. This setup has the advantage of great expressiveness and easy-to-reuse, compositional specifications. A major challenge in monitoring real-time data is to build stable and efficient stream processing engines. A monitor that consumes an unbounded amount of memory is bound to eventually disrupt the normal operation of the system. In real-time applications, data arrives at varying rates that are usually hard to predict. A key feature of RTLola is that it computes guaranteed bounds on the memory based on the desired output rates, which are usually known in advance. We illustrate the use of RTLola with a series of case studies from a wide range of real-time systems, including networks and unmanned aerial systems.

ABSTRACT. In this talk, I will present 1) a framework to systematically analyze convolutional neural networks and 2) a counterexample-guided data augmentation scheme. The analysis procedure comprises a falsification framework in the system-level context. The falsifier is based on an image generator that produces synthetic pictures by sampling in a lower dimension image modification subspace. The generated images are used to test the CNN and expose its vulnerabilities. The misclassified pictures (counterexamples) are then used to augment the original training set and hence improve the accuracy of the considered model. The talk focuses on case studies of object detection in autonomous driving based on deep learning.

ABSTRACT. Cyber-physical systems (CPSs) are used in many mission critical applications, such as automobiles, aircraft, and medical devices; therefore, it is vital to ensure that these systems behave correctly. Testing is required to ensure correct behavior for CPSs, but traditional methods to evaluate test data can be time consuming and unreliable. New technologies, such as property monitoring, can automatically evaluate measurements of system behaviors against requirements; however, most property monitoring methods rely on the availability of formal system requirements, often in the form of temporal logic formulae, which can be challenging to develop for complex applications. This talk describes industrial CPS challenges in defining formal requirements, presents examples from testing results for an automotive fuel cell application, and suggests possible directions for solutions.

ABSTRACT. In recent years, there has been a great interest in applying formal methods to the field of machine learning (ML). In this talk, I will discuss inferring high-level descriptions of a system from its execution signals. The system behaviors are formalized using a temporal logic language called Signal Temporal Logic (STL). I will first focus on supervised, off-line classification. Given a set of pairs of signals and labels, where each label indicates whether the respective signal exhibits some system property, a decision-tree algorithm outputs an STL formula which can distinguish the signals. I will then show how this method can be extended to the online learning scenario. In this setting, it is assumed that new signals may arrive over time and the previously inferred formula should be updated to accommodate the new data. Finally, I will focus on the (unsupervised) clustering problem. In this case, it is assumed that only a set of unlabeled signals is available, that is, it is not known a priori if a signal exhibits a specific behavior or satisfies some property, and the end goal is to group similar signals together, in so-called clusters, and to describe each cluster with a formula.

ABSTRACT. We propose to introduce first order quantifiers in Signal Temporal Logic. Our definitions enable to describe many properties of interest, such as the stabilization of a signal around an undetermined threshold, otherwise not expressible. A monitoring algorithm is described for the one-variable fragment of this new logic, based on a geometric representation of validity domains.

ABSTRACT. Monitor synthesis from high-level specifications provides a fast and convenient way of developing monitoring code with guarantees on monitoring complexity. It remains important to test the generated code on a realistic setup, that closely mimics the final deployment environment. In this talk we will describe the F1/10 Autonomous Racing Platform, and its associated simulator, as an environment for developing and testing auto-generated monitoring code for robotic applications. F1/10 is a fully open-source project for creating a 1/10th scale autonomous race car, and its associated simulator allows easy and risk-free testing of navigation and monitoring algorithms. The platform allows developers to run their monitors on the deployment hardware, inside a deployment software stack based on ROS, which means that the code can be deployed as-is on the car. This tutorial-style talk will also demonstrate how to setup the simulator and we will synthesize ROS-based monitors using the Reelay tool. We will also describe plans for creating hardware-as-a-service for testing algorithms targeting autonomous driving.