We study the problem where an autonomous system is in a critical situation and is faced with multiple options among which it has to choose to safely evade the criticality. Each of these options is also associated with some uncertainty. Traditional approaches from formal methods require a reachability analysis to evaluate which of the options is safe. While the computational cost of reachability analysis is well known, the presence of uncertainty adds an additional layer of complexity. As a result, performing reachability analysis for all the options before choosing one will not be feasible due to time constraints. This is a practical problem that arises is various scenarios, such as an autonomous vehicle in a potential accident that it has to evade to minimize damage. While models and algorithms for reachability analysis have been widely studied, reachability analysis in the presence of uncertainties have been less so. Despite its many applications, to the best of our knowledge, the problem of choosing in real-time, one of the many options for criticality evasion has not been studied in the past. We address this problem by proposing a new real-time reachable set computation technique for uncertain linear systems using techniques from perturbation theory.

Real-time scheduling of multiple control tasks in a weakly hard setting is an emerging research direction, as it offers a more flexible and feasible environment for task scheduling. This is especially pertinent for resource-constrained embedded applications where tasks are allowed to miss a few deadlines for prudent sharing of computational resources. However, a control task missing its deadline could result in the system being unsafe or unstable. A significant amount of research efforts have been reported in the literature addressing the schedulability of control tasks while preserving the stability or safety. However, all of them focus on a stable schedule or a safe schedule, but not both the safety and stability aspects together. In this work, we ensure both control stability and control safety to generate a safe and stable schedule for a weakly hard task system. In particular, we gradually endorse stability, safety, and schedulability, where we first synthesize a weakly hard constraint that preserves the desired stability of each control task. Next, we correlate stability with control safety and establish some mathematical results that guarantee control safety for an unbounded time horizon, unlike the existing methods. Finally, by leveraging Satisfiability Modulo Theories (SMT) , we synthesize the schedule that ensures control stability and safety while minimizing the worst-case response time of all the tasks, in a time-efficient way. To our knowledge, this is the first work to address stability, safety, and schedulability together for weakly hard control task systems. We validate our method through extensive experiments using standard automotive benchmarks. In addition, we demonstrate the efficiency of the proposed method in comparison with some of the state-of-the-art techniques, as well as highlight its scalability, thereby establishing its applicability in real-world scenarios.

Autonomous Underwater Vehicles (AUVs) play a crucial role in applications such as deep-sea exploration and military operations. However, variations in temperature, salinity, and depth affect the speed of sound, leading to communication delays and signal degradation. These environmental factors in-troduce uncertainties that complicate effective communication and may increase energy consumption as AUV s sometimes need to expend additional power to maintain connectivity due to the position drift.

Monitoring the correctness of distributed cyber-physical systems is essential. Detecting possible safety violations can be hard when some samples are uncertain or missing. We monitor here black-box cyber-physical system, with logs being uncertain both in the state and timestamp dimensions: that is, not only the logged value is known with some uncertainty, but the time at which the log was made is uncertain too. In addition, we make use of an over-approximated yet expressive model, given by a non-linear extension of dynamical systems. Given an offline log, our approach is able to monitor the log against safety specifications with a limited number of false alarms. As a second contribution, we show that our approach can be used online to minimize the number of sample triggers, with the aim at energetic efficiency. We apply our approach to three benchmarks, an anesthesia model, an adaptive cruise controller and an aircraft orbiting system.

With the emergence of complex autonomous systems, multiple control tasks are increasingly being implemented on shared computational platforms. Due to the resource-constrained nature of such platforms in domains such as automotive, scheduling all the control tasks in a timely manner is often difficult. The usual requirement---that all task invocations must meet their deadlines---stems from the isolated design of a control strategy and its implementation (including scheduling) in software. This separation of concerns, where the control designer sets the deadlines, and the embedded software engineer aims to meet them, eases the design and verification process. However, it is not flexible and is overly conservative. In this paper, we show how to capture the deadline miss patterns under which the safety properties of the controllers will still be satisfied. The allowed patterns of such deadline misses may be captured using what are referred to as "weakly-hard constraints." But scheduling tasks under these weakly-hard constraints is non-trivial since common scheduling policies like fixed-priority or earliest deadline first do not satisfy them in general. The main contribution of this paper is to automatically synthesize schedules from the safety properties of controllers. Using real examples, we demonstrate the effectiveness of this strategy and illustrate that traditional notions of schedulability, e.g., utility ratios, are not applicable when scheduling controllers to satisfy safety properties.

