Composability Tools for Assured Autonomy
Abstract
This proposal describes the development of a framework capable of composing assurance arguments to progressively certificate hybrid, adaptive, autonomous systems in a growing spectrum of possible environments. Herein, the focus is on utilizing formal methods to specify and reason on components of cyber-physical systems (CPS) and their attendant properties in order to obtain a global property for the entire system. Though formal composition frameworks are not novel, many are not well-suited for the verification of autonomous CPS. This is due in part to the complex interconnections of autonomous CPS components, the diverse types of properties that must be expressed and proven for CPS components, the presence of nondeterminism in adaptive and learning-based components, and the incompleteness of many compositional proof rules. This proposal addresses these issues by (1) utilizing various mathematical theories to express and reason on components and properties that are not amenable to formal methods, (2) incorporating run-time assurance monitors and pre-certified backup modules to complement learning-based components, and (3) obtaining evidence for assurance arguments in gradually broader environments via safe test & evaluation. These results will enable a reliable, modular, and tractable test & evaluation, verification & validation approach towards building assurance arguments for the ArmyÕs assets. Though the basis for this work is a formal framework, the tasks in this proposal are not focused on developing a novel formal framework from the ground up. Rather, one or two frameworks that have promise in addressing the aforementioned challenges but currently fall short will be chosen initially. Then, considerable work will be done on utilizing additional mathematical tools to enhance what currently exists in order to provide an approach that can rigorously reason on the diverse aspects of autonomous CPS. This includes integrating various mathematical theories to substantiate and express properties which cannot be proven or expressed solely in the formal framework. The proposed contributions will enable a systematic approach to proving refinement and composability of the disparate modules that constitute a CPS. Central to this work is addressing the nondeterminism inherent in adaptive and learning-based components of the CPS. A Òmonitor-and-switchÓ scheme is proposed for each adaptive or learningbased component, wherein run-time assurance monitors check the behavior of the system and its components and switch, when necessary, to limited-functionality, secondary components with verified safety invariants. This scheme enables the assured test & evaluation of autonomous CPS with adaptive components. Once enough evidence is generated for the adaptive components under a ÒbaseÓ environment, some environmental assumptions may be removed, and assurance evidence can be accumulated under a less restrictive environment. This process is repeated, cumulatively generating assurance on the autonomous CPS operation under broader and broader environments. Along with the enhancement of the composability framework, its application will be demonstrated by conducting expansive flight tests on unmanned aircraft systems. Test & evaluation will play an essential role in both validating the claims obtained formally and generating evidence for assurance arguments. The planned test program will demonstrate both the utility and soundness of the proposed approach in assuring autonomous CPS in dynamic environments.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jun 25, 2021
- Source ID
- W911NF2110250
Entities
People
- Mazen Farhood
Organizations
- Army Contracting Command
- United States Army
- Virginia Tech