A Process Algebraic Description of a Temporal Wireless Network Protocol


Electronic Communications of the EASST
Volume 45 (2011)

Proceedings of the
Fourth International Workshop on Formal Methods

for Interactive Systems
(FMIS 2011)

A Process Algebraic Description of a Temporal Wireless Network
Protocol

Colm Bhandal, Melanie Bouroche and Arthur Hughes

17 pages

Guest Editors: Judy Bowen, Steve Reeves
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

A Process Algebraic Description of a Temporal Wireless Network
Protocol

Colm Bhandal1∗, Melanie Bouroche1 and Arthur Hughes1

1 School of Computer Science & Statistics
Trinity College, Dublin, Ireland

bhandalc@tcd.ie
http://www.scss.tcd.ie/

Abstract: The problem of coordination is central to research in robotics, automat-
ically guided vehicles, autonomous cars, unmanned aerial vehicles, and any other
areas in which autonomous agents of any kind operate concurrently. This paper fo-
cuses on one particular model of coordination, namely Comhordú. The contribution
of this work is a formalisation of the existing model in precise mathematical terms.
This formalisation extends our understanding of the model and provides a basis for
future work such as the formal verification of model properties, e.g. system safety.

Keywords: Process calculus, Temporal, Protocol, Model, Wireless, Mobile agent,
System, Ad-hoc network.

1 Introduction

The problem of coordination is central to research in robotics [16, 26], automatically guided
vehicles [8], autonomous cars [4], unmanned aerial vehicles [2], and any other areas in which
autonomous agents of any kind operate concurrently. Of interest here are systems of mobile
autonomous agents, mobility here referring to physical movement in space. Coordination in this
setting is defined in [6] as “the management of interactions both amongst entities, and between
entities and their environment, towards the production of a result.”

The Comhordú model is a coordination model for the class of systems comprised of mobile
entities communicating over an unreliable wireless network. The model was developed in [6] and
[7] as an approach to coordination in a system of mobile agents that differed from the traditional
consensus-based approaches [21, 14, 11, 9] and other approaches [12, 27]. Within the model is
the notion of a safety constraint, which is specified for a particular system and denotes a property
that should never be violated by that system. Also included in the model is a description of how
entities should act to maintain this safety constraint, i.e. a protocol entities must follow.

This paper strives towards a formalisation of the Comhordú model. It is the first such attempt:
all work on Comhordú e.g. [6, 7] prior to this has been informal. The contribution of such a
formalisation if manifold. As stated in [28], a motivation for using formal specification is “to
add precision, to aid understanding, and to reason about properties of a design.” Precision &
understanding go hand in hand. An imprecise model or design of some system is difficult to
comprehend and may have many interpretations due to its inherent ambiguities. This lack of

∗ This author is sponsored by the Irish Research Council for Science, Engineering and Technology, IRCSET.

1 / 17 Volume 45 (2011)

mailto:bhandalc@tcd.ie
http://www.scss.tcd.ie/


A Process Algebraic Description of a Temporal Wireless Network Protocol

understanding will most likely lead to the design being incorrectly implemented, perhaps even to
the point of system failure. Further to increasing our understanding of a problem, formalisation
allows existing mathematical tools such as model checkers, e.g. [5], to be employed towards the
assertion of certain system properties.

Our present understanding of Comhordú is certainly enhanced as a direct result of this formal-
isation. The process of building a formal model of Comhordú has uncovered within the informal
model ambiguous concepts, hidden assumptions and under specified behaviours, none of which
were obvious prior to this work. These issues are resolved here via the introduction of modi-
fications and extensions to the model. Furthermore, while pre-existing model descriptions are
predominantly English-based, this description employs mathematical functions and a process
calculus [23] with formally defined rules. This adds an air of precision to the model. Finally, a
process algebraic description such as this one offers the future possibility of the specification of
system properties in a formal property logic. It is also likely that this formal model can be trans-
lated, somewhat approximately, into the language of a model checker which can machine verify
to an extent its correctness with respect to some sensible properties, such as the satisfaction of
the safety constraint.

The paper is organised as follows. Section 2 summarises the presentation of the protocol found
in [6] and [7]. Section 3 presents a semi formal Comhordú model. Extensions and modifications
to the original model are proposed therein, and the groundwork is laid for the subsequent formal
model. In Section 4, a process language is presented which is used in Section 5 to formally
specify the Comhordú protocol. A brief overview of related work is given in Section 6. Finally
in Section 7, this work is discussed and compared to related work.

2 Informal Description of the Comhordú System

Comhordú is a coordination model which was developed in [6] and [7]. The model is a means of
reasoning about certain systems of autonomous mobile entities which communicate over a wire-
less network. The model may also be used as an aid in the design of such systems. Summarised
in this section are the main aspects of the model. The description here is deliberately informal; a
formalised version of the same model will follow in Section 3 and Section 5.

In [6], it is noted that approaches to the problem of achieving coordination which were pro-
posed prior to Comhordú are primarily consensus based, with the exception of a few. While
these approaches are discussed in detail in [6], it is sufficient here to highlight that the corner-
stone of the Comhordú approach is that it departs from the traditional consensus based approach.
The consensus based approach requires that entities should have access to reliable communi-
cation and that the number of entities in the system is known a priori. The approach taken by
Comhordú is that, since neither of these conditions is guaranteed in a wireless ad-hoc network,
a consensus-based approach is not suitable in general. Within the Comhordú framework lies a
solution to coordination based on responsibility, an alternative concept to consensus.