A crucial requirement for control tasks in safety-critical systems like automotive is that all deadlines be met. This is becoming increasingly difficult when several tasks share common resources. One main reason for this lies in obtaining tight WCET estimations, especially as software and processor architectures continue to become more complex. Using safe but not necessarily tight WCET estimates and meeting all deadlines come at the expense of very pessimistic and inefficient implementations. In this paper, we show that by focusing on “higher-level” properties like control safety, instead of trying to meet all deadlines, it is possible to achieve more efficient implementations of control tasks on shared resources. This has considerable benefits in cost-sensitive domains like automotive. The core of our technique follows the AUTOSAR paradigm where groups of control computations with the same period constitute units of scheduling. Towards this, we suitably increase (boost) or decrease (compress) the sampling periods of control tasks and schedule them in a manner that is cognizant of their high-level safety constraints, but does not necessarily meet all deadlines. Our results for several standard controllers from the automotive domain illustrate the benefits of our approach.

Software in autonomous systems, owing to performance requirements, is deployed on heterogeneous hardware comprising task specific accelerators, graphical processing units, and multicore processors. But performing timing analysis for safety critical control software tasks with such heterogeneous hardware is becoming increasingly challenging. Consequently, a number of recent papers have addressed the problem of stability analysis of feedback control loops in the presence of timing uncertainties (cf., deadline misses). In this paper, we address a different class of safety properties, viz., whether the system trajectory deviates too much from the nominal trajectory, with the latter computed for the ideal timing behavior. Verifying such quantitative safety properties involves performing a reachability analysis that is computationally intractable, or is too conservative. To alleviate these problems we propose to provide statistical guarantees over behavior of control systems with timing uncertainties. More specifically, we present a Bayesian hypothesis testing method based on Jeffreys’s Bayes factor test that estimates deviations from a nominal or ideal behavior. We show that our analysis can provide, with high confidence, tighter estimates of the deviation from nominal behavior than using known reachability based methods. We also illustrate the scalability of our techniques by obtaining bounds in cases where reachability analysis fails to converge, thereby establishing the former’s practicality.

As embedded systems architectures become more complex and distributed, checking the safety of feedback control loops implemented on them becomes a crucial problem for emerging autonomous systems. Toward this, a number of recent papers have addressed the problem of checking stability in the presence of deadline misses. In this article, we argue that analyzing quantitative properties like the maximum deviation in system behavior (trajectory in the state space) between an ideal implementation platform and that having timing uncertainties is an equally important problem. We show that different strategies for handling deadline misses (or system overruns), all of which lead to a stable system, might differ considerably when considering such quantitative safety properties. However, analyzing such properties involves reachability analysis that is computationally expensive and, hence, not scalable. We show that suitable approximation strategies can address this computational bottleneck and such quantitative safety properties can be checked for realistic systems. As a result, we are able to identify best combinations of control and deadline miss handling strategies for individual systems and timing uncertainties.

A robot can invoke heterogeneous computation resources such as CPUs, cloud GPU servers, or even human computation for achieving a high-level goal. The problem of invoking an appropriate computation model so that it will successfully complete a task while keeping its compute and energy costs within a budget is called a model selection problem. In this paper, we present an optimal solution to the model selection problem with two compute models, the first being fast but less accurate, and the second being slow but more accurate. The main insight behind our solution is that a robot should invoke the slower compute model only when the benefits from the gain in accuracy outweigh the computational costs. We show that such cost-benefit analysis can be performed by leveraging the statistical correlation between the accuracy of fast and slow compute models. We demonstrate the broad applicability of our approach to diverse problems such as perception using neural networks and safe navigation of a simulated Mars rover.

Reachable set computation is one of the primary techniques for safety verification of linear dynamical systems. In reality the underlying dynamics have uncertainties like parameter variations or modeling uncertainties. Therefore, the reachable set computation must consider the uncertainties in the dynamics to be useful i.e . the computed reachable set should be over or under approximation if not exact. This paper presents a technique to compute reachable set of linear dynamical systems with uncertainties. First, we introduce a construct called support of a matrix. Using this construct, we present a set of sufficient conditions for which reachable set for uncertain linear system can be computed efficiently; and safety verification can be performed using bi-linear programming. Finally, given a linear dynamical system, we compute robust reachable set, which accounts for all possible uncertainties that can be handled by the sufficient conditions presented. Experimental evaluation on benchmarks reveal that our algorithm is computationally very efficient.