We study localization and control problems in which agent dynamics are described by difference or differential equations, while output measurements are collected at discrete times and given by finite-valued maps depending on possibly unknown landmark locations. Guided by the goal of understanding fundamental limitations imposed by such coarse measurements, we focus on characterizing indistinguishable states, i.e., agent-landmark pairs that produce identical observations under all control inputs. We show that indis-tinguishability relations can be checked automatically under mild assumptions and, being a special type of bisimulation, we develop an iterative algorithm for approximately computing them. We then introduce an analytical approach, rooted in observability theory of linear control systems, which iteratively computes a sequence of subspaces converging in finitely many steps to the indistinguishable subspace; a differential-geometric extension to nonlinear systems is also outlined.

We present a novel framework demonstrating zero-shot sim-to-real transfer of visual control policies learned in a Neural Radiance Field (NeRF) environment for quadrotors to fly through racing gates. Robust transfer from simulation to real flight poses a major challenge, as standard simulators often lack sufficient visual fidelity. To address this, we construct a photorealistic simulation environment of quadrotor racing tracks, called FalconGym, which provides effectively unlimited synthetic images for training. Within FalconGym, we develop a pipelined approach for crossing gates that combines (i) a Neural Pose Estimator (NPE) coupled with a Kalman filter to reliably infer quadrotor poses from single-frame RGB images and IMU data, and (ii) a self-attention-based multi-modal controller that adaptively integrates visual features and pose estimation. This multi-modal design compensates for perception noise and intermittent gate visibility. We train this controller purely in FalconGym with imitation learning and deploy the resulting policy to real hardware with no additional fine-tuning. Simulation experiments on three distinct tracks (circle, U-turn and figure-8) demonstrate that our controller outperforms a vision-only state-of-the-art baseline in both success rate and gate-crossing accuracy. In 30 live hardware flights spanning three tracks and 120 gates, our controller achieves a 95.8% success rate and an average error of just 10 cm when flying through 38 cm-radius gates.

Using formal methods to evaluate software and hardware enhances system reliability, which is crucial for safety-critical applications such as airplanes and autonomous vehicles. Formal methods are mathematical modeling techniques that can be used to verify the safety of systems. The use of formal methods is limited in industry due to a shortage of trained engineers. Educators in formal methods often report that many students do not see the benefit of formal methods and perceive the involved math as not worth the effort for their future careers as software engineers. This study aims to understand the current state of student beliefs and how using a formal verification tool affects student motivation to learn about formal methods. We used an Expectancy Value Cost Lite survey to measure student motivation. Students completed this survey multiple times while designing algorithms to control vehicles in different scenarios, both with and without a formal verification tool. We found that students in an autonomy class are motivated to use formal methods. Although the findings are not statistically significant, we observed a slight increase in motivation after using the tool. Additionally, using a formal verification tool solely for modeling may contribute to increased motivation. These results suggest that incorporating tools into coursework may be a useful step in motivating more students to study formal methods and enter the workforce with these skills.

Rendering produces 2D images from 3D scene representations, yet how continuous variations in camera pose and scenes influence these images—and, consequently, downstream visual models—remains underexplored. We introduce **abstract rendering**, a framework that computes provable bounds on all images rendered under continuously varying camera poses and scenes. The resulting abstract image, expressed as a set of constraints over the image matrix, enables rigorous uncertainty propagation through downstream neural networks and thereby supports certification of model behavior under realistic 3D semantic perturbations, far beyond traditional pixel-level noise models. Our approach propagates camera pose uncertainty through each rendering step using efficient piecewise linear bounds, including custom abstractions for three rendering-specific operations—matrix inversion, sorting-based aggregation, and cumulative product summation—not supported by standard tools. Our implementation, ABSTRACTRENDER, targets two state-of-the-art photorealistic scene representations—3D Gaussian Splats and Neural Radiance Fields (NeRF)—and scales to complex scenes with up to 1M Gaussians. Our computed abstract images achieve up to 3% over-approximation error compared to sampling results (baseline). Through experiments on classification (ResNet), object detection (YOLO), and pose estimation (GATENet) tasks, we demonstrate that abstract rendering enables formal certification of downstream models under realistic 3D variations—an essential step toward safety-critical vision systems.