Proc. FMIS 2011 2 / 17



ECEASST

2.1 Properties of the Comhordú Model

A Comhordú system1 incorporates a collection of entities. An entity is some mobile vehicle e.g.
a robot. Every entity has a type. The behaviour of an entity is governed partly by its type. At all
times, every entity will be in some state or another. The state of an entity contains information
about what it is doing, where it is, how fast it is travelling etc. A mode, or mode of operation, is
an abstraction of a state. For example, a state might tell us that a car is currently at coordinates
(154,23) travelling east at 9.6km/h while the mode of that same car might only indicate that
the car is travelling at an absolute speed in the range [0,10]km/h. A mode may be envisaged as
an equivalence class on states. We will assume here that the nature of abstraction from state to
mode yields a countable number of modes e.g. it may be that sates are points in some real space
while modes are cells in that space.

Every Comhordú system will have associated with it some notion of safe operation e.g. “No
vehicles are on a collision course”. A constraint on the system, called the safety constraint (Cs)
is a condition on the states of all the entities that embodies the safety requirements of the system.
This constraint may be evaluated at any time in the system. If it is true, then the system is safe
at the time of evaluation. A desirable property of any system is that the safety constraint always
holds true as long as entities within the system obey the system protocol i.e. as long as their
behaviours comply with certain rules of operation set out in the description of the system. A
key concept of the Comhordú system is that when entities are sufficiently far apart, they cannot
cause an incompatibility. This issue will be addressed later and used to reformulate the safety
constraint in simpler terms. Currently, a Comhordú safety constraint is given in terms of an
incompatibility that must never occur, where the following grammar describes incompatibilities.

incompatibility
def
= (incompatibility,“∧”,incompatibility)∣∣ (incompatibility,“∨”,incompatibility)∣∣ (elementType,“.”,stateVariable,relOperator,value)∣∣ (elementType,“.”,stateVariable,relOperator,elementType,

“.”,stateVariable)∣∣ (“distance(”, position,“,”, position,“)”,relOperatorr,value)∣∣ (“|”,entityType“.”,stateVariable,“|”,relOperator,value)
relOperator

def
= “ < ”

∣∣ “ ≤ ” ∣∣ “ > ” ∣∣ “ ≥ ” ∣∣ “ = ” ∣∣ “ 6= ”
The Comhordú model applies to systems communicating over a wireless network. A sub-

model of Comhordú is the space elastic model, a wireless communication model upon which
Comhordú is built. While the space elastic model concerns itself with problems at low level
communication layers, such as collisions at the physical layer, Comhordú deals at a higher level
of abstraction, relying on an interface provided by the space elastic model. This interface guaran-
tees time bounded notification of coverage to all entities in the network. Assume an entity begins
sending a message at time t. The actual coverage (Ca) of this message is the area to which it is

1 An instance of the model.

3 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

delivered by time t + msgLatency, where msgLatency is a fixed constant of the system. Provided
by the space elastic model is a notification of Ca to the sender within a time bound adaptNoti f .
In other words, by time t + msgLatency + adaptNoti f , an entity that has sent a message at time
t will be notified of the area to which that message was delivered by time t + msgLatency.

2.2 The Comhordú Protocol

A Comhordú system must contain a number of distinguished modes called fail safe modes. In
these modes, an entity must not be capable of contributing towards an incompatibility in the
system. Hence, if all entities remain in fail safe modes all the time, the system remains trivially
safe. However, if an entity wishes to progress towards one of its goals, it will most likely need
to transition to or remain in some mode that may result in an incompatibility. For example, if
a robot needs to get from point A to point B, is must move to do so, but moving introduces the
possibility of a collision. Entering such a mode in an arbitrary way would pose a threat to the
safety of the system. Hence, a protocol is imposed upon entities such that safety remains intact.

The protocol dictates that an entity wishing to act in some mode begins periodically sending
messages, to entities in its environment, containing its position and the desired mode of opera-
tion. The sender waits a pre-determined amount of time, while remaining to periodically broad-
cast messages, before entering this desired mode and progressing towards its goal. If at any time
the sender is notified of a degradation in coverage, or if it receives a message from another entity
with which it may become incompatible, it will immediately begin to transition to a different
mode that will ensure system safety. A conservative action for entities either receiving messages
from other possibly incompatible entities or experiencing coverage difficulties is to immediately
transition to a fail safe mode to maintain system safety. Henceforth, we shall refer to an entity in
some fail safe mode as being in the mode F S, i.e. we will cease to distinguish between different
fail safe modes. This is possible as the primary concern of the protocol is ensuring a lack of
incompatibilities, and all fail safe modes are equivalent in terms of the inability of any entity in
such a mode to cause an incompatibility.

In Figure 1, a sending entity sender sends a message to entities in its environment (receivers).
However, a degradation in coverage occurs and the message is not sent to a sufficient set of
receivers. The sender is notified of this degradation by the space elastic model at or before time
t′ = t + msgLatency + adaptNoti f , where t is the time the message sending was initiated. Since
an entity may not know the result of its message broadcast until time t′, it is necessary for every
entity to wait for a time of t′−t = msgLatency + adaptNoti f before it can act. However, the
question still remains as to whether this wait time is sufficient i.e. can an entity begin acting once
this time has elapsed? A consideration of this question in Section 3 leads to the conclusion that
this wait time alone is not always sufficient.

