Environmental Engineering Reference
In-Depth Information
explosion problem, testers have artificially reduced the number of states of
these types of systems and approximated the underlying software using mod-
els. This approach, in general, sacrifices fidelity and can result in missed errors.
Consequently, even with relatively few spacecraft, the state space can be too
large to realistically test.
One of the most challenging aspects of using swarm technology is deter-
mining how to verify that emergent system behavior will be proper and that
no undesirable behaviors will occur. Verifying intelligent swarms is even more
dicult because the swarms no longer consist of homogeneous members with
limited intelligence and communications. Verification will be dicult not only
because each individual is tremendously complex, but also because of the
many interacting intelligent elements. To address the verification challenge,
ongoing research is investigating formal methods and techniques for verifica-
tion and validation of swarm-based missions.
Formal methods are proven approaches for ensuring the correct operation
of complex interacting systems. Formal methods are particularly useful in
specifying complex parallel and distributed systems - where a single person
finds it dicult to fully understand the entire system and where there are
typically multiple developers. Testers can use a formal specification to prove
that system properties are correct - for example, that the underlying system
will go from one state to another or not into a specific state. They can also
check for particular types of errors such as race conditions, and use the formal
specification as a basis for model checking.
Most formal methods do not address the problem of verifying emergent
behavior. Clearly in the ANTS PAM concept, the combined behavior of indi-
vidual spacecraft is far more complex than the behavior of each spacecraft in
isolation. The formal approaches to swarm technologies (FAST) project sur-
veyed formal methods techniques to determine whether any would be suitable
for verifying swarm-based systems and their emergent behavior [
125
,
126
].
The project found that there are a number of formal methods that support
the specification of either concurrency or algorithms, but not both. Though
there are a few formal methods that have been used to specify swarm-based
systems, the project found only two formal approaches that were used to
analyze the emergent behavior of swarms.
Weighted synchronous calculus of communicating systems (WSCCS), a
process algebra, was used by Sumpter et al. to analyze the nonlinear as-
pects of social insects [
163
]. X-Machines have been used to model cell biol-
ogy [
61
,
62
], and with modifications, the X-Machines model has the potential
for specifying swarms. Simulation approaches are also being investigated to
determine emergent behavior [
55
]. However, these approaches do not predict
emergent behavior from the model, but rather model the emergent behavior
after the fact.
The FAST project defined an integrated formal method, which is appro-
priate for the development of swarm-based systems [
121
]. Future work will
concentrate on the application of the method to demonstrate its usefulness,
