Parallel and Distributed Systems, International Conference on (2005)
July 20, 2005 to July 22, 2005
Christopher Rouff , SAIC
Mike Hinchey , NASA GSFC
Walt Truszkowski , NASA GSFC
James Rash , NASA GSFC
<p>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.</p>
Verification, formal methods, swarms, autonomy, emergent behavior, spacecraft.
C. Rouff, J. Rash, W. Truszkowski and M. Hinchey, "Verifying Large Numbers of Cooperating Adaptive Agents," Parallel and Distributed Systems, International Conference on(ICPADS), Fukuoka, Japan, 2005, pp. 391-397.