Difference between revisions of "Formal Methods for V&V and T&E of Autonomous Systems"

From MurrayWiki
Jump to: navigation, search
(Created page with "{{subst:project boilerplate}} {{Project |Title=Formal Methods for V&V and T&E of Autonomous Systems |Agency=AFOSR |Start date=1 July 2019 |End date=30 Jun 2022 |Support summar...")
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
 
{{righttoc}}  
 
{{righttoc}}  
Project description (typically about a paragraph)
+
The goal of this project to advance the mathematical and algorithmic foundations of test and evaluation by com- bining 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. Building on previous results 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 experience in the development of operational autonomous systems we are 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 (V&V) as well as test and evaluation (T&E) of the specifications, and per- form proof-of-concept demonstrations that demonstrate the use of formal methods for V&V and T&E 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; de- sign 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.
  
 
{| cellpadding=0 cellspacing=0 width=80%
 
{| cellpadding=0 cellspacing=0 width=80%
Line 11: Line 11:
 
|
 
|
 
Collaborators:
 
Collaborators:
 
+
* Aaron Ames
 +
* Petter Nilsson
 
Past participants:
 
Past participants:
 
{{project past participants}}
 
{{project past participants}}
Line 17: Line 18:
  
 
=== Objectives ===
 
=== Objectives ===
[[Image:project-name.png|right|400px]]
+
[[Image:afosr-testandeval.png|right|400px]]
Description of the main objectives of the project
+
The output of the project will be a set of tools (theory and algorithms) that address these challenges by demonstrating the use of formal techniques for specification, design, verification, and testing of autonomous systems operating in heterogeneous, multi-agent, adversarial environments. More specifically, we aim to accomplish the following specific objectives:
 +
* Create a mathematical framework for specification of desired characteristics of multi-agent autonomous and semi-autonomous systems that account for cooperative, adversarial, and adaptive interactions between agents.
 +
* Develop algorithms and software toolboxes for creation of layered models that are suitable for al- gorithmic verification of performance that incorporate existing test data as well as generate test plans and performance monitors for using in operational test and evaluation.
 +
* Demonstrate key concepts on a proof-of-concept experimental testbed that demonstrates the integration of test data with formal methods for specification and verification of autonomous and semi-autonomous system performance.
  
 
=== References ===
 
=== References ===

Revision as of 04:29, 10 June 2019

The goal of this project to advance the mathematical and algorithmic foundations of test and evaluation by com- bining 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. Building on previous results 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 experience in the development of operational autonomous systems we are 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 (V&V) as well as test and evaluation (T&E) of the specifications, and per- form proof-of-concept demonstrations that demonstrate the use of formal methods for V&V and T&E 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; de- sign 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.

Current participants:

Additional participants:

Collaborators:

  • Aaron Ames
  • Petter Nilsson

Past participants:

Objectives

Afosr-testandeval.png

The output of the project will be a set of tools (theory and algorithms) that address these challenges by demonstrating the use of formal techniques for specification, design, verification, and testing of autonomous systems operating in heterogeneous, multi-agent, adversarial environments. More specifically, we aim to accomplish the following specific objectives:

  • Create a mathematical framework for specification of desired characteristics of multi-agent autonomous and semi-autonomous systems that account for cooperative, adversarial, and adaptive interactions between agents.
  • Develop algorithms and software toolboxes for creation of layered models that are suitable for al- gorithmic verification of performance that incorporate existing test data as well as generate test plans and performance monitors for using in operational test and evaluation.
  • Demonstrate key concepts on a proof-of-concept experimental testbed that demonstrates the integration of test data with formal methods for specification and verification of autonomous and semi-autonomous system performance.

References

None to date


  • Agency: AFOSR
  • Grant number:
  • Start date: 1 July 2019
  • End date: 30 Jun 2022
  • Support: 1.5 postdocs, 2 graduate students
  • Reporting: Annual program review + report