Verifying future swarm-based missions

NASA is investigating new paradigms for future space exploration, heavily focused on the (still) emerging technologies of autonomous and autonomic systems. Traditional missions, reliant on one large spacecraft, are being replaced with missions that involve smaller collaborating spacecraft, analogous to swarms in nature. This approach offers several advantages: the ability to send spacecraft to explore regions of space where traditional craft simply would be impractical, greater redundancy (and, consequently, greater protection of assets), and reduced costs and risk, to name but a few. These new approaches to exploration simultaneously pose many challenges. The missions will be unmanned and highly autonomous. They will also exhibit the properties of autonomic systems, being selfprotecting, self-healing, self-configuring, and self-optimizing. To address the challenge in verifying the above missions, a NASA project, Formal Approaches to Swarm Technology (FAST), is investigating appropriate formal methods for use in such missions, and is beginning to apply these techniques to specifying and verifying parts of a NASA swarm-based concept mission.