Formal Methods for VandV and TandE of Autonomous Systems
Abstract
We propose to advance the mathematical and algorithmic foundations of test and evaluation by combining advances in formal methods for specification and verification of reactive, distributed systems with algorithmic design of multi agent test scenarios, and algorithmic evaluation of test results. Our approach will build on recent advances by our groups and others in synthesis of formal contracts for performance of agents and subsystems, development of barrier certificate methods for provably safe performance of nonlinear control systems, and substantial experience in the development of operational autonomous systems (self driving cars, legged robots, and cooperative autonomous aerial vehicles). We will expand these results by creating a mathematical framework for specifying the desired characteristics of multi agent systems involving cooperative, adversarial, and adaptive interactions, develop algorithms for verification and validation (VandV) as well as test and evaluation (TandE) of the specifications, and perform proof of concept demonstrations that demonstrate the use of formal methods for VandV and TandE of autonomous systems. If successful, our results will provide more systematic methods for describing the desired properties of military systems in complex environments; new algorithms for verification of system level designs against those properties, synthesis of test plans, and analysis of test results; design rules that allow adaptation and machine learning to be integrated without compromising system safety and performance specifications; and demonstration of the envisioned techniques in a multi agent, free flight arena that will provide experimental validation of the results.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 14, 2022
- Source ID
- FA95501910302
Entities
People
- Richard M. Murray
Organizations
- Air Force Office of Scientific Research
- California Institute of Technology
- United States Air Force