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.

Software Defined Vehicles (SDVs) represent a paradigm shift in the automotive industry, where vehicles are increasingly controlled and managed through software, while relying less on mechanical and hardware components. While this allows considerable flexibility in the introduction of new “smart” features and fast tracks innovations in multiple domains, it also creates new challenges and opportunities in architecture design, control, and security. By adopting modular architectures, adaptive control strategies, and robust security measures, SDVs can pave the way for a safer and more efficient future of transportation. In this paper, we cover perspectives from both, industry and academia, in this area. They provide embedded systems researchers an overview of recent developments and emerging challenges in SDV from the perspective of architecture design, control, and security. The emerging challenges also set the foundations for future research in this domain.

In this paper, we perform a safety and performance analysis of an autonomous vehicle utilizing a reactive planner and controller to navigate a race lap. Unlike traditional planning algorithms that use a map of the environment, the reactive planner generates the plan based solely on current sensor inputs. Our reactive planner selects a waypoint on the local Voronoi diagram, and we use a pure-pursuit controller to navigate towards this waypoint.Our analysis consists of two parts. The first part demonstrates that the reactive planner computes a plan locally consistent with the Voronoi plan derived from a full map. The second part models the vehicle’s navigation along the Voronoi diagram as a hybrid automaton. To prove the safety and performance specifications, we compute the reachable set of this hybrid automaton and apply enhancements to simplify this computation. We show that an autonomous vehicle using our reactive planner and controller is safe and successfully completes a lap on five different circuits. Additionally, we have implemented our planner and controller in a simulation environment and on a scaled-down autonomous vehicle, demonstrating that our approach works well across a variety of circuits.

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.

We propose a new technique for performing state-space exploration of closed-loop control systems with neural network feedback controllers. Our approach involves approximating the sensitivity of the trajectories of the closed-loop dynamics. Using such an approximator and the system simulator, we present a guided state-space exploration method that can generate trajectories visiting the neighborhood of a target state at a specified time. We present a theoretical framework which establishes that our method will produce a sequence of trajectories that will reach a suitable neighborhood of the target state. We provide a thorough evaluation of our approach on various systems with neural network feedback controllers of different configurations. We outperform earlier state-space exploration techniques and achieve significant improvement in both the quality (explainability) and performance (convergence rate). Finally, we adopt our algorithm for the falsification of a class of temporal logic specification, assess its performance, and show its potential in supplementing existing falsification algorithms.

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.

Feedback control loops are ubiquitous in any autonomous system. The design flow for any controller starts by determining a control strategy, while abstracting away all implementation details. However, when designing controllers for autonomous systems, there is significant computation associated with the perception modules. For example, this involves vision processing using deep neural networks on multicore CPU+accelerator platforms. Such computation can be organized in many different ways, with each choice resulting in very different sensor-to-actuator delays and tradeoffs between cost, delay, and accuracy. Further, each of these choices requires the control strategy to be designed accordingly. It is not possible for a control designer to enumerate and account for all of these choices manually, or abstract them away as “implementation details” as done in traditional controller design. In this paper we outline this problem and discuss how automated controller-synthesis techniques could help in addressing it.

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.

In this paper, we present a 2-step framework for high-precision dense depth perception from stereo RGB images and sparse LiDAR input. In the first step, we train a deep neural network to predict dense depth map from the left image and sparse LiDAR data, in a novel self-supervised manner. Then in the second step, we compute a disparity map from the predicted depths, and refining the disparity map by making sure that for every pixel in the left, its match in the right image, according to the final disparity, is the local optimum.

Computing the set of reachable states is a widely used technique for proving that a hybrid system satisfies its safety specification. Flow-pipe construction methods interleave phases of computing continuous successors and phases of computing discrete successors. Directly doing this leads to a combinatorial explosion problem, though, as with each discrete successor there may be an interval of time where the transition can occur, so that the number of paths becomes exponential in the number of discrete transitions. For this reason, most reachable set computation tools implement some form of set aggregation for discrete transitions, such as, performing a template-based overapproximation or convex hull aggregation. These aggregation methods, however, in theory can lead to unbounded error, and in practice are often the root cause of why a safety specification cannot be proven. This paper proposes techniques for improving the accuracy of the aggregation operations performed for reachable set computation. First, we present two aggregation strategies over generalized stars, namely convex hull aggregation and template based aggregation. Second, we perform adaptive deaggregation using a data structure called Aggregated Directed Acyclic Graph (AGGDAG). Our deaggregation strategy is driven by counterexamples and hence has soundness and relative completeness guarantees. We demonstrate the computational benefits of our approach through two case studies involving satellite rendezvous and gearbox meshing.

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.