3 Towards a Formal Comhordú Model

In this section, semi-formal modified definitions of the features discussed in Section 2 are pro-
vided. These definitions form a bridge between the informal descriptions of Section 2 and the
strictly formal process-algebraic model of Section 5. In addition, new features are proposed here

Proc. FMIS 2011 4 / 17



ECEASST

Figure 1: Message sending with coverage degradation

that were absent in the original model. The need to define such features became apparent through
the process of formalising the model. The need to modify existing definitions also emerged as a
result of the formalisation process. This array of semi-formal definitions, be they restatements of
existing definitions or entirely new ones, lays the groundwork for the process-algebraic model.

3.1 Space Elastic Model

Recall the space elastic model from Section 2. A formal definition of the interface provided by
this model is given here. The definition is broken into a definition of coverage and a definition
of coverage-update. Let us say we observe a Comhordú system evolving from time t, and that an
entity e within the system begins sending a message to its environment at this time. Then at time
t′ = t + msgLatency, the actual coverage Ca of e for this observation is the maximum distance d
such that if there was an entity e′ within this distance of e at time t′, e′ would have received the
message sent by e at t. Now, let us assume the system further evolves and we observe it at time
t′′ = t′ + adaptNoti f . Then by this time, e is guaranteed by the space elastic model to know Ca
i.e. e will be notified of the coverage at time t′ within a time bound of adaptNoti f .

3.2 Safety Constraint

We reformulate the safety constraint in terms of a function minDistComp. The function applied
to modes i and j, minDistComp(i, j) yields the minimum distance by which entities in those
modes must be separated such that the entities are guaranteed to be compatible. The safety
constraint then reduces to the assertion that at all times, all pairs of entities in modes i, j are

5 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

separated by at least minDistComp(i, j). The function is symmetric. Since entities in fail safe
mode cannot cause incompatibilities, the function evaluates to 0 when mode F S is one of its
arguments, as per Equation 1.

∀m : M•minDistComp(m,F S) = 0 (1)

3.3 Reasoning about the Coverage

Ignore(e,i,s,e′, j,s′)
def
= i = F S∨ j = F S∨(e = e′)∨(dist(s,s′)

rangeOK(i,r)
def
= i = F S∨r > dmax(i)+ smax.(trans(i)+ period(i)
+ max(trans,adaptNoti f ))

> minDistComp(i, j)+ smax.(trans( j)+ period( j)

+ max(trans,adaptNoti f )+ 0.5msgLatency))c

trans
def
= setMax({trans(i)|i : M})

dmax(i)
def
= setMax({minDistComp(i, j)| j : M})

We have reasoned about various aspects of the coverage and arrived at the above constant
and function definitions that will be needed in the formal model. Ignore(e,i,s,e′, j,s′) asserts
whether a listener e in mode i and position s can ignore a message sent by e′ in mode j and
position s′. rangeOK(i,r) asserts whether the range r of a message sent by an entity in mode i
is sufficient. We assume an upper bound on the time it takes an entity in mode i to transition to
mode F S. We call this time trans(i). We then define trans as the maximum such time for any
mode. The function dmax(i) is the maximum of all the minimum distances of compatibility for
all mode pairs including i.

3.4 Mode Transitions

A relation  is defined over mode pairs such that i  j denotes the fact that an entity in mode i
can transition to be in mode j. We have as a feature of the system that i  F S for all non fail safe
modes. This condition is needed to ensure safety via the protocol. While transitioning between
modes, an entity will broadcast as if it were two entities in parallel, one broadcasting i messages,
the other broadcasting j messages. This idea is taken from the idea of “soft handovers” [15] in
the field of mobile cellular networks. In networks employing this idea, cell coverage overlaps
and users crossing the overlapping area between cells remain in the coverage of their original
cell while they connect to the new cell. The physical time it takes to transition from mode i to
mode j is given by ts(i, j), while the total wait time is given in Equation 2.

tw(i, j)
def
= max(msgLatency + max(adaptNoti f ,trans),ts(i, j)) (2)

Proc. FMIS 2011 6 / 17



ECEASST

4 The Modelling Language for Comhordú

In this section, the language TCBS’ will be presented. The language is strongly based on the
Timed Calculus of Broadcasting Systems (TCBS) [23] and has been influenced by the work in
[13]. Expressions in this language which constitute a formal Comhordú model will appear in
Section 5. The syntax of the language yields its set of terms, which are built inductively. A term
belongs to the language iff it can be constructed using the language base terms & constructors.
A process P is a closed term, i.e. one without any free variables. The structural operational
semantics of the language is given via four relations over processes. The ignore relation asserts
whether a process can ignore a value spoken by another process and essentially do nothing. The
input relation captures the behaviour of a process that can consume and use some value, thus
becoming a different process. The output relation applies to processes that can speak a value and
then become some other process. Novel to the timed version of the calculus, the delay relation
links processes such that one may delay and become the other. Given below is the inductively
built syntax of the TCBS’ language.

T ::= 0
∣∣ (in e)?T ∣∣ (out e)!T ∣∣ Takei∈I Ti ∣∣ if b then T ∣∣ A(~e) ∣∣ T( f ,g) ∣∣ (T | T ) ∣∣ del(d).T