Abstract Reachability analysis for dynamical systems typically relies on the system’s Jacobian to bound sensitivity of solutions. This method fails for nonsmooth dynamical systems as the Jacobian becomes undefined at the points where the vector field is non-differentiable. Such models can be hybridized by gluing together several smooth subsystems or modes via transitions, but the accuracy of reachability degrades when reachable sets are propagated across the mode boundaries. We propose an alternative approach based on lexicographic differentiation . Lexicographic differentiation was introduced by Nesterov as a foundation for calculus for nonsmooth functions. Our algorithm computes linear bounds on sets of lexicographic Jacobians, which give bounds on trajectory sensitivities. This avoids hybridization, eliminates mode transition computations, and yields more accurate reachsets. On nonsmooth models, our method improves accuracy on average by 50%, compared to hybrid algorithms. It is also one of the first methods to effectively handle reachability of ReLU neural ODEs.

Engineering safe and trustworthy autonomous systems demand formal methodologies that accommodate statistical models and assumptions. In the first part of this talk, I will present safety verification methods that use reachability analysis. This research explores a spectrum of model assumptions and the corresponding guarantees and utilities. The methods combine simulation data with sensitivity analysis. At one end, complete dynamical models offer strong guarantees, but their utility can be limited. Learning sensitivity from data comes with statistical guarantees, and the algorithms are applicable to real-world scenarios, and still confer the benefits of formal reasoning via composition and abstraction. This flexible approach informs our current work on the Verse framework which aims to make code-level analysis for autonomous multi-agent scenarios accessible to undergraduates in engineering design courses.

Perception modules are integral in many modern autonomous systems, but their accuracy can be subject to the vagaries of the environment. In this paper, we propose a learning-based approach that can automatically characterize the error of a perception module from data and use this for safe control. The proposed approach constructs an inverse perception contract (IPC) which generates a set that contains the ground-truth value that is being estimated by the perception module, with high probability. We apply the proposed approach to study a vision pipeline deployed on a quadcopter. With the proposed approach, we successfully constructed an IPC for the vision pipeline. We then designed a control algorithm that utilizes the learned IPC, with the goal of landing the quadcopter safely on a landing pad. Experiments show that with the learned IPC, the control algorithm safely landed the quadcopter despite the error from the perception module, while the baseline algorithm without using the learned IPC failed to do so.

Modern autonomous vehicle systems (AVS) use complex perception and control components. Developers gradually change these components over the vehicle’s lifecycle, requiring frequent regression testing. Unfortunately, high-fidelity simulations of these complex AVS for evaluating safety are costly, and their complexity hinders the development of precise but less computationally intensive surrogate models.We present GAS, a novel approach for expediting simulation-based safety testing of AVS with complex perception and control components. GAS creates a surrogate of the complete vehicle model (i.e., those with complex perception, control, and dynamics components). The surrogates execute faster than the original models and are used to precisely estimate two key properties: the probability that the AVS will violate safety assertions and the bounds on global sensitivity indices of the AVS.We evaluate GAS on five scenarios involving crop management vehicles, self driving carts, and unmanned aircraft. Each AVS in these scenarios contains a complex perception or control component. We generate surrogates of these vehicles using GAS and check the accuracy of the above properties. Compared to the original simulation, GAS models enable estimating the probability of violating a safety assertion 3.7 times faster on average and analyzing sensitivity 1.4 times faster on average.

No abstract available.

Abstract We present the Verse library with the aim of making hybrid system verification more usable for multi-agent scenarios. In Verse, decision making agents move in a map and interact with each other through sensors. The decision logic for each agent is written in a subset of Python and the continuous dynamics is given by a black-box simulator. Multiple agents can be instantiated, and they can be ported to different maps for creating scenarios. Verse provides functions for simulating and verifying such scenarios using existing reachability analysis algorithms. We illustrate capabilities and use cases of the library with heterogeneous agents, incremental verification, different sensor models, and plug-n-play subroutines for post computations.

We introduce a novel notion of perception contracts to reason about the safety of controllers that interact with an environment using neural perception. Perception contracts capture errors in ground-truth estimations that preserve invariants when systems act upon them. We develop a theory of perception contracts and design symbolic learning algorithms for synthesizing them from a finite set of images. We implement our algorithms and evaluate synthesized perception contracts for two realistic vision-based control systems, a lane tracking system for an electric vehicle and an agricultural robot that follows crop rows. Our evaluation shows that our approach is effective in synthesizing perception contracts and generalizes well when evaluated over test images obtained during runtime monitoring of the systems.

