Experiences applying formal approaches in the development of swarm-based space exploration systems

Experiences applying formal approaches in the development
of swarm-based space exploration systems

Abstract

NASA is researching advanced technologies
for future exploration missions using intelligent
swarms of robotic vehicles. One of these missions is the
Autonomous Nano-Technology Swarm (ANTS)mission
that will explore the asteroid belt using 1,000 cooperative
autonomous spacecraft. The emergent properties of
intelligent swarms make it a potentially powerful concept,
but at the same time more difficult to design and
ensure that the proper behaviors will emerge. NASA is
investigating formal methods and techniques for verification
of such missions. The advantage of using formal
methods is the ability to mathematically verify the
behavior of a swarm, emergent or otherwise. Using the
ANTS mission as a case study, we have evaluated multiple
formal methods to determine their effectiveness
in modeling and ensuring desired swarm behavior. This
paper discusses the results of this evaluation and proposes
an integrated formal method for ensuring correct
behavior of future NASA intelligent swarms.