The process 0 denotes the null process. It may delay indefinitely and ignores anything it hears.
It cannot evolve to become another process and cannot output any value. An input-prefixed
process (in e)?T is one which listens for a value matching the pattern of e. Since this is a process,
all free variables in T are bound by e. Once a value v is heard that matches e, all free variables
in e, and hence in T are bound to the matched values. The output prefixed process (out e)!P may
broadcast a value v, to which the expression e evaluates. Notice that e and P are closed here. Here
is a simple example to demonstrate the syntax so far. Let P

def
= (in [x,y,z])?(out (x + y + z))!0.

Assuming our language is defined over integers and lists of integers, we have that P listens for
a list of three integers, outputs their sum, and finally terminates. Let’s say P hears [1,2,3]. We

represent this by the input action P
[1,2,3]?
−−−−→P′′ where P′′ = (out (1+2+3))!0. Since 1+2+3 = 6,

P′′ then outputs 6 before terminating. This is represented by the output action P′′
6!−→ 0.

Takei∈I Pi denotes a choice over the set of process Ti indexed by elements of a set I. Roughly
speaking, this process can choose to behave as any of its constituent processes Ti. For finite sums,
this choice notation is often replaced by the infix operator + e.g. in P + Q. if b then P behaves
exactly as P does when b evaluates to true, and behaves as 0 otherwise. A(~e) is the parametrised
process on the vector of closed expressions ~e = (e1,e2,...,en). Each such process is given an
accompanying definition A(~x)

def
= TA where the free variables of TA are contained in ~x. P( f ,g) is

the process P with remap functions f and g applied to it. When P can speak v, this process can
speak f (v) and when this process hears u, the nested P hears g(u). del(d).P is a process that
must delay by d before it may perform any of the actions available to P. (P | Q) denotes two
process operating in parallel.

Table 1 defines the structural operational semantics (SOS) of the TCBS’ language. These are
the laws which govern how processes, i.e. expressions in the language, evolve. In this table,
comp is the symmetric function such that comp(w!,w?) = comp(w!,w;) = w!, comp(w?,w?) =
comp(w?,w;) = w?, comp(w;,w;) = w;, comp(d,d) = d and otherwise comp(α,β ) =⊥. When

7 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

Table 1: Structural operational semantics of TCBS’

Ignore (
w;−→) Input ( v?−→) Out put ( w!−→) Delay ( d−→)

0
w;−→ 0 0 d−→ 0

∀~v•w 6= e[~v/ f v(e)]
(in e)?T

w;−→ (in e)?T

v = e[~v/ f v(e)]

(in e)?T
v?−→ T [~v/ f v(e)]

(in e)?T
d−→ (in e)?T

(out e)!P
w;−→ (out e)!P

JeK = w

(out e)!P
w!−→ P

∀i ∈ I •Pi
w;−→ Pi

Takei∈I Pi
w;−→ Takei∈I Pi

∃i ∈ I •Pi
v?−→ P′

Takei∈I Pi
v?−→ P′

∃i ∈ I •Pi
w!−→ P′

Takei∈I Pi
w!−→ P′

∀i ∈ I •Pi
d−→ P′i

Takei∈I Pi
d−→ Takei∈I P′i

JbK = false

if b then P
w;−→ if b then P

JbK = false

if b then P
d−→ if b then P

P
w;−→ P

if b then P
w;−→ if b then P

P
v?−→ P′ JbK = true

if b then P
v?−→ P′

P
w!−→ P′ JbK = true

if b then P
w!−→ P′

P
d−→ P′ JbK = true

if b then P
d−→ P′

TA[~e/~x]
α−→ P′

A(~e)
α−→ P′

P
gw;
−−→ P

P( f ,g)
w;−→ P( f ,g)

P
gv?
−−→ P′

P( f ,g)
v?−→ P′

( f ,g)

P
w!−→ P′

P( f ,g)
f w!
−−→ P′

( f ,g)

P
d−→ P′

P( f ,g)
d−→ P′

( f ,g)

P
α−→ P′ Q

β
−→ Q′ comp(α,β ) 6=⊥

(P | Q)
comp(α,β )
−−−−−−→ (P′ | Q′)

P
α−→ P′

del(0).P
α−→ P′

d′ ≤ d

del(d).P
d′−→ del(d −d′).P

d > 0
del(d).P

w;−→ del(d).P
P

d′−→ P′

del(d).P
d+d′−−−→ P′

Proc. FMIS 2011 8 / 17



ECEASST

two concurrent process P and Q perform actions α and β concurrently, comp(α,β ) denotes the
composition of these actions i.e. the overall action of the process (P | Q). This is the action
seen by the external environment or equivalently an observer. There is a certain precedence
present here. Whenever an output is performed by either process, the observed action is output.
Otherwise, when there is at least one input, an input is observed to occur overall. Finally, when
only ignore actions are performed, the resultant action is also an ignore.

We assume that all terms A(~x) are given associated definitions TA where the free variables of
TA are a subset of the free variables of ~x. Also, the bound variables of TA are disjoint from the
free variables of ~x- this can always be achieved by alpha renaming. It is further assumed that all
such terms TA are guarded. A guarded term is one in which all parametrised process names of the
form A(~x) are part of some sub-expression whose structure is either an input prefix, and output
prefix, or a non-zero delay prefix [1]. This assumption prevents the occurrence of nonsensical
definitions such as A

def
= A. Notice that in the SOS, we only deal with processes i.e. closed terms.

