Phase II: Correct-by-Construction Synthesis for Multi-Vehicle Autonomy Missions

ABSTRACT: The kinds of capability advancements we anticipate include scalable support for multi-vehicle scenarios with concurrent executions, timing and synchronization constraints, heterogeneous sets of specifications, and fault tolerance. The tool development will focus on an open-source software package that integrates with AFRL's AMASE multi-vehicle UAV simulator. The software package 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.; 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.