Properties of a formal method for prediction of emergent behaviors in swarm-based systems

Christopher Rouff, Mike Hinchey, Walt Truszkowski, James Rash

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Autonomous intelligent swarms of satellites are being proposed for NASA missions that have complex behaviors and interactions. The emergent properties of swarms make these missions powerful, but at the same time more difficult to design and assure that proper behaviors will emerge. This paper gives the results of research into formal methods techniques for verification and validation of NASA swarm-based missions. Multiple formal methods were evaluated to determine their effectiveness in modeling and assuring the behavior of swarms of spacecraft. The NASA ANTS mission was used as an example of swarm intelligence for which to apply the formal methods. This paper will give the evaluation of these formal methods and give partial specifications of the ANTS mission using four selected methods. We then give an evaluation of the methods and the needed properties of a formal method for effective specification and prediction of emergent behavior in swarm-based systems.

Original languageEnglish
Title of host publicationProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004
EditorsJ.R. Cuellar, Z. Liu
Pages24-33
Number of pages10
DOIs
Publication statusPublished - 2004
Externally publishedYes
EventProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004 - Beijing, China
Duration: 28 Sep 200430 Sep 2004

Publication series

NameProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004

Conference

ConferenceProceedings of the Second International Conference on Software Engineering and Formal Methods. SEFM 2004
Country/TerritoryChina
CityBeijing
Period28/09/0430/09/04

Fingerprint

Dive into the research topics of 'Properties of a formal method for prediction of emergent behaviors in swarm-based systems'. Together they form a unique fingerprint.

Cite this