5 Formal Description of the Model

The arguments of Section 3 and the language of Section 4, will now be amalgamated into one
coherent formal model of Comhordú. We begin with a description of the system at the highest
level. The system is initialised with three parameters. n : N represents the total number of entities;
S : R2[n] is a finite list of n points in the plane, which are the positions of the entities; V : R2[n]
are the velocities of the entities as two dimensional vectors. This system easily generalises to k
dimensions. Below is the expression for the system. It is given as n entities running in parallel.

Sys(n,S,V )
def
=

n

∏
i=1

E(i,si,vi)

Here, ∏ni=1 Pi is the fold of the binary parallel composition operator over the processes Pi indexed
by the set { j ∈N+| j ≤ n}. For the sake of formality, let us say that this fold is right associative.
Also, we note that si,vi are the elements of lists S,V respectively indexed by i.

The TCBS’ language is defined relative to a value type and a boolean type, each with its own
associated expression language. Here, the value type will be briefly introduced. The language
for boolean expressions Bex p will not be presented here, but is assumed to be well behaved. In
the following, u,v will range over values in the type Val, b over Bex p, c over Chan, s over Base
and e will be a process identifier of type N.

Base
def
= R∪R2 ∪N∪{A,W}

Val
def
= s

∣∣ c〈~s〉
Chan

def
= adaptNoti f

∣∣ bc ∣∣ coverage(e) ∣∣ f romRelay ∣∣ read ∣∣ start(e)∣∣ switch ∣∣ toServer
5.1 Top level Composition of an Entity

Let us now focus on the structure of the entity process. This process is divided into three logical
sub-components. The protocol is a high level description of the message sending/receiving be-

9 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

haviour of the entity. The environment buffers outgoing messages and filters incoming messages
based on the facts that messages take time to propagate through space and that not all messages
reach every entity. Finally, the mobile sub-process records in its parameters the position and
velocity of the entity, updating these periodically based on the mode of the entity. All entities
are initialised to be in mode F S.

E(e,s,v)
def
= (Protocol(e) | Environment(e) | Mobile(0,s,v))[/0](G)\{S}

G
def
= {start(e) 7→ start,coverage(e) 7→ coverage}

S
def
= {read,toServer,switch, f romRelay,adaptNoti f start,coverage}

We have used some syntactic shortcuts in this specification. The relabelling shortcut generates
a map from values to values given a finite map of channels in the form of a list. The idea is that if
one channel is mapped to another in the finite map, then all values constructed with this channel
are mapped to values constructed with the other channel. Formally, the syntactic sugar for the
remap is defined as follows.

P[LF ](LG)
def
= P( f ,g)

f (c〈xs〉) def= F(c)〈xs〉
g(c〈xs〉) def= G(c)〈xs〉

Here, F and G are functions from channel names to channel names. They are specified by the
finite lists of pairs LF and LG respectively. Pairs in each list are of the form c 7→ c′ such that no
c occurs as the first element of more than one pair in a list. Channels c not explicitly mapped by
these lists are assumed to map to themselves. The definition for F is given below. G follows an
analogous definition in terms of LG.

