Verifying large numbers of cooperating adaptive agents

NASA is proposing to use large numbers of cooperating spacecraft in future exploration missions. These swarms will exhibit complex behaviors and interactions that can result in unintended emergent properties. Verifying the proper behavior of these new types of missions will be critical to their success. This paper gives the results of research into the use of formal methods techniques for verification of a large number of cooperating agents. Multiple formal methods were evaluated to determine their effectiveness in assuring the behavior of swarms of spacecraft. The NASA ANTS mission was used as an example of swarm intelligence against which to apply the formal methods. This paper discusses the evaluation of these formal methods, provides a partial specification of ANTS using four selected methods, and an outline of an integrated formal method for verifying future NASA swarm missions.