Deep learning (DL) models are becoming effective in solving computer-vision tasks such as semantic segmentation, object tracking, and pose estimation on real-world captured images. Reliability analysis of autonomous systems that use these DL models as part of their perception systems have to account for the performance of these models. Autonomous systems with traditional sensors have tried-and-tested reliability assessment processes with modular design, unit tests, system integration, compositional verification, certification, etc. In contrast, DL perception modules relies on data-driven or learned models. These models do not capture uncertainty and often lack robustness. Also, these models are often updated throughout the lifecycle of the product when new data sets become available. However, the integration of an updated DL-based perception requires a reboot and start afresh of the reliability assessment and operation processes for autonomous systems. In this paper, we discuss three challenges related to specifying, verifying, and operating systems that incorporate DL-based perception. We illustrate these challenges through two concrete and open source examples.

Abstract We present , a tool that uses neural networks for predicting reachable sets from executions of a dynamical system. Unlike existing reachability tools, computes areachability functionthat outputs an accurate over-approximation of the reachable set foranyinitial set in a parameterized family. Such reachability functions are useful for online monitoring, verification, and safe planning. implements empirical risk minimization for learning reachability functions. We discuss the design rationale behind the optimization problem and establish that the computed output is probably approximately correct. Our experimental evaluations over a variety of systems show promise. can learn accurate reachability functions for complex nonlinear systems, including some that are beyond existing methods. From a learned reachability function, arbitrary reachtubes can be computed in milliseconds. is available at https://github.com/sundw2014/NeuReach .

Abstract Tor has millions of daily users seeking privacy while browsing the Internet. It has thousands of relays to route users’ packets while anonymizing their sources and destinations. Users choose relays to forward their traffic according to probability distributions published by the Tor authorities. The authorities generate these probability distributions based on estimates of the capacities of the relays. They compute these estimates based on the bandwidths of probes sent to the relays. These estimates are necessary for better load balancing. Unfortunately, current methods fall short of providing accurate estimates leaving the network underutilized and its capacities unfairly distributed between the users’ paths. We present MLEFlow, a maximum likelihood approach for estimating relay capacities for optimal load balancing in Tor. We show that MLEFlow generalizes a version of Tor capacity estimation, TorFlow-P, by making better use of measurement history. We prove that the mean of our estimate converges to a small interval around the actual capacities, while the variance converges to zero. We present two versions of MLEFlow: MLEFlow-CF, a closed-form approximation of the MLE and MLEFlow-Q, a discretization and iterative approximation of the MLE which can account for noisy observations. We demonstrate the practical benefits of MLEFlow by simulating it using a flow-based Python simulator of a full Tor network and packet-based Shadow simulation of a scaled down version. In our simulations MLEFlow provides significantly more accurate estimates, which result in improved user performance, with median download speeds increasing by 30%.

Convolutional Neural Networks (CNN) for object detection, lane detection, and segmentation now sit at the head of most autonomy pipelines, and yet, their safety analysis remains an important challenge. Formal analysis of perception models is fundamentally difficult because their correctness is hard if not impossible to specify. We present a technique for inferring intelligible and safe abstractions for perception models from system-level safety requirements, data, and program analysis of the modules that are downstream from perception. The technique can help tradeoff safety, size, and precision, in creating abstractions and the subsequent verification. We apply the method to two significant case studies based on high-fidelity simulations (a) a vision-based lane keeping controller for an autonomous vehicle and (b) a controller for an agricultural robot. We show how the generated abstractions can be composed with the downstream modules and then the resulting abstract system can be verified using program analysis tools like CBMC. Detailed evaluations of the impacts of size, safety requirements, and the environmental parameters (e.g., lighting, road surface, plant type) on the precision of the generated abstractions suggest that the approach can help guide the search for corner cases and safe operating envelops.

Abstract We present $$\mathsf {SceneChecker}$$ SceneChecker , a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. $$\mathsf {SceneChecker}$$ SceneChecker converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. $$\mathsf {SceneChecker}$$ SceneChecker uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated $$\mathsf {SceneChecker}$$ SceneChecker on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, $$\mathsf {SceneChecker}$$ SceneChecker shows 14 $$\times $$ × average speedup in verification time, even while using those very tools as reachability subroutines.

