Scalable verification of autonomous systems using gray-box reachability approved for public release
Abstract
Autonomous system design combines model-based fields such as control theory and robotics with data-driven approaches such as machine, learning and deep neural networks. Traditional verification and validation (V&V) methods like testing and simulation are useful too,ls for designing and debugging systems. Unfortunately, exhaustive simulation of complex autonomous systems is not possiblesimulatio,n may miss unsafe situations.In the proposed research, our objective is to develop stronger analysis methods by reasoning with the u,ncertainty in the environment and how it propagates through each of the components in the autonomous system. The technical approach,is grounded in formal verification through reachability analysis of hybrid systems, where sets of states are propagated using mathem,atical models of nondeterministic components and the physical world. At a high-level, rather than simulating individual system state,s, reachability analysis takes into account nondeterminism and performs reasoning with sets instead of individual system states. We,hypothesize that set-based reachability is better suited for V&V of autonomous systems, better able to find errors caused by sequenc,es of rare events.However, there are practical issues when applying set-based reachability to autonomous systems. Most critically, a,spects of the system may not be fully exposed, such as a proprietary module designed by a subcontractor or a component from an allie,d nation. For this reason, we strive to develop verification approaches that are gray-box, where some components may have a mathemat,ical model of their behaviors but others could be black-box simulators with limited information about their internals.The objective,of the proposed research is to improve upon simulation-based approaches and develop rigorous analysis methods for heterogeneous gray,-box systems. This includes inferring symbolic models from gray-box components, the development of probabilistic-symbolic analysis m,ethods, and approaches to increase scalability through uncertainty reduction. (approved for public release)
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Feb 08, 2022
- Source ID
- N000142212156
Entities
People
- Stanley Bak
Organizations
- Office of Naval Research
- Research Foundation for the State University of New York
- United States Navy