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.
more »
« less
π²πΌπΎππΎπ’ππΎπΌππΎπ : Boosting Scenario Verification Using Symmetry Abstractions
We present π²πΌπΎππΎπ’ππΎπΌππΎπ, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. π²πΌπΎππΎπ’ππΎπΌππΎπ 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. π²πΌπΎππΎπ’ππΎπΌππΎπ 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 π²πΌπΎππΎπ’ππΎπΌππΎπ 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*, π²πΌπΎππΎπ’ππΎπΌππΎπ shows 14Γ average speedup in verification time, even while using those very tools as reachability subroutines.
more »
« less
- Award ID(s):
- 1918531
- PAR ID:
- 10366109
- Editor(s):
- Silva, A. and
- Date Published:
- Journal Name:
- Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science(), vol. Springer, Cham
- Volume:
- 12759
- Page Range / eLocation ID:
- 580β594
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Silva, A. (Ed.)This paper presents Verisig 2.0, a verification tool for closed-loop systems with neural network (NN) controllers. We focus on NNs with tanh/sigmoid activations and develop a Taylor-model-based reachability algorithm through Taylor model preconditioning and shrink wrapping. Furthermore, we provide a parallelized implementation that allows Verisig 2.0 to efficiently handle larger NNs than existing tools can. We provide an extensive evaluation over 10 benchmarks and compare Verisig 2.0 against three state-of-the-art verification tools. We show that Verisig 2.0 is both more accurate and faster, achieving speed-ups of up to 21x and 268x against different tools, respectively.more » « less
-
This manuscript presents the updated version of the Neural Network Verification (NNV) tool. NNV is a formal verification software tool for deep learning models and cyber-physical systems with neural network components. NNV was first introduced as a verification framework for feedforward and convolutional neural networks, as well as for neural network control systems. Since then, numerous works have made significant improvements in the verification of new deep learning models, as well as tackling some of the scalability issues that may arise when verifying complex models. In this new version of NNV, we introduce verification support for multiple deep learning models, including neural ordinary differential equations, semantic segmentation networks and recurrent neural networks, as well as a collection of reachability methods that aim to reduce the computation cost of reachability analysis of complex neural networks. We have also added direct support for standard input verification formats in the community such as VNNLIB (verification properties), and ONNX (neural networks) formats. We present a collection of experiments in which NNV verifies safety and robustness properties of feedforward, convolutional, semantic segmentation and recurrent neural networks, as well as neural ordinary differential equations and neural network control systems. Furthermore, we demonstrate the capabilities of NNV against a commercially available product in a collection of benchmarks from control systems, semantic segmentation, image classification, and time-series data.more » « less
-
Deshmukh, Jyotirmoy V. ; Havelund, Klaus ; Perez, Ivan (Ed.)Reachability analysis is a fundamental problem in verification that checks for a given model and set of initial states if the system will reach a given set of unsafe states. Its importance lies in the ability to exhaustively explore the behaviors of a model over a finite or infinite time horizon. The problem of reachability analysis for Cyber-Physical Systems (CPS) is especially challenging because it involves reasoning about the continuous states of the system as well as its switching behavior. Each of these two aspects can by itself cause the reachability analysis problem to be undecidable. In this paper, we survey recent progress in this field beginning with the success of hybrid systems with affine dynamics. We then examine the current state-of-the-art for CPS with nonlinear dynamics and those driven by ``learning-enabled'' components such as neural networks. We conclude with an examination of some promising directions and open challenges.more » « less
-
This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. We focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network's hybrid system with the plant's, we transform the problem into a hybrid system verification problem which can be solved using state-of-the-art reachability tools. We show that reachability is decidable for networks with one hidden layer and decidable for general networks if Schanuel's conjecture is true. We evaluate the applicability and scalability of Verisig in two case studies, one from reinforcement learning and one in which the neural network is used to approximate a model predictive controller.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
