# Presentation: 037061

## Formal Approaches 

**to Swarm Technologies**
- Technical Briefing

*Christopher Rouff, Amy Vanderbilt - SAIC*
*Walt **Truszkowski, James Rash -  **NASA GSFC, Code 588*
*Mike Hinchey - NASA GSFC, Code 581*

- SAS 2004

## Problem

- Future space missions will require cooperation between multiple satellites/rovers
- Developers are proposing intelligent, autonomous swarms to do new science
- Swarm-based systems are highly parallel and nondeterministic
- Testing these systems using current techniques will be difficult to impossible

## ANTS Mission

## ANTS MISSION

## Difficulty of Testing Swarms

-  Emergent properties that may not be known
-  Highly distributed and parallel
-  Large number of interacting entities
-  Worse than exponential growth in interactions
-  Intelligent entities (capabilities increase over time)
-  Total or near total autonomy
-  Very little experience in verification and validation of swarm-based systems

## Relevance to NASA

** **Many future missions will be intelligent collaborative distributed systems
-  Autonomy and autonomic properties will be necessary to manage and operate these systems
-  Swarms will allow new way for doing science
-  Verifying these missions will be paramount due to complexity and emergent behaviors
-  Need verification techniques for these systems

## Approach

-  Survey formal approaches for agent-based, multi-agent and swarm-based systems for appropriate swarm-based methods
-  Apply most promising approaches to parts of ANTS
-  Evaluate methods for needed properties
-  Model and outline swarm-based formal method
-  Develop formal method for swarm-based systems
-  Do formal specification of ANTS using new method
-  Prototype support tools

## Accomplishments

** **Surveyed formal approaches
-  Applied most promising approaches to ANTS
-  Evaluated methods
-  Developed properties for swarm formal method
-  Developed model and outline for a hybrid swarm-based formal method

## Formal Methods Survey

**Criteria for Surveying Formal Methods**
- Emphasis given to formal methods used for:
- Swarm, multi-agent, or distributed specifications
- Evaluated based on:
- Concurrency support, algorithm support, tool support, formal basis, used in agent-based specifications, used in swarm-based specifications

## Formal Methods Surveyed

** ****Process Algebras**
- CSP, CCS, Pi-Calculus, I/O Automata
** ****Model-Oriented Approaches**
- Z, B, FSMs, Statecharts, Petri Nets, X-Machines
** ****Logics**
- Temporal, Real Time, BDI, KARO
** ****Other Approaches**
- Artificial Physics, Mathematical Analysis, Game Theory, UML, Hybrid Approaches

## Specifications 

** ****CSP – **Communicating Sequential Processes
** ****WSCCS – **Weighted Synchronous Calculus of Communicating Systems
** ****Unity logic**
** ****X-Machines**

## CSP

** ****Communicating Sequential Processes**
-  Developed by C.A.R. Hoare
-  Process Algebra
-  Processes are recursively defined as an event followed by a process
-  Use channels for processes to communicate
-  Channels are guarded by events
-  Properties of CSP specifications can be proven correct

## CSP

## CSP

## CSP

## CSP

## CSP

** ****Evaluation**
-  Strengths
-  Specifying inter-process protocols
-  Identifying race conditions
-  Easily translated into model checking language
-  Weaknesses
-  No mechanism for analyzing emergent behavior

## WSCCS

-  Weighted Synchronous Calculus of Communicating Systems
-  Developed by Chris Tofts
-  Used to model social insects
-  Uses a state-based approach with frequencies and priorities for transitions
-  Frequencies and priorities can give you the probability of taking an action

## WSCCS

| Agent State | Actions leading to the agent state | f | p |
| --- | --- | --- | --- |
|  | Identity |  |  |
| Communicating | SendMessageWorker  | 50 | 2 |
|  | SendMessageLeader | 50 | 2 |
|  | SendMessageError | 1 | 1 |
|  | ReceiveMessageWorker | 50 | 2 |
|  | ReceiveMessageLeader | 50 | 2 |
|  | ReceiveMessageError | 1 | 1 |
| Reasoning | ReasoningDeliberatve | 50 | 2 |
|  | ReasoningReactive | 50 | 2 |
| Processing | ProcessingSortingAndStorage | 17 | 2 |
|  | ProcessingGeneration | 17 | 2 |
|  | ProcessingPrediction | 17 | 2 |
|  | ProcessingDiagnosis | 16 | 2 |
|  | ProcessingRecovery | 16 | 2 |
|  | ProcessingRemediation | 17 | 2 |

## WSCCS

## WSCCS

## WSCCS

