Search for: All records

The key concept for safe and efficient traffic management for Unmanned Aircraft Systems (UAS) is the notion of operation volume (OV). An OV is a 4-dimensional block of airspace and time, which can express an aircraft’s intent, and can be used for planning, de-confliction, and traffic management. While there are several high-level simulators for UAS Traffic Management (UTM), we are lacking a frame- work for creating, manipulating, and reasoning about OVs for heterogeneous air vehicles. In this paper, we address this and present SkyTrakx—a software toolkit for simulation and verification of UTM scenarios based on OVs. First, we illustrate a use case of SkyTrakx by presenting a specific air traffic coordination protocol. This protocol communicates OVs between participating aircraft and an airspace manager for traffic routing. We show how existing formal verification tools, Dafny and Dione, can assist in automatically checking key properties of the protocol. Second, we show how the OVs can be computed for heterogeneous air vehicles like quadcopters and fixed-wing aircraft using another verification technique, namely reachability analysis. Finally, we show that SkyTrakx can be used to simulate complex scenarios involving heterogeneous vehicles, for testing and performance evaluation in terms of workload and response delays analysis. Our experiments delineate the trade-off between performance and workload across different strategies for generating OVs. 

As autonomous systems begin to operate amongst humans, methods for safe interaction must be investigated. We consider an example of a small autonomous vehicle in a pedestrian zone that must safely maneuver around people in a free-form fashion. We investigate two key questions: How can we effectively integrate pedestrian intent estimation into our autonomous stack? Can we develop an online monitoring framework to give rigorous assurances on the safety of such human-robot interactions? We present a pedestrian intent estimation framework that can accurately predict future pedestrian trajectories given multiple possible goal locations. We integrate this into a reachability-based online monitoring and decision making scheme that formally assesses the safety of these interactions with nearly real-time performance (approximately 0.1s). These techniques are both tested in simulation and integrated on a test vehicle with a complete in-house autonomous stack, demonstrating safe interaction in real-world experiments. 

In this paper, we investigate how symmetry transformations of equivariant dynamical systems can reduce the computation effort for safety verification. Symmetry transformations of equivariant systems map solutions to other solutions. We build upon this result, producing reachsets from other previously computed reachsets. We augment the standard simulation-based verification algorithm with a new procedure that attempts to verify the safety of the system starting from a new initial set of states by transforming previously computed reachsets. This new algorithm required the creation of a new cache-tree data structure for multi-resolution reachtubes. Our implementation has been tested on several benchmarks and has achieved significant improvements in verification time. 

We study the problem of load-balancing in path selection in anonymous networks such as Tor. We first find that the current Tor path selection strategy can create significant imbalances. We then develop a (locally) optimal algorithm for selecting paths and show, using flow-level simulation, that it results in much better balancing of load across the network. Our initial algorithm uses the complete state of the network, which is impractical in a distributed setting and can compromise users' privacy. We therefore develop a revised algorithm that relies on a periodic, differentially private summary of the network state to approximate the optimal assignment. Our simulations show that the revised algorithm significantly outpe forms the current strategy while maintaining provable privacy guarantees.