NRC Research Associate Programs
Fellowships Office
Policy and Global Affairs

Participating Agencies - AFRL

  sign inOpen Printer View

Opportunity at Air Force Research Laboratory (AFRL)

Formal Methods for Design and Verification of Autonomous Systems

Location

Aerospace Systems Directorate, RQ/Control, Power and Thermal Management Division

RO# Location
13.30.10.C0399 Wright-Patterson AFB, OH 454337542

Advisers

name email phone
Laura Renae Humphrey laura.humphrey@us.af.mil (937) 713-7032

Description

Verification and Validation (V&V) of autonomous systems is known to be challenging. Testing is the most common V&V approach, yet full-scale testing of autonomous systems is infeasible due to the immense number of costly and time-consuming tests that would be required to fully explore all possible system behaviors. Formal methods (i.e., mathematically-based approaches for specification, design, and verification) perform verification through analysis rather than testing, providing a potential solution to this problem. However, this requires using formal methods from the beginning, i.e. during the development of requirements, architectures, and component-level designs. They cannot simply be applied to an arbitrary system after it has already been built.

Toward this end, we are using formal methods to design autonomous capabilities for single-agent and multi-agent systems, especially unmanned air vehicles, such that we can provide machine-checked proofs of correctness. This includes formalizing system, architecture, and component-level requirements; the system architecture itself; and component-level designs/algorithms. It also includes creating verified software implementations of architectural components and component-level designs/algorithms. We therefore have an interest in using approaches such as model checking, automated theorem proving, and abstract interpretation to 1) formalize system-, architecture-, and component-level requirements and analyze them for consistency, completeness, realizability, etc., 2) compositionally verify that interacting components satisfy high-level system requirements, 3) manually develop autonomy algorithms and verify them against requirements, 4) synthesize autonomy algorithms from requirements in a “correct-by-construction” manner, 5) create software implementations that are formally verified to meet their requirements, and 6) wherever necessary, use other approaches such as modeling & simulation and testing to supplement formal methods and explain the overall verification strategy and evidence in an assurance case. Research in this area could involve creating new theory to increase the efficiency and/or expressivity of formal methods as applied to these areas; integrating new theory into open source tools; developing and analyzing/verifying formal requirements, architectures, and/or component-level designs/algorithms; developing verified software implementations of architecture and component-level designs/algorithms; and creating “best practices” for applying formal methods to autonomous systems.

Keywords:
Formal methods; software verification; model checking; automated theorem proving; compositional verification; end-to-end verification; multi-agent systems; autonomous systems

Eligibility

Citizenship:  Open to U.S. citizens
Level:  Open to Postdoctoral and Senior applicants

Stipend

Base Stipend Travel Allotment Supplementation
$76,542.00 $4,000.00

$3,000 Supplement for Doctorates in Engineering & Computer Science

Experience Supplement:
Postdoctoral and Senior Associates will receive an appropriately higher stipend based on the number of years of experience past their PhD.

Copyright © 2022. National Academy of Sciences. All rights reserved.Terms of Use and Privacy Policy