** ****Evaluation**
-  Strengths
-  Process algebra strengths
-  Specifies priorities and probabilities of actions
-  Rules for predicting behavior
-  Weaknesses
-  Ability to track and model goals and other aspects of the spacecraft

## Unity Logic

-  Developed by Chandy and Misra
-  Syntax similar to Propositional Logic
-  Reason about predicates and states
-  Very good for concurrent systems

## Unity Logic

**Assertions**

- [Communicating]ReasoningDeliberatve(Leader)[Reasoning]

- [Reasoning] SendMessage (Leader,Worker)[Communicating]

- [Processing] SendMessage (Leader, Worker) [Communicating]

## Unity Logic

** ****Evaluation**
- Strengths
-  Strengths of logic-based systems
-  A method for reasoning about predicates and the states they imply
-  A method for defining specific mathematical and statistical calculations to be performed
-  Weaknesses
-  Not rich enough for reasoning about emergent behavior

## X-Machines

-  Developed by Samuel Eilenberg
-  Based on Finite State Machines
-  Have an internal memory state
-  Transitions are functions:
-  Input x Memory → Output x Memory

## X-Machines

## X-Machines

## X-Machines

**Set of states**

**Transition functions**

## X-Machines

- Start		SendMessage 	Commun.
- 		ReceiveMessage	Commun.
- 		Reason		Reasoning
- 		Process		Processing
- Communicating	SendMessage 	Commun.
- 		ReceiveMessage	Commun.
- 		Reason		Reasoning
- 		Process		Processing
- Reasoning	SendMessage 	Commun.
- 		ReceiveMessage	Commun.
- 		Reason		Reasoning
- 		Process		Processing
- Processing	SendMessage 	Commun.
- 		ReceiveMessage	Commun.
- 		Reason		Reasoning
- 		Process		Processing

**Leader States and Transitions**

## X-Machines

## X-Machines

** ****Evaluation**
-  Strengths
-  State-based system with memory
-  Executable
-  Weaknesses
-  No robust means for reasoning about or predicting behaviors beyond standard propositional logic

## Model of Formal Method

-  Blending of methods seems to be the best approach for specifying swarm-based systems
-  Blending of priority and probability aspects of WSCCS with memory and transition function aspects of X-Machines as well as logic from Unity Logic is a possibility and is currently being researched

## Model of Formal Method

## Future Work

-  Exploring Chaos Theory
-  Modifying WSCCS with different probabilistic methods
-  Blending above methods into a hybrid formal method

## Next steps

- Develop formal method for swarm-based systems based on current model
- Do formal specification of ANTS using new method
- Prototype support tools

## Publications

**Conferences**
- Rouff, C., Vanderbilt, A., Hinchey, M. Truszkowski, W., Rash, J.  Properties of a Formal Method for Prediction of Emergent Behaviors in Swarm-based Systems.  2nd IEEE International Conference on Software Engineering and Formal Methods.  Beijing, China, 26-30 September, 2004.
- Rouff, C. Hinchey, M. and Truszkowski, W.  Towards a Formal Approach to Swarm Technology.  8th International Conference on Space Operations (SpaceOps 2004).  Montreal, Canada, May 17-21, 2004.
- Rouff, C., Vanderbilt, A., Truszkowski, W., Rash, J. and Hinchey, M.  Verification of NASA Emergent Systems.  First IFIP International Conference on Artificial Intelligence Applications and Innovations.  August 23-26, 2004.
- Rouff, C., Vanderbilt, A., Truszkowski, W., Rash, J. and Hinchey, M.  Verification of NASA Emergent Systems.  Ninth International Conference on Engineering of Complex Computer Systems (ICECCS 2004), Florence, Italy, April 14-16, 2004.

## Publications

**Workshops**
- Rouff, C., Vanderbilt, A., Hinchey, M., Truszkowski, W., and Rash, J.  Verification of Emergent Behaviors in Swarm-based Systems.  Workshop on Engineering of Autonomic Systems.  In Proceedings of IEEE International Conference on Engineering of Computer Based Systems (ECBS 2004), Brno, Czech Republic, May 24-27, 2004.
- Rouff, C., Vanderbilt, A., Hinchey, M., Truszkowski, W., and Rash, J.  Properties of a Formal Method for Modeling Emergence in Swarm-based Systems.  In Proceedings of the Third NASA Goddard Workshop on Formal Approaches to Agent Based Systems.  Springer, Lecture Notes in Artificial Intelligence.  April 2004.
- Rouff, C., Truszkowski, W., Rash, J. and Hinchey, M.  Formal Approaches to Intelligent Swarm Technology.  IEEE/NASA Software Engineering Workshop.  December 2003.