We address the problem of synthesizing a controller for nonlinear systems with reach-avoid requirements. Our controller consists of a reference controller and a tracking controller which drives the actual trajectory to follow the reference trajectory. We identify a type of reference trajectory such that the tracking error between the actual trajectory of the closed-loop system and the reference trajectory can be bounded. Moreover, such a bound on the tracking error is independent of the reference trajectory. Using such bounds on the tracking error, we propose a method that can find a reference trajectory by solving a satisfiability problem over linear constraints. Our overall algorithm guarantees that the resulting controller can make sure every trajectory from the initial set of the system satisfies the given reach-avoid requirement. We also implement our technique in a tool FACTEST . We show that FACTEST can find controllers for four vehicle models (3–6 dimensional state space and 2–4 dimensional input space) across eight scenarios (with up to 22 obstacles), all with running time at the sub-second range.

Programming languages, libraries, and development tools have transformed the application development processes for mobile computing and machine learning. This paper introduces CyPhyHouse—a toolchain that aims to provide similar programming, debugging, and deployment benefits for distributed mobile robotic applications. Users can develop hardware-agnostic, distributed applications using the high-level, event driven Koord programming language, without requiring expertise in controller design or distributed network protocols. The modular, platform-independent middleware of CyPhyHouse implements these functionalities using standard algorithms for path planning (RRT), control (MPC), mutual exclusion, etc. A high-fidelity, scalable, multi-threaded simulator for Koord applications is developed to simulate the same application code for dozens of heterogeneous agents. The same compiled code can also be deployed on heterogeneous mobile platforms. The effectiveness of CyPhyHouse in improving the design cycles is explicitly illustrated in a robotic testbed through development, simulation, and deployment of a distributed task allocation application on in-house ground and aerial vehicles.

We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map any solution of the system to another solution. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of a virtual system which defines symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of a virtual system, we present a prototype tool CacheReach that builds a cache of reachsets, in a way that is agnostic of the representation of the reachsets and the reachability analysis method used. Our experimental evaluation of CacheReach shows up to 64% savings in safety verification computation time on multi-agent systems with 3-dimensional linear and 4-dimensional nonlinear fixed-wing aircraft models following sequences of waypoints. These savings and our theoretical results illustrate the potential benefits of using symmetry-based caching in the safety verification of multi-agent systems.

A robot’s code needs to sense the environment, control the hardware, and communicate with other robots. Current programming languages do not provide suitable abstractions that are independent of hardware platforms. Currently, developing robot applications requires detailed knowledge of signal processing, control, path planning, network protocols, and various platform-specific details. Further, porting applications across hardware platforms remains tedious. We present Koord—a domain specific language for distributed robotics—which abstracts platform-specific functions for sensing, communication, and low-level control. Koord makes the platform-independent control and coordination code portable and modularly verifiable. Koord raises the level of abstraction in programming by providing distributed shared memory for coordination and port interfaces for sensing and control. We have developed the formal executable semantics of Koord in the K framework. With this symbolic execution engine, we can identify assumptions (proof obligations) needed for gaining high assurance from Koord applications. We illustrate the power of Koord through three applications: formation flight, distributed delivery, and distributed mapping. We also use the three applications to demonstrate how platform-independent proof obligations can be discharged using the Koord Prover while platform-specific proof obligations can be checked by verifying the obligations using physics-based models and hybrid verification tools.

We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Our solution uses a combination of an open-loop controller and a tracking controller, thereby reducing the problem to smaller tractable problems. We show that, once a tracking controller is fixed, the reachable states from an initial neighborhood, subject to any disturbance, can be over-approximated by a sequence of ellipsoids, with sizes that are independent of the open-loop controller. Hence, the open-loop controller can be synthesized independently to meet the reach-avoid specification for an initial neighborhood. Exploiting several techniques for tightening the over-approximations, we reduce the open-loop controller synthesis problem to satisfiability over quantifier-free linear real arithmetic. The overall synthesis algorithm, computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We present RealSyn , a tool implementing this synthesis algorithm, and we show that it scales to several high-dimensional systems with complex reach-avoid specifications. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Automated vulnerability assessment and exploit generation for computing systems have been explored for decades. However, these approaches are incomplete in assessing industrial control systems, where networks of computing devices and physical processes interact for safety-critical missions. We present an attack synthesis algorithm against such cyber-physical electricity grids. The algorithm explores both discrete network configurations and continuous dynamics of the plant's embedded control system to search for attack strategies that evade detection with conventional monitors. The algorithm enabling this exploration is rooted in recent developments in the hybrid system verification research: it effectively approximates the behavior of the system for a set of possible attacks by computing sensitivity of the system's response to variations in the attack parameters. For parts of the attack space, the proposed algorithm can infer whether or not there exists a feasible attack that avoids triggering protection measures such as relays and steady-state monitors. The algorithm can take into account constraints on the attack space such as the power system topology and the set of controllers across the plant that can be compromised without detection. With a proof-of-concept prototype, we demonstrate the synthesis of transient attacks in several typical electricity grids and analyze the robustness of the synthesized attacks to perturbations in the network parameters.