Simulations are a practical method of increasing the confidence that a system design is correct. This paper presents techniques which aim to determine all the states that can be reached using a particular hybrid automaton simulation algorithm, a property we call simulation-equivalent reachability. Although this is a slightly weaker property than traditional reachability, its computation can be efficient and accurate. We present HyLAA, the first tool for simulation-equivalent reachability for hybrid automata with affine dynamics. HyLAA's analysis is exact; upon completion, the tool provides a concrete simulation trace to an unsafe state if and only if the hybrid automaton simulation engine could produce such a trace. In the backend, the tool implements an efficient algorithm for continuous post that exploits the superposition principle of linear systems, requiring only n+1 simulations per mode for an n-dimensional linear system. This technique is capable of analyzing a replicated helicopter system with over 1000 state variables in less than 20 minutes. The tool also contains several novel performance enhancements, such as invariant constraint elimination, warm-start linear programming, and trace-guided set deaggregation.

We present Compare-Execute-Check-Engine (C2E2), a tool that implements a simulation based verification algorithm for annotated hybrid systems. The input to C2E2 is an annotated Stateflow model (or an annotated hybrid system in an xml format) with possibly nonlinear ordinary differential equations (ODEs) and a temporal property, which can be either an invariant property or a temporal precedence property. For verification, C2E2 compiles the ODEs using a validated numerical solver, generates simulations, and computes an over-approximation of the set of reachable states. If the over-approximation of the reachable states satisfies (or violates) the temporal property specified, then C2E2 terminates, otherwise it computes a more precise over-approximation and repeats. We would demonstrate the following features of C2E2 (a) the graphical user interface, (b) specifying the safety and temporal precedence properties, and (c) verifying the properties and visualizing the reachable set, which helps in building intuition about the behaviors of the hybrid system.

Deployed embedded software interacts with sensors and actuators to control a physical environment. While the evolution of the control system is specified by Ordinary Differential Equations (ODEs), the embedded software periodically senses the state of the system, performs computation over the inputs, and initiates the actuators based on the result of computation. In this paper, we present a bounded time safety verification technique for periodically actuated linear control systems. The model considered in this paper takes into account that the control tasks are executed on a real time operating system and hence the task, in some instances misses the real time deadlines. Using matrix exponentiation, and symbolic evaluation of inputs, we reduce the verification problem of such systems into software verification with computation over reals. We compare different techniques for verifying such software, highlight the merits of each of the approaches, and present our experimental results.

Simulations can help enhance confidence in system designs but they provide almost no formal guarantees. In this paper, we present a simulation-based verification framework for embedded systems described by non-linear, switched systems. In our framework, users are required to annotate the dynamics in each control mode of switched system by something we call a discrepancy function that formally measures the nature of trajectory convergence/divergence of the system. Discrepancy functions generalize other measures of trajectory convergence and divergence like Contraction Metrics and Incremental Lyapunov functions. Exploiting such annotations, we present a sound and relatively complete verification procedure for robustly safe/unsafe systems. We have built a tool based on the framework that is integrated into the popular Simulink/Stateflow modeling environment. Experiments with our prototype tool shows that the approach (a) outperforms other verification tools on standard linear and non-linear benchmarks, (b) scales reasonably to larger dimensional systems and to longer time horizons, and (c) applies to models with diverging trajectories and unknown parameters.

An embedded software controller is safe if the composition of the controller and the plant does not reach any unsafe state starting from legal initial states (in an unbounded time horizon). Linear systems - specified using linear ordinary differential or difference equations - form an important class of models for such control systems. We present a new decidability result for safety verification of linear systems. Our decidability result assumes that the set of initial states and the set of unsafe states satisfy some conditions. When the set of initial and unsafe states do not satisfy these conditions, they can be overapproximated by sets that do satisfy the conditions. We thus get a counterexample guided abstraction refinement (CEGAR) procedure for the unconstrained safety verification of linear systems. Our new procedure performs abstraction-refinement on the initial and unsafe region, and not on the system itself. We present the new procedure and describe experimental results that demonstrate its effectiveness.

A set of states S is said to be inevitable for a hybrid automaton A if every behavior of A ultimately reaches S within bounded time. Inevitability captures various commonly occurring liveness properties. In this paper, we present an algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function-based relational abstractions for the continuous dynamics with (b) automated construction of well-founded relations for the loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with respect to the chosen Lyapunov functions. The algorithm is implemented in a prototype tool (LySHA) which is integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness of the methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty locations.

This paper presents an algorithm for checking global predicates from distributed traces of cyber-physical systems. For an individual agent, such as a mobile phone or a robot, a trace is a finite sequence of state observations and message histories. Each observation has a possibly inaccurate timestamp from the agent's local clock. The challenge is to symbolically over approximate the reachable states of the entire system from the unsynchronized traces of the individual agents. The presented algorithm first approximates the time of occurrence of each event, based on the synchronization errors of the local clocks, and then over approximates the reach sets of the continuous variables between consecutive observations. The algorithm is shown to be sound, it is also complete for a class of agents with restricted continuous dynamics and when the traces have precise information about timing synchronization inaccuracies. The algorithm is implemented in an SMT solver-based tool for analyzing distributed Android apps. Experimental results illustrate that interesting properties like safe separation, correct geocast delivery, and distributed deadlocks can be checked for up-to twenty agents in minutes.