Correct-by-Construction Synthesis for Multi-Vehicle Autonomy Missions

Award Information
Agency: Department of Defense
Branch: Air Force
Contract: FA9550-15-C-0023
Agency Tracking Number: F14A-T06-0018
Amount: $149,974.00
Phase: Phase I
Program: STTR
Solicitation Topic Code: AF14-AT06
Solicitation Number: 2014.1
Timeline
Solicitation Year: 2014
Award Year: 2015
Award Start Date (Proposal Award Date): 2014-12-01
Award End Date (Contract End Date): 2015-09-01
Small Business Information
421 SW Sixth, Suite 300, Portland, OR, 97204
DUNS: 000000000
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Lee Pike
 (503) 626-6616
 leepike@galois.com
Business Contact
 Jodee LeRoux
Phone: (503) 808-7209
Email: jodee@galois.com
Research Institution
 University of Pennsylvania
 Ufuk Topcu
 3541 Walnut Street
Franklin Building, Suite P221
Philadelphia, PA, 19104
 (215) 898-7293
 Nonprofit college or university
Abstract
ABSTRACT: The kinds of capability advancements we anticipate include scalable support for multi-vehicle scenarios with concurrent executions, co-existence of adversarial and cooperative assets, timing and synchronization constraints, heterogeneous sets of specifications (e.g., prioritization over soft vs. hard constraints), and fault-tolerance. The tool development will focus on an open-source software package, which aims (i) to bridge the model-based protocol synthesis artifacts with the low-level implementations and the underlying communication and networking backbone while preserving the correctness guarantees, and (ii) to systematically and manageably interface operators/designers to autonomy protocols through a dedicated domain specific language (DSL). The DSL will provide specification templates, operator tools, and type-checking to detect specification errors before synthesis. We propose to explore techniques to overcome issues in scalability and simplifying specifications. We also propose to develop approaches to assist in certification as well as provide validation that the design and implementation are correct. We will validate our theoretical advances in a real-world testbed, using a small quadcopter unpiloted air system developed by Galois. BENEFIT: We anticipate new approaches to specify and synthesize missions for multi-vehicle scenarios as well as artifacts to ensure the controller implementations are correct. Furthermore, our approach raises the level of abstraction for mission planners. Our proposal will provide the technology to increase the autonomy of multi-vehicle missions as well as the confidence in the missions specified.

* Information listed above is at the time of submission. *

Agency Micro-sites

SBA logo
Department of Agriculture logo
Department of Commerce logo
Department of Defense logo
Department of Education logo
Department of Energy logo
Department of Health and Human Services logo
Department of Homeland Security logo
Department of Transportation logo
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government