No abstract available.

We present a demo of DryVR 2.0, a framework for verification and controller synthesis of cyber-physical systems composed of black-box simulators and white-box automata. For verification, DryVR 2.0 takes as input a black-box simulator, a white-box transition graph, a time bound and a safety specification. As output it generates over-approximations of the reachable states and returns "Safe" if the system meets the given bounded safety specification, or it returns "Unsafe" with a counter-example. For controller synthesis, DryVR 2.0 takes as input black-box simulator(s) and a reach-avoid specification, and uses RRTs to find a transition graph such that the combined system satisfies the given specification.

Finding the minimal bit rate needed for state estimation of a dynamical system is a fundamental problem in control theory. In this paper, we present a notion of topological entropy, to lower bound the bit rate needed to estimate the state of a nonlinear dynamical system, with unknown bounded inputs, up to a constant error ε. Since the actual value of this entropy is hard to compute in general, we compute an upper bound. We show that as the bound on the input decreases, we recover a previously known bound on estimation entropy - a similar notion of entropy - for nonlinear systems without inputs [10]. For the sake of computing the bound, we present an algorithm that, given sampled and quantized measurements from a trajectory and an input signal up to a time bound T > 0, constructs a function that approximates the trajectory up to an ε error up to time T. We show that this algorithm can also be used for state estimation if the input signal can indeed be sensed in addition to the state. Finally, we present an improved bound on entropy for systems with linear inputs.

Finding the minimal bit rate needed for state estimation of a dynamical system is a fundamental problem in control theory. We present two notions of topological entropy, one to lower bound the bit rate needed to estimate the state of a nonlinear dynamical system, with unknown bounded inputs, up to a constant error ε. The other is to do the same but to estimate the state of a switched system with unknown switching signal up to an error that is bounded by ε for τ seconds after each switch and then decays exponentially at a rate of α till the next switch. Since computation of entropy is hard in general, we present upper bounds on both notions of entropy. Finally, we present preliminary results on the relation between the two notions. Note that most of the ideas presented in this abstract are from our papers [4] and [5].

Simulation-driven verification can provide formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set overapproximations from a set of initial states through numerical simulations and sensitivity analysis. This article addresses this problem by providing algorithms for computing discrepancy functions as the upper bound on the sensitivity, that is, the rate at which trajectories starting from neighboring states converge or diverge. The algorithms rely on computing local bounds on matrix measures as the exponential change rate of the discrepancy function. We present two techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function, and therefore, the conservativeness of the overapproximation, is locally minimized. The proposed algorithms enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy functions give soundness and relative completeness of the overall simulation-driven safety-bounded verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the algorithms.

State estimation is a fundamental problem for monitoring and controlling systems. Engineering systems interconnect sensing and computing devices over a shared bandwidth-limited channels, and therefore, estimation algorithms should strive to use bandwidth optimally. We present a notion of entropy for state estimation of switched nonlinear dynamical systems, an upper bound for it and a state estimation algorithm for the case when the switching signal is unobservable. Our approach relies on the notion of topological entropy and uses techniques from the theory for control under limited information. We show that the average bit rate used is optimal in the sense that, the efficiency gap of the algorithm is within an additive constant of the gap between estimation entropy of the system and its known upper-bound. We apply the algorithm to two system models and discuss the performance implications of the number of tracked modes.

Safety verification of embedded systems modeled as hybrid systems can be scaled up by employing simulation-guided reach set over-approximation techniques. Existing methods are either applicable to only restricted classes of systems, overly conservative, or computationally expensive. We present new techniques to compute a locally optimal bloating factor based on discrepancy functions, which allow construction of reach set over-approximations from simulation traces for general nonlinear systems. The discrepancy functions are critical for tools like C2E2 to verify bounded time safety properties for complex hybrid systems with nonlinear continuous dynamics. The new discrepancy function is computed using local bounds on a matrix measure under an optimal metric such that the exponential change rate of the discrepancy function is minimized. The new technique is less time consuming and less conservative than existing techniques and does not incur significant computational overhead. We demonstrate the effectiveness of our approach by comparing the performance of a prototype implementation with the state-of-the-art reachability analysis tool Flow

