Information Technology Reference
In-Depth Information
formal methods in agent-oriented engineering, might not be best for modelling biologi-
cal phenomena due to the lack of expressiveness when it comes to such large-scale com-
municating and emergent systems. Moreover, as the complexity of a MAS increases,
considerable difficulties get introduced in the process of formal modelling.
Biological and biologically-inspired systems (bio-MAS) can be characterised as spa-
tial MAS. Spatial agents can be defined as collections of agents distributed and moving
through a physical space. They have incomplete knowledge of the environment and
can change their direction and position within the environment. When it comes to data
modelling of spatial agents, there are three key features in their development [5]:
-
Conceptual data model, which acts as a representation of the reality as it is, defined
by the users;
-
Logical data model, which defines how the conceptual model will be implemented;
and
-
The physical data model or the computer code of the application.
Targeting the conceptual data model, there are different approaches for modelling spa-
tial phenomena of biological systems: process algebra can be applied to develop a
calculus of processes that could describe the spatial geometric transformations [6].
Membrane computing can also be utilised by introducing geometric information [7]
or population P systems [8]. Another agent-based approach is the intracellular NF-
κ
B
signalling pathway for modelling spatial information in predictive complex biological
systems [9]. However, the combination of biological agents and spatial data modelling
still remains an active research field. With this work we focus on modelling spatial
agents with a formal method, namely X-machines, which are targeted at representing
the behaviour of biological colonies.
Defined as complex systems, spatial MAS should be characterised with reliability,
quality and robustness. Therefore, besides modelling, verification can be considered
the next important step in the developing cycle. However, it is fairly straightforward
(although not easy) to apply the known verification and validation techniques to spatial
systems composed from one agent, but it is extremely hard to transfer such techniques
to spatial MAS with a dynamic behaviour. We discuss that visual animation as an infor-
mal verification technique, helps in discovering the flaws of the formally unverifiable
properties within a spatial MAS (such as their position or direction with respect to the
environment). It is argued that attempts to formally verify such properties would result
into a combinatorial explosion. Moreover, visual animation provides means to facil-
itate the communication gap between the formal methods experts and the biologists
(which in turn have no formal background) by providing an immediate feedback under-
standable to both sides. And finally, visual animation can often lead to detecting some
emergent behaviour within a system. Therefore, this work opens the question about how
to automatically visualise a given state based model.
Starting with a detailed discussion on X-machines, later extended by a case study
(Section 2), we demonstrate its drawbacks when it comes to modelling the spatial char-
acteristic of an agent. This provides grounds to introducing a formal variation called
Spatial X-machines (
sp
XMs, Section 3). This structure will be carefully deliberated,
followed by discussion about their support towards verification and validation (Sec-
tion 4). Given a formal model, it is interesting to consider what properties should be
