ABSTRACT. Using Artificial Intelligence (AI) in machine learning can modify many safety-critical applications, such as automotive and healthcare applications. The maturity of these technologies has reached a point where they are now clearly offering benefits through various safety applications. Unfortunately, the use of learning-enabled components that do not guarantee trust can lead to dramatic situations. Rigorous design and trust are imperative for AI’s widespread adoption and, thus, overall success. Establishing trust, however, is a complex process. Several constituent elements of trust cover all the dimensions of an AI system. In this presentation, I will focus on three essential questions. These are: 1- Is AI in mission-critical systems hype, or is it something sustainable? 2- What is the difference between pure software engineering and learning-enabled systems, especially mission-critical ones? 3- How can we ensure the trustworthiness of these critical systems with learning-enabled components? I'll devote a good part of my presentation to this last question, particularly to the problem of runtime monitoring of learning-enabled components.

ABSTRACT. Runtime verification (RV) allows monitoring the executions of a system while checking them against a formal specification, often written using temporal logic. While RV allows checking the actual executions of a system, a major constraint is that when applied online, it is expected that a verdict about the compatibility of the current execution and the specification is provided based on a the (finite) prefix observed so far. The ability to decide on such a verdict is called monitorability.

ABSTRACT. We present a method for mining parameters of temporal specifications for signal classification. Given a parametric formula and a set of labeled traces, we find one parameter valuation for each class and use it to instantiate the specification template. The resulting formula characterizes the signals in a class by discriminating them from signals of other classes. We propose a two-step approach: first, for each class, we approximate its validity domain, which is the region of the valuations that render the formula satisfied. Second, we select from each validity domain the valuation that maximizes the distance from the validity domain of other classes. We provide a statistical guarantee that the selected parameter valuation is at a bounded distance from being optimal. Finally, we validate our approach on three case studies from different application domains.

ABSTRACT. We investigate the role of ensemble methods in learning runtime monitors for the operational design domains of autonomous systems. An operational design domain (ODD) of a system captures the conditions under which we can trust the components of the system to maintain its safety. A runtime monitor of an ODD predicts based on a sequence of monitorable observations whether the system is about to exit the ODD. For black-box systems, a key challenge in learning an ODD monitor is obtaining a monitor with a high degree of accuracy. While statistical theories such as the theory of probably approximate learning (PAC) allow us to provide guarantees on the accuracy of a learned ODD monitor up to a certain confidence probability (by setting a bound on the number of needed training data), practically, there will always remain a chance, that using such a one-shot approach will result in monitor with a high misclassification rate. To address this challenge we consider well-known ensemble learning algorithms and utilize them for learning ODD ensembles. We derive theoretical bounds on the estimated misclassification risk of ensembles and show that this is monotonically decreasing with growing ODD ensembles. To demonstrate the advantage of ensemble methods, we evaluate the impact of the different ensemble learning methods using a case study from the domain of autonomous driving.

ABSTRACT. We introduce Spatial Regular Expressions (SpREs) as a novel querying language for pattern matching over perception streams containing spatial and temporal data. To highlight the capabilities of SpREs, we developed the STREM tool as a matching framework that works in both the offline and online domain. We demonstrate the tool through an offline example with an AV dataset, an online example through an integration with the ROS and CARLA simulators, and an initial set of performance benchmarks on various SpRE queries. From our designed matching framework, we are able to find over 20,000 matches within 296 ms making it highly usable in runtime monitoring applications.

ABSTRACT. In the domain of video delivery, industrial software systems that produce multimedia streams are increasingly more complex. To ensure correctness of their behaviors, there is a strong need for verification and validation activities. In particular, formal verification seems a promising approach for that. However, applying formal verification on industrial legacy systems is challenging. Their intrinsic complexity, their interactions, and the complexity of video standards that are constantly evolving make the task difficult. To face these issues, this paper presents the ATEME Monitoring Tool (AMT), a runtime verification tool used to monitor formal properties on output streams of video delivery systems. This tool can be used all along the product life cycle to make syntactic and semantic verification when analyzing bugs (on live streams or on captures), developing new features, and doing non-regression checks. Using the tool, we have successfully found and/or reproduce real issues violating requirements of software systems delivering over-the-top (OTT) streams.

ABSTRACT. Video capturing devices with limited storage capacity have become increasingly common in recent years. As a result, there is a growing demand for techniques that can effectively analyze and understand these videos. While existing approaches based on data-driven methods have shown promise, they are often constrained by the availability of training data. In this paper, we focus on dashboard camera videos and propose a novel technique for recognizing important events, detecting traffic accidents, and trimming accident video evidence based on anomaly detection results. By leveraging meaningful high-level time-series abstraction and logical reasoning methods with state-of-the-art data-driven techniques, we aim to pinpoint critical evidence of traffic accidents in driving videos captured under various traffic conditions with promising accuracy, continuity, and integrity. Our approach highlights the importance of utilizing a formal system of logic specifications to deduce the relational features extracted from a sequence of video frames and meets the practical limitations of real-time deployment.

ABSTRACT. Pedestrian detection is an important part of the perception system of autonomous vehicles. Foggy and low-light conditions are quite challenging for pedestrian detection, and several models have been proposed to increase the robustness of detections under such challenging conditions. Checking if such a model performs well is largely evaluated by manually inspecting the results of object detection. We propose a monitoring technique that uses Timed Quality Temporal Logic (TQTL) to do differential testing: we first check when an object detector (such as vanilla YOLO) fails to accurately detect pedestrians using a suitable TQTL formula on a sequence of images. We then apply a model specialized to adverse weather conditions to perform object detection on the same image sequence. We use Image-Adaptive YOLO (IA-YOLO) for this purpose. We then check if the new model satisfies the previously failing specifications. Our method shows that such a differential testing approach can be used to check the robustness of specialized models used for image processing.