Formally Verified Run-Time Assurance (RTA) in the Presence of Information Uncertainty

With the rapid expansion in the development and intended use of autonomous systems, the ability to certify that these systems will operate in a robust and safe manner has not kept pace. This gap is leading to an extensive increased cost of development/procurement, delays in adoption, and in the most severe cases, a decrease in safety margins. The major focus of the effort is to demonstrate and prototype a formal run-time assurance (RTA) system that accounts for data integrity and information uncertainty. Many approaches to RTA currently rely solely on static boundary conditions and discrete switching approaches, thus not resilient to changes to state observability changes and resulting uncertainty. This lack of built-in resiliency can be very detrimental to operational efficiency.  Our innovative approach to RTA will inherently build in the various aspects of state uncertainty into the formalization of the safety conditions and switching logic.  Accounting for the data uncertainty and simultaneously maintaining the formalization of the system will be the key innovation of this work. This development research will be performed using a typical rejoin scenario to study the general principles and formulate recommendations for scaling the formal process to larger systems. The proposal team has included a letter of support for future integration of the design within the reinforcement learning environment developed by the Autonomy Capability Team (ACT3) researchers and will provide recommendations for generation of flight-ready software. Our long-term technical objectives include developing a USAF commercialization strategy, demonstrating capabilities of our Formally Verified RTA for an aircraft rejoin scenario, scaling the formal process to larger systems, demonstrating ability to extend our RTA technology to other missions without extensive development, finding additional USAF customers, and including this technology within the Air Force Cognitive Engine (ACE) for expanded USAF use.