Formal modelling of the dynamic behaviour of biology-inspired, agent-based systems

Multi-agent systems are highly dynamic since the agents' abilities and the system configuration often changes over time. In some ways, such multiagent systems seem to behave like biological processes; new agents appear in the system, some others cease to exist, and communication between agents changes. One of the challenges is to attempt to formally model the dynamic configuration of multi-agent systems. Towards this aim, we present a formal method, namely X-machines, that can be used to formally specify, verify, and test individual agents. In addition, communicating X-machines provide a mechanism for allowing agents to communicate messages to each other. We utilize concepts from biological processes in order to identify and define a set of operations that are able to reconfigure a multi-agent system. In this chapter we present an example in which a biology-inspired system is incrementally built in order to meet our objective.