We investigate the problem of constructing exponentially converging estimates of the state of a continuous-time system from state measurements transmitted via a limited-data-rate communication channel, so that only quantized and sampled measurements of continuous signals are available to the estimator. Following prior work on topological entropy of dynamical systems, we introduce a notion of estimation entropy which captures this data rate in terms of the number of system trajectories that approximate all other trajectories with desired accuracy. We also propose a novel alternative definition of estimation entropy which uses approximating functions that are not necessarily trajectories of the system. We show that the two entropy notions are actually equivalent. We establish an upper bound for the estimation entropy in terms of the sum of the system's Lipschitz constant and the desired convergence rate, multiplied by the system dimension. We propose an iterative procedure that uses quantized and sampled state measurements to generate state estimates that converge to the true state at the desired exponential rate. The average bit rate utilized by this procedure matches the derived upper bound on the estimation entropy. We also show that no other estimator (based on iterative quantized measurements) can perform the same estimation task with bit rates lower than the estimation entropy. Finally, we develop an application of the estimation procedure in determining, from the quantized state measurements, which of two competing models of a dynamical system is the true model. We show that under a mild assumption of exponential separation of the candidate models, detection is always possible in finite time. Our numerical experiments with randomly generated affine dynamical systems suggest that in practice the algorithm always works.

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.

We developed StarL as a framework for programming, simulating, and verifying distributed systems that interacts with physical processes. StarL framework has (a) a collection of distributed primitives for coordination, such as mutual exclusion, registration and geocast that can be used to build sophisticated applications, (b) theory libraries for verifying StarL applications in the PVS theorem prover, and (c) an execution environment that can be used to deploy the applications on hardware or to execute them in a discrete event simulator. The primitives have (i) abstract, nondeterministic specifications in terms of invariants, and assume-guarantee style progress properties, (ii) implementations in Java/Android that always satisfy the invariants and attempt progress using best effort strategies. The PVS theories specify the invariant and progress properties of the primitives, and have to be appropriately instantiated and composed with the application's state machine to prove properties about the application. We have built two execution environments: one for deploying applications on Android/iRobot Create platform and a second one for simulating large instantiations of the applications in a discrete even simulator. The capabilities are illustrated with a StarL application for vehicle to vehicle coordination in an automatic intersection that uses primitives for point-to-point motion, mutual exclusion, and registration.

We present a modular technique for simulation-based bounded verification for nonlinear dynamical systems. We introduce the notion of input-to-state discrepancy of each subsystem Ai in a larger nonlinear dynamical system A which bounds the distance between two (possibly diverging) trajectories of Ai in terms of their initial states and inputs. Using the IS discrepancy functions, we construct a low dimensional deterministic dynamical system M(δ). For any two trajectories of A starting δ distance apart, we show that one of them bloated by a factor determined by the trajectory of M contains the other. Further, by choosing appropriately small δ's the overapproximations computed by the above method can be made arbitrarily precise. Using the above results we develop a sound and relatively complete algorithm for bounded safety verification of nonlinear ODEs. Our preliminary experiments with a prototype implementation of the algorithm show that the approach can be effective for verification of nonlinear models.

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.

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 which uses simulation traces and formal models for computing overapproximations of reach sets of deterministic hybrid systems. The implementation of the algorithm in a tool, Hybrid Trace Verifier (HTV), uses Mathwork's Simulink/Stateflow (SLSF) environment for generating simulation traces and for obtaining formal models. Computation of the overapproximation relies on computing error bounds in the dynamics obtained from the formal model. Verification results from three case studies, namely, a version of the navigation benchmark, an engine control system, and a satellite system suggest that this combined formal analysis and simulation based approach may scale to larger problems.

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.

This article introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded control systems. In a PCHA, control actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. For PCHAs with polynomial continuous vector fields, it is possible to check these conditions automatically using, for example, quantifier elimination or sum of squares decomposition. We examine the feasibility of this automatic approach on a small example. The proposed technique is also used to manually verify safety and progress properties of a fairly complex planner-controller subsystem of an autonomous ground vehicle. Geometric properties of planner-generated paths are derived which guarantee that such paths can be safely followed by the controller.

