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.

key words

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

Citizenship:  Open to U.S. citizens

Level:  Open to Postdoctoral and Senior applicants