F(c) =
{

c′ if c 7→ c′ ∈ LF ;
c if ∀c′•c 7→ c′ /∈ LF .

We have also defined a restriction shortcut for channels. Here, it is desired that a process P
cannot send/receive messages to/from its environment over any channel in the set of channels S.
Since channels are modelled in this language by value constructors, this is the same as saying
that P cannot send to or receive from its environment any values constructed using the value
constructors in S. More formally:

P\{C} def= P[C′](C′)
C′

def
= {c 7→ τ|c ∈C}

5.2 Protocol Agents

Zoning in on the protocol process, which constitutes the bulk of the system, we are faced with a
parallel composition of six components. These six components can themselves be grouped into
two sets of 3: the active set, and the dormant set. In the active set are three processes. Active(i)

Proc. FMIS 2011 10 / 17



ECEASST

executes the task of periodically sending messages to its environment containing mode and posi-
tion information, as per the protocol description. LisAct(e,i) receives incoming messages from
the environment. If any of these messages cannot be ignored, then this process will initiate a
transition of the entity to fail safe mode via an internal broadcast to all protocol sub-components.
ANCheckA(i) performs a similar duty to the message listener but it instead listens for degra-
dations in coverage. The dormant set contains three processes also. The dormant process is so
called because it idles for a time until the entity decides to change mode. This decision is mod-
elled via input on the channel start. The process then evolves to a waiting process, which like
the active process periodically broadcasts both mode and position information.

The processes ANCheckD(i) and LisDorm(e,i) are analogous to Active(i) and LisAct(e,i)
respectively, only instead of initiating fail safe transitions on reception of a coverage degradation
or incompatible message, they initiate an abort broadcast which causes a rollback action of
the waiting process to its dormant state. The rollback is possible as opposed to a full fail safe
transition because the entity has not yet entered the waiting mode yet. The Protocol process is
parametrised on the id of the entity to which it belongs. All its components are initialised to fail
safe mode.

Protocol(e)
def
= (Active(0) | Dormant(0) | LisAct(e,0) | LisDorm(e,0)
| ANCheckA(0) | ANCheckD(0))\{trans,abort}

Active(i)
def
= (out read〈〉)!((in read〈s〉)?((out toServer〈A,i,s〉)!(del(p(i)).Active(i)+ A′)
+ A′)+ A′)+ A′

A′
def
= (in switch〈 j〉)?Active( j)

Dormant(i)
def
= Take j∈{k|i k}(in start〈 j〉)?Waiting(i, j,tw(i, j))+ D′(i)

D′(i)
def
= (in trans)?Waiting(i,0,trans(i))+(in abort)?Dormant(i)

Waiting(i, j,t)
def
= (out read〈〉)!(in read〈s〉)?((out toServer〈W, j,s〉)!W′(i, j,t)+ D′(i))+ D′(i)

W′(i, j,t)
def
= del(p( j)).Waiting(i, j,t − p( j))
+ del(t).(out switch〈 j〉)!Dormant( j)+ D′(i)

LisAct(e,i)
def
= (in f romRelay〈e′, j,s′〉)?(LisAct(e,i)
| MessHand(e,i,e′, j,s′))+ LA′(e)

11 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

MessHand(e,i,e′, j,s′)
def
= (out read〈〉)!(in read〈s〉)?MH′(e,i,s,e′, j,s′)

LA′(e)
def
= (in trans)?LisAct(e,0)+(in switch〈 j〉)?LisAct(e, j)

MH′(e,i,s,e′, j,s′)
def
= if ¬Ignore(e,i,s,e′, j,s′) then (out trans)!0

LisDorm(e,i)
def
= Take j∈{k|i k}(in start〈 j〉)?LW(e,i, j)+ LW′(e,i)

LW(e,i, j)
def
= (in f romRelay〈e′, j′,s′〉)?(LW(e,i, j)
| MessHand(e, j′,e′, j,s′)({trans7→abort},/0))
+ LW′(e,i)

LW′(e,i)
def
= (in trans)?LW(e,i,0)

+(in switch〈 j〉)?LisDorm(e, j)+(in abort)?LisDorm(e,i)

ANCheckA(i)
def
= (in adaptNoti f〈t,i,r〉)?(ANCheckA(i) | ANC′(i,r))
+(in switch〈 j〉)?ANCheckA( j)

ANC′(i,r)
def
= if ¬rangeOK(i,r) then (out trans)!0

ANCheckD(i)
def
= Take j∈{k|i k}(in start〈 j〉)?ANCheckW(i, j)

ANCheckW(i, j)
def
= (in adaptNoti f〈W, j,r〉)?(ANCheckW(i, j)
| ANC′( j,r)({trans7→abort},/0))+(in switch〈 j〉)?ANCheckD( j)
+(in trans)?ANCheckW(i,0)+(in abort)?ANCheckD(i)

5.3 Environment & Space Elastic Model

Here the focus is on processes which model the environment i.e. the propagation of messages
through space and the filtering of these messages based on their coverage. Also modelled in this
logical sub-component is the interface provided by the space elastic model, which provides any
sender with a coverage notification adaptNoti f time units after message sending is initiated.

Server(e) buffers outgoing messages. When an entity sends a message, it is caught by this
server process and held in a freshly created buffer process for a time of msgLatency, after which
it is then forwarded on to all other entities. RelayServ catches incoming messages and tests them
based on their coverage field. If the coverage of the sent message is less than the distance be-
tween sender and receiver, then the message is discarded. Otherwise, it is passed through to the
protocol process. Let it be noted that in an actual implementation of a Comhordú system, these
environment processes would not exist. Instead, they would be replaced by the actual environ-
ment. Furthermore, message fields such as the exact position of the sender at the time of delivery
of the message would not be included in the message, nor would the coverage- these would be
emergent properties. However, they are necessary here to encode the assumed behaviour of the
environment.

Proc. FMIS 2011 12 / 17



ECEASST

Environment(e)
def
= RelayServ | Server(e)

Server(e)
def
= (in toServer〈t,i,s〉)?(Server(e) | Buffer(e,t,i,s))

Buffer(e,t,i,s)
def
= del(msgLatency).(in coverage〈r〉)?(in read〈s′〉)?(out bc〈r,e,i,s,s′〉)!

del(adaptNoti f ).(out adaptNoti f〈t,i,r〉)!0

RelayServ
def
= (in bc〈r,e,i,s′,s′′〉)?(RelayServ | Relay(r,e,i,s′,s′′))

Relay(r,e,i,s′,s′′)
def
= (out read〈〉)!(in read〈s〉)?R′(r,s,s′′,e,i,s′)

R′(r,s,s′′,e,i,s′)
def
= if inRange(r,s,s′′) then (out f romRelay〈e,i,s′〉)!0

The predicate inRange used in these expressions asserts whether or not a message, whose
radius of delivery is specified, should be delivered to a given entity based on the position of this
entity and the sending entity. Equation 3 defines this predicate.

inRange(r,s,s′)
def
= (dist(s,s′)≤ r) (3)

5.4 Mobile Agent

The mobile agent is a simple process modelling the physical state of an entity. Mobile(i,s,v)
records via its parameters the position s, velocity v and mode i of the entity to which is belongs.
It periodically updates the position and velocity based on functions s′(i,s,v) and v′(i,s,v) respec-
tively. It is assumed here that the mode i along with the current position and velocity is enough
to determine the new position and velocity. However, this process, being independent of the rest
of the system, can easily be altered to change the way position and velocity are updated e.g. by
adding new parameters. The period of update is arbitrarily chosen and represents a discrete tick
in time. Since this process calculus does not allow continuous actions, this discrete approxima-
tion must suffice. We now take notice of the functions s′′ and v′′. These make an approximate
correction to the velocity and position when this process is interrupted by a mode change, which
is necessary since it is impossible to know how much time has elapsed since the last update.
The nature of such a correction will not be examined here, though it should be such that error is
minimised in some sense.

Mobile(i,s,v)
def
= MobTrack(i,s,v) | MobServ(s)

MobTrack(i,s,v)
def
= del(update).(out read〈s〉)!MobTrack(i,s′(i,s,v),v′(i,s,v))
+(in switch〈 j〉)?MobTrack(i,s′′(i,s,v),v′′(i,s,v))

MobServ(s)
def
= (in read〈〉)?((out read〈s〉)!MobServ(s)+ MS)+ MS

MS
def
= (in read〈s′〉)?MobServ(s′)

13 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

6 Related Work

In this section, we will briefly mention some related modelling languages to TCBS’ and highlight
their weaknesses, compared to TCBS’, in terms of their applicability to the Comhordú problem.
As mentioned earlier, TCBS’ is a variation on the existing TCBS of [23], which itself is an
extension of CBS [24]. The differences between TCBS’ and TCBS are mostly influenced by the
changes made to CBS in [13]. The advantage of TCBS’ over TCBS is the clarity of notation
achieved therein. Other formalisms were considered as alternatives to the timed broadcasting
calculus. UPPAAL [5] is a model checker for finite timed automata [3]. The advantage of using
UPPAAL to model a system is that certain system properties can be specified and machine-
checked. However, the finiteness restriction of UPPAAL does not accommodate a fully general
model and this has lead us towards the more powerful paradigm of process algebras. There are
a myriad of process algebras currently in existence. We narrow our attention only to those most
suitable.

Recently developed are a group of algebras for modelling wireless systems [18, 20, 17, 22, 25].
At first glance, these algebras seem ideal for the modelling task at hand. However, many of them
focus on low level aspects of the wireless network such as collision detection. This would suit
a formalised space elastic model but is too detailed for Comhordú. The languages also lack any
notion of time. A similar calculus that does include time is given in [19], but the time modelled
is in ticks rather than delays of real amounts and again the focus is on collisions. Long stand-
ing timed process algebras such as TCCS [29] and TCSP [10] were considered. However, the
weakness of these languages is that they do not include broadcast as a communication primi-
tive, whereas TCBS’ does, thus making it more suitable to the task of modelling an inherently
broadcast-based system than any of these other languages considered.

7 Conclusions & Future Work

In this paper a formalisation of the Comhordú model has been achieved. This formalisation
provides us with a clearer understanding of the model, removing any ambiguity from pre-existing
model descriptions. It paves the way for future verification work using model checkers. As a
general framework, the model also serves as a guide to the construction of model instances i.e.
formalisations of particular Comhordú systems. Finally, it has emerged through the process
of formalising the Comhordú system that some new concepts were required at the heart of the
model. In particular, there was the notion of “soft handover” from one mode to another, an idea
taken from the telecoms community; the safety constraint language was reduced to the simpler
notion of distance-based incompatibilities, which unlike expressions in the original language
seem satisfiable in general by the protocol alone; coverage zones were re-evaluated and deduced
from first principles, with some new constants and functions defined to yield expressions for
sufficient coverage, wait time and ignorable messages.

Let us now consider future explorations that may be carried out to extend this work. The
ultimate goal is to prove the general safety of the model, i.e. prove that for any Comhordú system
adhering to the Comhordú protocol, the safety constraint holds. As discussed earlier, to prove
this safety condition, it will be enough to prove that adherence to the Comhordú protocol implies

Proc. FMIS 2011 14 / 17



ECEASST

sufficient spacing of the entities according to the distance function supplied. Other properties of
the system also remain to be investigated such as those of liveness and deadlock. The intuition at
the moment is that we will develop a property logic enabling us to express such conditions. After
this, we can attempt proofs of certain properties by hand or we can develop some approximation
of this system in a model checker like UPPAAL & machine check these properties. It is expected
that both techniques will be employed. There have already been investigations performed on
the behaviour of the system via the application of the TCBS’ SOS laws to the formal system
expressions of Section 5 to yield traces through the system. Due to spatial limitations however,
these traces could not be included here.

Acknowledgements: We extend a special thanks to Matthew Hennessy for his insights and his
advice relating to this work. We also express our gratitude towards the anonymous reviewers of
this paper for their feedback and their time.

Bibliography

[1] L. Aceto, A. Ingólfsdóttir, K. G. Larsen, and J. Srba. Reactive systems: modelling, specifi-
cation and verification. Cambridge Univ Pr, 2007.

[2] M. Alighanbari, Y. Kuwata, and J. How. Coordination and Control of Multiple UAVs with
Timing Constraints and Loitering. In Proceedings ofAmerican Control Conference, 2003.

[3] R. Alur and D.L. Dill. A theory of timed automata* 1. Theoretical computer science,
126(2):183–235, 1994.

[4] J. Baber, J. Kolodko, T. Noel, M. Parent, and L. Vlacic. Cooperative autonomous driving:
intelligent vehicles sharing city roads. IEEE Robotics & Automation Magazine, 12(1):44–
49, 2005.

[5] Gerd Behrmann, Alexandre David, and Kim Larsen. A tutorial on uppaal. In Marco
Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time Sys-
tems, volume 3185 of Lecture Notes in Computer Science, pages 33–35. Springer Berlin /
Heidelberg, 2004.

[6] M. Bouroche. Real-Time Coordination of Mobile Autonomous Entities. PhD thesis, Uni-
versity of Dublin, Trinity College, 2007.

[7] M. Bouroche and V. Cahill. We don’t need to agree to coordinate. Workshop on Dependable
Network Computing and Mobile Systems (DNCMS’08), 1:47–51, October 2008.

[8] J. Cawkwell. A visually guided agv for use as passenger transport in urban areas. In
Intelligent Transportation Systems, 2000. Proceedings. 2000 IEEE, pages 311–315. IEEE,
2000.

[9] C.M. Clark. Dynamic robot networks: a coordination platform for multi-robot systems.
PhD thesis, Citeseer, 2004.

15 / 17 Volume 45 (2011)



A Process Algebraic Description of a Temporal Wireless Network Protocol

[10] J. Davies and S. Schneider. A brief history of timed csp. Theoretical Computer Science,
138(2):243–271, 1995.

[11] C.L. Fok, G.C. Roman, and G. Hackmann. A lightweight coordination middleware for
mobile computing. In Coordination Models and Languages, pages 135–151. Springer,
2004.

[12] V. Gervasi and G. Prencipe. Coordination without communication: the case of the flocking
problem. Discrete Applied Mathematics, 144(3):324–344, 2004.

[13] M. Hennessy and J. Rathke. Bisimulations for a calculus of broadcasting systems* 1.
Theoretical Computer Science, 200(1-2):225–260, 1998.

[14] C. Julien and G.C. Roman. Active coordination in ad hoc networks. In Coordination
Models and Languages, pages 199–215. Springer, 2004.

[15] R. Koodli and C.E. Perkins. Fast handovers and context transfers in mobile networks. ACM
SIGCOMM Computer Communication Review, 31(5):37–47, 2001.

[16] N. Kubota, Y. Nojima, N. Baba, F. Kojima, and T. Fukuda. Evolving pet robot with emo-
tional model. In Proceedings of the 2000 Congress on Evolutionary Computation, 2000.,
volume 2, pages 1231–1237. IEEE, 2000.

[17] I. Lanese and D. Sangiorgi. An operational semantics for a calculus for wireless systems.
Theoretical Computer Science, 411(19):1928–1948, 2010.

[18] M. Merro. An observational theory for mobile ad hoc networks. Electronic Notes in Theo-
retical Computer Science, 173:275–293, 2007.

[19] Massimo Merro and Eleonora Sibilio. A timed calculus for wireless systems. In Farhad
Arbab and Marjan Sirjani, editors, Fundamentals of Software Engineering, volume 5961 of
Lecture Notes in Computer Science, pages 228–243. Springer Berlin / Heidelberg, 2010.

[20] N. Mezzetti and D. Sangiorgi. Towards a calculus for wireless systems. Electronic Notes
in Theoretical Computer Science, 158:331–353, 2006.

[21] A.L. Murphy, G.P. Picco, and G.C. Roman. Lime: A middleware for physical and logi-
cal mobility. In International Conference On Distributed Computing Systems, page 0524.
Published by the IEEE Computer Society, 2001.

[22] S. Nanz and C. Hankin. A framework for security analysis of mobile wireless networks.
Theoretical Computer Science, 367(1-2):203–227, 2006.

[23] K. Prasad. Broadcasting in time. In Paolo Ciancarini and Chris Hankin, editors, Coordi-
nation Languages and Models, volume 1061 of Lecture Notes in Computer Science, pages
321–338. Springer Berlin / Heidelberg, 1996.

[24] KVS Prasad. A calculus of broadcasting systems. Science of Computer Programming,
25(2-3):285–327, 1995.

Proc. FMIS 2011 16 / 17



ECEASST

[25] KVS Prasad. A prospectus for mobile broadcasting systems. Electronic Notes in Theoreti-
cal Computer Science, 162:295–300, 2006.

[26] R.D. Schraft. Mechatronics and robotics for service applications. Robotics Automation
Magazine, IEEE, 1(4):31 –35, dec 1994.

[27] P. Verissimo and A. Casimiro. Event-driven support of real-time sentient objects. In Object-
Oriented Real-Time Dependable Systems, 2003. (WORDS 2003). Proceedings of the Eighth
International Workshop on, pages 2 – 9, jan. 2003.

[28] J. Woodcock and J. Davies. Using Z: specification, refinement, and proof, volume 39.
Prentice Hall, 1996.

[29] Wang Yi. Real-time behaviour of asynchronous agents. In J. Baeten and J. Klop, editors,
CONCUR ’90 Theories of Concurrency: Unification and Extension, volume 458 of Lecture
Notes in Computer Science, pages 502–520. Springer Berlin / Heidelberg, 1990.

17 / 17 Volume 45 (2011)


	Introduction
	Informal Description of the Comhordú System
	Properties of the Comhordú Model
	The Comhordú Protocol

	Towards a Formal Comhordú Model
	Space Elastic Model
	Safety Constraint
	Reasoning about the Coverage
	Mode Transitions

	The Modelling Language for Comhordú
	Formal Description of the Model
	Top level Composition of an Entity
	Protocol Agents
	Environment & Space Elastic Model
	Mobile Agent

	Related Work
	Conclusions & Future Work