In a previous paper [7] we have identified a special class of linear hybrid automata, called Deterministic Transversal Linear Hybrid Automata, and shown that an e-reach set up to a finite time, called a bounded e-reach set, can be computed using infinite precision calculations. However, given the linearity of the system and the consequent presence of matrix exponentials, numerical errors are inevitable in this computation. In this paper we address the problem of determining a bounded e-reach set using variable finite precision numerical approximations. We present an algorithm for computing it that uses only such numerical approximations. We further develop an architecture for such bounded e-reach set computation which decouples the basic algorithm for an e-reach set with given parameter values from the choice of several runtime adaptation needed by several parameters in the variable precision approximations.

This paper describes a toolkit for synthesizing hybrid supervisory control systems starting from the popular Simulink/Stateflow modeling environment. The toolkit provides a systematic strategy for translating Simulink/Stateflow models to hybrid automata and a discrete abstraction-based algorithm for synthesizing supervisory controllers.

Abstract This paper describes a methodology for developing and verifying a class of distributed systems in which the state space may be discrete or continuous. Our focus is on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also outlined.

Advances in wireless vehicular networks present us with opportunities for developing new distributed traffic control algorithms that avoid phenomena such as abrupt phase transitions. Towards this end, we study the problem of distributed traffic control in a partitioned plane where the movement of all entities (vehicles) within each partition (cell) is tightly coupled. We present a distributed traffic control protocol that guarantees minimum separation between vehicles at all times, even when some cells' control software may fail. Once failures cease, the protocol is guaranteed to stabilize and the vehicles with feasible paths to a target cell make progress towards it. The algorithm relies on two general principles: temporary blocking for maintenance of safety and local geographical routing for guaranteeing progress. Our proofs use mostly assertional reasoning and may serve as a template for analyzing other safe and stabilizing distributed traffic control protocols. We also present simulation results which provide estimates of throughput as a function of vehicle velocity, safety separation, path complexity, and failure-recovery rates.

Providing integrity, efficiency, and performance guarantees is a key challenge in the development of next-generation cyberphysical systems. Rather than mandating complete system verification, the Simplex Architecture provides robust designs by incorporating a supervisory controller that takes corrective action only when the system is in danger of violating a desired invariant property such as safety. The central issue in applying this approach is designing the switching logic for the supervisory controller such that it guarantees safety and at the same time is not overly conservative.Previous research in the area relied on finding Lyapunov functions for the underlying continuous dynamical system. In contrast, in this paper, we present an automatic method for solving this design problem through discrete abstractions of the underlying hybrid system and model checking. We present a case study where, in collaboration with John Deere, we use the developed approach to create the Simplex decision module for an off-road vehicle, which is formally verified as both correct and timely.

We describe how a set of mobile robots can arrange themselves on any specified curve on the plane in the presence of dynamic changes both in the underlying ad hoc network and in the set of participating robots. Our strategy is for the mobile robots to implement a self-stabilizing virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs), and local broadcast communication. The VNs are associated with predetermined regions in the plane and coordinate among themselves to distribute the client nodes relatively uniformly among the VNs' regions. Each VN directs its local client nodes to align themselves on the local portion of the target curve. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired target formation.

Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A. We introduce a new type of simulation relation for hybrid automata— switching simulation —for establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT τ a can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. A solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton.

Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAME-based theorem proving support provided in the toolkit, for proving system properties, including timing properties. Several examples are provided by way of illustration.

Existing geographic routing algorithms depend on the planarization of the network connectivity graph for correctness, and the planarization process gives rise to a well-defined notion of "faces". In this paper, we demonstrate that we can improve routing performance by storing a small amount of local face information at each node. We present a protocol, path vector exchange (PVEX), that maintains local face information at each node efficiently, and a new geographic routing algorithm, greedy path vector face routing (GPVFR), that achieves better routing performance in terms of both path stretch and hop stretch than existing geographic routing algorithms by exploiting available local face information. Our simulations demonstrate that GPVFR/PVEX achieves significantly reduced path and hop stretch than greedy perimeter stateless routing (GPSR) and somewhat better performance than greedy other adaptive face routing (GOAFR+) over a wide range of network topologies. The cost of this improved performance is a small amount of additional storage, and the bandwidth required for our algorithm is comparable to GPSR and GOAFR+ in quasi-static networks.