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, 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.