A Process Algebra for Link Layer Protocols

Abstract

We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.

1 Introduction

The (data) link layer is the 2nd layer of the ISO/OSI model of computer networking [18]. Amongst others, it is responsible for the transfer of data between adjacent nodes in Wide Area Networks (WANs) and Local Area Networks (LANs).

Examples of link layer protocols are Ethernet for LANs [16], the Point-to-Point Protocol [24] and the High-Level Data Link Control protocol (e.g. [14]). Part of this layer are also multiple access protocols such as the Carrier-Sense Multiple Access with Collision Detection (CSMA/CD) protocol for re-transmission in Ethernet bus networks and hub networks, or the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol [17, 19] in wireless networks.

One of the unique characteristics of the link layer is that when devices attempt to use a medium simultaneously, collisions of messages occur. So, any modelling language and formal analysis of layer-2 protocols has to support such collisions. Moreover, some protocols are of probabilistic nature: CSMA/CA for example chooses time slots probabilistically with discrete uniform distribution.

As we are not aware of any formal framework with primitives for modelling data collisions, this paper introduces a process algebra for modelling and analysing link layer protocols. In Sect. 2 we present an algebra featuring a unique mechanism for modelling collisions, ‘hard-wired’ in the semantics. It is the nonprobabilistic fragment of the Algebra for Link Layer protocols (ALL), which we introduce in Sect. 3. In Sect. 4 we formulate packet delivery, a liveness property that ideally ought to hold for link layer protocols, either outright, or with a high probability. In Sect. 5 we use this framework to formally model and analyse the CSMA/CA protocol.

Our analysis confirms the hidden station problem for the version of CSMA/CA without virtual carrier sensing (Sect. 5.2). However, we also show that the version with virtual carrier sensing overcomes not only this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.

2 A Non-probabilistic Subalgebra

In this section we propose a timed process algebra that can model the collision of link layer messages, called frames.¹ It can be used for link layer protocols that do not feature probabilistic choice, and is inspired by the (Timed) Algebra for Wireless Networks ((T-)AWN) [2, 12, 13], a process algebra suitable for modelling and analysing protocols on layers 3 (network) and 4 (transport) of the OSI model.

The process algebra models a (wired or wireless) network as an encapsulated parallel composition of network nodes. Due to the nature of the protocols under consideration, on each node exactly one sequential process is running. The algebra features a discrete model of time, where each sequential process maintains a local variable holding its local clock value—an integer. We employ only one clock for each sequential process. All sequential processes in a network synchronise in taking time steps, and at each time step all local clocks advance by one unit. Since this means that all clocks are in sync and do not run at different speeds it is clear that we do not consider the problem of clock shift. For the rest, the variable behaves like any other variable maintained by a process: its value can be read when evaluating guards, thereby making progress time-dependant, and any value can be assigned to it, thereby resetting the local clock. Network nodes communicate with their direct neighbours—those nodes that are in transmission range. The algebra provides a mobility option that allows nodes to move in or out of transmission range. The encapsulation of the entire network inhibits communications between network nodes and the outside world, with the exception of the receipt and delivery of data packets from or to clients (the higher OSI layers).

2.1 A Language for Sequential Processes

The internal state of a process is determined, in part, by the values of certain data variables that are maintained by that process. To this end, we assume a data structure with several types, variables ranging over these types, operators and predicates. Predicate logic yields terms (or data expressions) and formulas to denote data values and statements about them. Our data structure always contains the types , , , , and of discrete time values, which we take to be integers, network layer data, messages, chunks of messages that take one time unit to transmit, node identifiers and sets of node identifiers. We further assume that there are variables of type and of type . In addition, we assume a set of process names. Each process name X comes with a defining equation

in which , are variables and $P$ is a sequential process expression defined by the grammar below. It may contain the variables as well as X. However, all occurrences of data variables in $P$ have to be bound.² The choice of the underlying data structure and the process names with their defining equations can be tailored to any particular application of our language.

The sequential process expressions are given by the following grammar:

Here X is a process name, a data expression of the same type as , $\varphi$ a data formula, an assignment of a data expression to a variable of the same type, a data expression of type , and , data variables of types , respectively.

Given a valuation of the data variables by concrete data values, the sequential process acts as $P$ if $\varphi$ evaluates to true, and deadlocks if $\varphi$ evaluates to false. In case $\varphi$ contains free variables that are not yet interpreted as data values, values are assigned to these variables in any way that satisfies $\varphi$, if possible. The process acts as $P$, but under an updated valuation of the data variable . The process $P\mathop {+}Q$ may act either as $P$ or as $Q$, depending on which of the two processes is able to act at all. In a context where both are able to act, it is not specified how the choice is made. The process $\alpha .P$ first performs the action $\alpha$ and subsequently acts as $P$. The above behaviour is identical to AWN, and many other standard process algebras. The action transmits (the data value bound to the expression) to all other network nodes within transmission range. The action models the injection by the network layer of a data packet to be transmitted to a destination . Technically, and are variables that will be bound to the obtained values upon receipt of a $\mathbf{newpkt}$. Data is delivered to the network layer by . In contrast to AWN, we do not have a primitive for receiving messages from neighbouring nodes, because our processes are always listening to neighbouring nodes, in parallel with anything else they do.

As in AWN, the internal state of a sequential process described by an expression $P$ is determined by $P$, together with a valuation $\xi$ associating values to variables maintained by this process. Valuations naturally extend to $\xi$-closed expressions—those in which all variables are either bound or in the domain of $\xi$. We denote the valuation that assigns the value v to the variable , and agrees with $\xi$ on all other variables, by . The valuation $\xi _{|S}$ agrees with $\xi$ on all variables and is undefined otherwise. Moreover we use as an abbreviation for , for suitable types.

To capture the durational nature of transmitting a message between network nodes, we model a message as a sequence of chunks, each of which takes one time unit to transmit. The function calculates the amount of time steps needed for a sending a message, i.e. it calculates the number of chunks. We employ the internal data type . The chunk indicates the c th fragment of a message m. Data conflicts—junk transmitted via the medium—is modelled by the special chunk , and the absence of an incoming chunk is modelled by .

Our process algebra maintains a variable of type , storing the fragment of the current message received so far.

As a value of this variable, indicates that the first c chunks of message m have been received in order; indicates that the last incoming chunk was not the expected (next) part of a message in progress, and indicates that the channel was idle during the last time step. The table on the right, with $*$ a wild card, shows how the value of evolves upon receiving a new chunk .

Specifications may refer to the data type only through the Boolean functions —having a single argument of type —and , defined by and . A guard evaluates to true iff a new message has just been received; evaluates to true iff in the last time slice the medium was idle.

The structural operational semantics of Table 1 describes how one internal state can evolve into another by performing an action. The set of actions consists of , , , , and internal actions $\tau \!$, for each choice of , , , and , where the first two actions are time consuming. On every time-consuming action, each process receives a chunk and updates the variable accordingly; moreover, the variable is incremented on all process expressions in a (complete) network synchronously.

Table 1. Structural operational semantics for sequential process expressions

Besides the special variables and , the formal semantics employs an internal variable that enumerates the chunks of split messages and is used to identify which chunk needs to be sent next. The variables , and are not meant to be changed by ALL specifications, e.g. by using assignments. We call them read-only and collect them in the set .

Let us have a closer look at the rules of Table 1.

The first two rules describe the sending of a message . Remember that calculates the time needed to send . The counter keeps track of the time passed already. The action occurs when the node transmits the fragment ; simultaneously, it receives the fragment .³ The counter is 0 before a message is sent, and is incremented before the transmission of each chunk. So, each chunk sent has the form . To ease readability we abbreviate by . In case the (already incremented) counter is strictly smaller than the number of chunks needed to send , another transmit-action is needed (Rule 1); if the last fragment has been sent () the process can continue to act as $P$ (Rule 2).

The actions and are instantaneous and model the submission of data d from the network layer, destined for , and the delivery of data d to the network layer, respectively. The process has also the possibility to wait, namely if no network layer instruction arrives.

Rule 6 defines a rule for assignment in a straightforward fashion; only the valuation of the variable is updated.

In Rules 7 and 8, which define recursion, is the valuation that only assigns the values to the variables , for $i=1,\ldots ,n$, and maintains the values of the variables , and . These rules state that a defined process X has the same transitions as the body p of its defining equation. In case of a -transition, the sequential process does not progress, and accordingly the recursion is not yet unfolded.

Most transition rules so far feature statements of the form where is a data expression. The application of the rule depends on being defined. Rule 9 covers all cases where the above rules cannot be applied since at least one data expression in an action $\alpha$ is not defined. A state $\xi ,P$ is unvalued, denoted by , if $P$ has the form , , or with either or or or some undefined. From such a state the process can merely wait.

A process $P+Q$ can wait only if both $P$ and $Q$ can do the same; if either $P$ or $Q$ can achieve ‘proper’ progress, the choice process $P+Q$ always chooses progress over waiting. A simple induction shows that if and then $P=P'$, $Q=Q'$ and $\zeta =\zeta '$.

The first rule of (12), describing the semantics of guards , is taken from AWN. Here says that $\zeta$ is an extension of $\xi$, i.e. a valuation that agrees with $\xi$ on all variables on which $\xi$ is defined, and evaluates other variables occurring free in $\varphi$, such that the formula $\varphi$ holds under $\zeta$. All variables not free in $\varphi$ and not evaluated by $\xi$ are also not evaluated by $\zeta$. Its negation says that no such extension exists, and thus, that $\varphi$ is false in the current state, no matter how we interpret the variables whose values are still undefined. If that is the case, the process $[\varphi ]p$ will idle by performing the action .

2.2 A Language for Node Expressions

We model network nodes in the context of a (wireless) network by node expressions of the form

Here is the address of the node, is a sequential process expression with a valuation $\xi$, and is the range of the node, defined as the set of nodes within transmission range of . Unlike AWN, the process algebra does not offer a parallel operator for combining sequential processes; such an operator is not needed due to the nature of link layer protocols.

In the semantics of this layer it is crucial to handle frame collisions. The idea is that all chunks sent are recorded, together with the respective recipient. In case a node receives more than one chunk at a time, a conflict is raised, as it is impossible to send two or more messages via the same medium at the same time.

The formal semantics for node expressions, presented in Table 2, uses transition labels , , , , and $\tau$, with partial functions , , and .

Table 2. Structural operational semantics for node expressions

All time-consuming actions on process level ( and ) are transformed into an action on node level: the first argument maps to if and only if the chunk is transmitted to . The second argument maps to if and only if the chunk is received on process level at node . For the sos-rules of Table 2 we use the set-theoretic presentation of partial functions. The two rules for $\mathbf{wait}$ set , as no chunks are transmitted; the rules for $\mathbf{transmit}$ allow a transmitted chunk to travel to all nodes within transmission range: . In case that during the transmission or waiting no chunk is received () we set ; otherwise , indicating that chunk is received by node .

The actions and as well as the internal actions $\tau$ are simply inherited by node expressions from the processes that run on these nodes.

The remaining rules of Table 2 model the mobility aspect of wireless networks; the rules are taken straight from AWN [12, 13]. We allow actions and for modelling a change in network topology. These actions can be thought of as occurring nondeterministically, or as actions instigated by the environment of the modelled network protocol. In this formalisation node is in the range of node , meaning that can receive messages sent by , if and only if is in the range of . To break this symmetry, one just skips the last four rules of Table 2 and replaces the synchronisation rules for connect and disconnect in Table 3 by interleaving rules (like the ones for deliver, newpkt and $\tau$) [12]. For some applications a wired or non-mobile network need to be considered. In such cases the last six rules of Table 2 are dropped.

Whether a node receives its own transmissions depends on whether . Only if our process algebra will disallow the transmission from and to a single node at the same time, yielding a .

2.3 A Language for Networks

A partial network is modelled by a parallel composition $\Vert$ of node expressions, one for every node in the network. A complete network is a partial network within an encapsulation operator $[\_]$, which limits the communication between network nodes and the outside world to the receipt and delivery of data packets to and from the network layer.

Table 3. Structural operational semantics for network expressions

The syntax of networks is described by the following grammar:

with . Here $M_S^T$ models a partial network describing the behaviour of all nodes . The set T contains the identifiers of all nodes that are part of the complete network. This grammar guarantees that node identifiers of node expressions—the first component of —are unique.

The operational semantics of network expressions is given in Table 3. Internal actions $\tau$ as well as the actions and are interleaved in the parallel composition of nodes that makes up a network, and then lifted to encapsulated networks (Line 1 of Table 3).

Actions traffic and (dis)connect are synchronised. The rule for synchronising the action (Line 3), the only action that consumes time on the network layer, uses the union $\uplus$ of partial functions. It is formally defined as

The synchronisation of the sets and has the following intuition: if a node identifier is in both and then there exist two nodes that transmit to node at the same time, and therefore a frame collision occurs. In our algebra this is modelled by the special chunk . The sos rules of Tables 2 and 3 guarantee that there cannot be collisions within the set of received chunks . The reason is that each node merely contributes to a chunk for itself; it can be the chunk though. Therefore we could have written instead of in the sixth rule of Table 3.

The last rule propagates a -action of a partial network M to a complete network [M]. By then consists of all chunks (after collision detection) that are being transmitted by any member in the network, and consists of all chunks that are received. The condition determines the content of the messages in . The -actions become internal at this level, as they cannot be steered by the outside world; all that is left is a time-step tick.

2.4 Results on the Process Algebra

As for the process algebra T-AWN [2], but with a slightly simplified proof, one can show that our processes have no time deadlocks:

Theorem 2.1

A complete network N in our process algebra always admits a transition, independently of the outside environment, i.e. $\forall N, \exists a$ such that and .

More precisely, either , or or .

The following results (statements and proofs) are very similar to the results about the process algebra AWN, as presented in [13]. A rich body of foundational meta theory of process algebra allows the transfer of the results to our setting, without too much overhead work.

Identical to AWN and its timed version T-AWN, our process algebra admits a translation into one without data structures (although we cannot describe the target algebra without using data structures). The idea is to replace any variable by all possible values it can take. The target algebra differs from the original only on the level of sequential processes; the subsequent layers are unchanged. The construction closely follows the one given in the appendix of [2]. The inductive definition contains the rules

and

.

Most other rules require extra operators that keep track of the passage of time and the evolution of other internal variables. The resulting process algebra has a structural operational semantics in the (infinitary) de Simone format, generating the same transition system—up to strong bisimilarity, —as the original. It follows that , and many other semantic equivalences, are congruences on our language [23].

Theorem 2.2

Strong bisimilarity is a congruence for all operators of our language.

This is a deep result that usually takes many pages to establish (e.g. [25]). Here we get it directly from the existing theory on structural operational semantics, as a result of carefully designing our language within the disciplined framework described by de Simone [23].    $\square$

Theorem 2.3

The operator $\Vert$ is associative and commutative, up to  .

Proof

The operational rules for this operator fits a format presented in [6], guaranteeing associativity up to . The ASSOC-de Simone format of [6] applies to all transition system specifications (TSSs) in de Simone format, and allows 7 different types of rules (named 1–7) for the operators in question. Our TSS is in de Simone format; the four rules for $\Vert$ of Table 3 are of types 1, 2 and 7, respectively. To be precise, it has rules $1_a$ and $2_a$ for , rules $7_{(a,b)}$ for

and rules $7_{(c,c)}$ for . Moreover, the partial communication function is given by and $\gamma (c,c)=c$. The main result of [6] is that an operator is guaranteed to be associative, provided that $\gamma$ is associative and six conditions are fulfilled. In the absence of rules of types 3, 4, 5 and 6, five of these conditions are trivially fulfilled, and the remaining one reduces to

$$\begin{aligned} 7_{(a,b)} \Rightarrow (1_a \Leftrightarrow 2_b) \wedge (2_a \Leftrightarrow 2_{\gamma (a,b)}) \wedge (1_b \Leftrightarrow 1_{\gamma (a,b)})\, . \end{aligned}$$

Here $1_a$ says that rule $1_a$ is present, etc. This condition is trivially met for $\Vert$ as there neither exists a rule of the form nor of the form , or $1_c$, $2_c$ with c as above. As on traffic actions $\gamma$ is basically the union of partial functions ($\uplus$), where a collision in domains is indicated by an error , it is straightforward to prove associativity of $\gamma$.

Commutativity of $\Vert$ follows by symmetry of the sos rules.    $\square$

3 An Algebra for Link Layer Protocols

We now introduce ALL, the Algebra for Link Layer protocols. It is obtained from the process algebra presented in the previous section by the addition of a probabilistic choice operator $\bigoplus _{0}^n$. As a consequence, the semantics of the algebra is no longer a labelled transition system, but a probabilistic labelled transition system (pLTS) [8]. This is a triple , where

• (i) S is a set of states

• (ii) is a set of actions

• (iii) , where is the set of all (discrete) probability distributions over S: functions $\varDelta :S\rightarrow [0,1]$ with $\sum _{s\in S}\varDelta (s)=1$.

As with LTSs, we usually write instead of $(s,\alpha ,\varDelta ) \in {\rightarrow }$. The point distribution $\delta _s$, for $s\in S$, is the distribution with $\delta _s(s)=1$. We simply write for . An LTS may be viewed as a degenerate pLTS, in which only point distributions occur. For a uniform distribution over $s_0,\dots ,s_n\in S$ we write . The pLTS associated to ALL takes S to be the disjoint union of the pairs $\xi ,P$, with $P$ a sequential process expression, and the network expressions. is the collection of transition labels, and $\rightarrow$ consists of the transitions derivable from the structural operational semantics of the language.

Rules (1)–(6), (9), (11) and (12) of Table 1 are adopted to ALL unchanged, whereas in Rules (7), (8) and (10) the state $\zeta ,P'$ (or $\zeta ,Q'$) is replaced by an arbitrary distribution $\varDelta$. Add to those the following rule for the probabilistic choice operator:

Here the data variable i may occur in P. The rules of Tables 2 and 3 are adapted to ALL unchanged, except that $P'$, $M'$ and $N'$ are now replaced by arbitrary distributions over sequential processes and network expressions, respectively. Here we adapt the convention that a unary or binary operation on states lifts to distributions in the standard manner. For example, if $\varDelta$ is a distribution over sequential processes, and , then describes the distribution over node expressions that only has probability mass on nodes with address and range R, and for which the probability of is $\varDelta (P)$. Likewise, if $\varDelta$ and $\varTheta$ are distributions over network expressions, then $\varDelta \Vert \varTheta$ is the distribution over network expressions of the form $M\Vert N$, where $(\varDelta \Vert \varTheta )(M\Vert N) = \varDelta (M)\cdot \varTheta (N)$.

4 Formalising Liveness Properties of Link Layer Protocols

Link layer protocols communicate with the network layer through the actions and . The typical liveness property expected of a link layer protocol is that if the network layer at node injects a data packet d for delivery at destination then this packet is delivered eventually. In terms of our process algebra, this says that every execution of the action ought to be followed by the action . This property can be formalised in Linear-time Temporal Logic [22] as

(1)

for any and . This formula has the shape , and is called an eventuality property in [22]. It says that whenever we reach a state in which the precondition $\phi ^{ pre}$ is satisfied, this state will surely be followed by a state were the postcondition $\phi ^{ post}$ holds. In [7, 13] it is explained how action occurrences can be seen or encoded as state-based conditions. Here we will not define how to interpret general LTL-formula in pLTSs, but below we do this for eventuality properties with specific choices of $\phi ^{ pre}$ and $\phi ^{ post}$.

Formula (1) is too strong and does not hold in general: in case the nodes and are not within transmission range of each other, the delivery of messages from to is doomed to fail. We need to postulate two side conditions to make this liveness property plausible. Firstly, when the request to deliver the message comes in, needs to be connected to . We introduce the predicate to express this, and hence take $\phi ^{ pre}$ to be . Secondly, we assume that the link between and does not break until the message is delivered. As remarked in [13], such a side condition can be formalised by taking $\phi ^{ post}$ to be . Thus the liveness property we are after is

(2)

We now define the validity of eventuality properties . Here $\phi ^{ pre}$ and $\phi ^{ post}$ denote sets of transitions and actions, respectively, and hold if one of the transitions or actions in the set occurs. In (2), $\phi ^{ pre}$ denotes the transitions with label that occur when the side condition is met, whereas is a set of actions.

A path in a pLTS is an alternating sequence $s_0,\alpha _1,s_1,\alpha _2,\dots$ of states and actions, starting with a state and either being infinite or ending with a state, such that there is a transition with $\varDelta _{i+1}(s_{i+1})>0$ for each i. The path is rooted if it starts with a state marked as ‘initial’, and complete if either it is infinite, or there is no transition starting from its last state. A state or transition is reachable if it occurs in a rooted path.

In a pLTS with an initial state, an eventually formula , with $\phi ^{ pre}$ and $\phi ^{ post}$ denoting sets of transitions and actions, holds outright if all complete paths starting with a reachable transition from $\phi ^{ pre}$ contain a transition with a label from $\phi ^{ post}$.

Definitions 3 and 5 in [9] define the set of probabilities that a pLTS with an initial state will ever execute the action $\omega$. One obtains a set of probabilities rather than a single probability due to the possibility of nondeterministic choice. This definition generalises to sets of actions $\phi ^{ post}$ (seen as disjunctions) by first renaming all actions in such a set into $\omega$. It also generalises trivially to pLTSs with an initial transition. For t a transition in a pLTS, let $Prob (t,\phi ^{ post})$ be the infimum of the set of probabilities that the pLTS in which t is taken to be the initial transition will ever execute $\phi ^{ post}$. Now in a pLTS with an initial state, an eventually formula holds with probability at least p if for all reachable transitions t in $\phi ^{ pre}$ we have $Prob (t,\phi ^{ post})\ge p$.

Possible correctness criteria for link layer protocols are that the liveness property (2) either holds outright, holds with probability 1, or at least holds with probability p for a sufficiently high value of p.

Sometimes we are content to establish that (2) holds under the additional assumptions that the network is stable until our packet is delivered, meaning that no links between any nodes are broken or established, and/or that the network layer refrains from injecting more packets. This is modelled by taking

(3)

We will refer to this version of (2) as the weak packet delivery property. Packet delivery is the strengthening without $\mathbf{newpkt}(*,*)$ in (3), i.e. not assuming that the network layer refrains from injecting more packets.

5 Modelling and Analysing the CSMA/CA Protocol

In this section we model two versions of the CSMA/CA protocol, using the process algebra ALL. Moreover, we briefly discuss some results we obtained while analysing these protocols.

The Carrier-Sense Multiple Access (CSMA) protocol is a media access control (MAC) protocol in which a node verifies the absence of other traffic before transmitting on a shared transmission medium. If a carrier is sensed, the node waits for the transmission in progress to end before initiating its own transmission. Using CSMA, multiple nodes may, in turn, send and receive on the same medium. Transmissions by one node are generally received by all other nodes connected to the medium.

The CSMA protocol with Collision Avoidance (CSMA/CA) [17, 19]⁴ improves the performance of CSMA. If the transmission medium is sensed busy before transmission then the transmission is deferred for a random time interval. This interval reduces the likelihood that two or more nodes waiting to transmit will simultaneously begin transmission upon termination of the detected transmission. CSMA/CA is used, for example, in Wi-Fi.

It is well known that CSMA/CA suffers from the hidden station problem (see Sect. 5.2). To overcome this problem, CSMA/CA is often supplemented by the request-to-send/clear-to-send (RTS/CTS) handshaking [19]. This mechanism is known as the IEEE 802.11 RTS/CTS exchange, or virtual carrier sensing. While this extension reduces the amount of collisions, wireless 802.11 implementations do not typically implement RTS/CTS for all transmissions because the transmission overhead is too great for small data transfers.

We use the process algebra ALL to model both the CSMA/CA without and with virtual carrier sensing.

5.1 A Formal Model for CSMA/CA

Our formal specification of CSMA/CA consists of four short processes written in ALL. It is precise and free of ambiguities—one of the many advantages formal methods provide, in contrast to specifications written in English prose.

The syntax of ALL is intended to look like pseudo code, and it is our belief that the specification can easily be read and understood by software engineers, who may or may not have experience with process algebra.

As the underlying data structure of our model is straightforward, we do not present it explicitly, but introduce it while describing the different processes.

The basic process , depicted in Process 1, is the protocol’s entry point.

This process maintains a single data variable in which it stores its own identity. It waits until either it receives a request from the network layer to transmit a packet to destination , or it receives from another node in the network a CSMA message (data frame) destined for itself.

In case of a newly injected data packet (Line 1), the process is called; this process (described below) initiates the sending of the message via the medium. When passing the message on to we use a function that generates a message in a format used by the protocol: next to the header fields (from which we abstract) it contains the injected as well as the designated receiver and the sender —the current node.

In case of an incoming destined for this node (the third argument carrying the destination is ) (Line 2)—any other incoming message is ignored by this process—the is handed over to the network layer () followed by the transmission of an acknowledgement back to the sender of the message (). CSMA/CA requires a short period of idling medium before sending the acknowledgement: in [19] this interval is called short interframe space (). The process waits until the time of the interframe spacing has passed, and then transmits the acknowledgement. The acknowledgement sent is not always received by , e.g. due to data collision; therefore could send the same message again (see Process 4) and could deliver the same data to the network layer again.

The process (Process 2) initiates the sending of a message via the medium. Next to the variable , which is maintained by all processes, it maintains the variable and : stores the number of attempts already made to send message . When the process is called the first time for a message (Line 1 of Process 1) the value of is 0.

The constant specifies the maximum number of attempts the protocol is allowed to retransmit the same message. If the limit is not yet reached (Line 1) the message is sent. As mentioned above, CSMA/CA defers messages for a random time interval to avoid collision. The node must start transmission within the contention window , a.k.a. backoff time. is calculated in Line 2; it increases exponentially.⁵ After is determined, the process is called, which performs the actual transmit-action. In case the maximum number of retransmits is reached (Line 4), the process notifies the network layer and restarts the protocol, awaiting new instructions from the application layer, or a new incoming message.

Process 3 takes care of the actual transmission of . However, the protocol has a complicated procedure when to send this message.

First, the process senses the medium and awaits the point in time when it is idle (Line 6). In case, before this happens, it receives from another node in the network a CSMA message destined for itself (Line 1), this message is handled just as in Process 1, except that after acknowledging this message the protocol returns to Process 3.

To guarantee a gap between messages sent via the medium, CSMA/CA (as well as other protocols) specifies the distributed (coordination function) interframe space (), which is usually small,⁶ but larger than , so that acknowledgements get priority over new data frames. When the medium becomes busy during the interframe space, another node started transmitting and the process goes back to listening to the medium (Line 9). In case nothing happens on the medium and the end of the interframe space is reached (Line 10), the process determines the actual time to start transmitting the message, taking the backoff time into account (Line 11). If the medium is idle for the entire backoff period (Line 15), the message is transmitted (Line 16), and the process calls the process that will await an acknowledgement from the recipient of (Line 17); the third argument specifies the maximum time the process should wait for such an acknowledgement. (As mentioned before an acknowledgement may never arrive.) If another node transmits on the medium during the backoff period, the protocol restarts the routine (Lines 13 and 14), with an adjusted backoff value —the process already started waiting and should not be punished when the waiting is restarted; this update guarantees fairness of the protocol.

The process awaiting an acknowledgement (Process 4) is straightforward. It waits until either it receives a CSMA message destined for itself (Line 1), or it receives an acknowledgement (Line 6), or it has waited for this acknowledgement as long as it is going to (Line 8).

In the first case, the message is handled just as in Process 1, except that after acknowledging this message the protocol returns to Process 4. In the second case the network layer is informed that the sending of was successful and the process loops back to Process 1 (Line 7). Line 8 describes the situation where no acknowledgement message arrives and the process times out. Here CSMA/CA retries to send the message; the counter is incremented.

5.2 The Hidden Station Problem

As mentioned in the introduction to this section, CSMA/CA suffers from the hidden station problem. This refers to the situation where two nodes A and C are not within transmission range of each other, while a node B is in range of both. In this situation C may be transmitting to B, but A is not able to sense this, and thus may start a transmission to B at roughly the same time, leading to data collisions at B.

While CSMA/CA is not able to avoid such collisions as a whole—it is always possible that two (or more) nodes hidden from each other happen to (randomly) choose the same backoff time to send messages—it is the exponential growth of the backoff slots that makes the problem less pressing in the long run, as the following theorem shows.

Theorem 5.1

If then weak packet delivery holds with probability 1.

Proof sketch

Since the number of messages that nodes transmit is bounded, and all nodes select random times to start transmitting out of an increasing longer time span, with probability 1 each message will eventually go through. $\Box$

In practice, is set to a value that is not high enough to approximate the idea behind the above proof. In fact, the transmission time of a single message may be larger than the maximal backoff period allowed. For this reason the hidden station problem does occur when running the CSMA/CA protocol, as studies have shown [5]. Nevertheless, the above analysis still shows that link layer protocols can be formally analysed by process algebra in general, and ALL in particular.

Fig. 1.

RTS/CTS exchange

5.3 A Formal Model for CSMA/CA with Virtual Carrier Sensing

To overcome the hidden station problem the usage of a request-to-send/clear-to-send (RTS/CTS) handshaking [19] mechanism is available. This mechanism is also known as virtual carrier sensing. The exchange of RTS/CTS messages happens just before the actual data is sent, see Fig. 1. The mechanism serves two purposes: (a) As the RTS and CTS messages are very short—they only contain two node identifiers as well as a natural number indicating the time it will take to send the actual (plus overhead)—the likelihood of a collision is reduced. (b) While the handshaking does not help with solving the hidden station problem for the RTS message itself, it avoids the problem for the sending of . The reason is that a hidden node, which could interfere with the sending of will receive the CTS message from the designated recipient of , and the hidden node will remain silent until the has been sent.

As for the CSMA/CA protocol we have modelled this extension in ALL, based on the model of CSMA/CA we presented earlier.

Our extended model uses two functions to generate and messages, respectively. The signature of both is . The first argument carries the sender (source) of the message, the second the indented destination, and the third argument a duration (time period) of silence that is requested/granted. For example, before the message is transmitted, the time period is calculated by

The calculation is straightforward as it follows the protocol logic and determines the amount of time needed until the acknowledgement would be received (see Fig. 2). After the message has been received the medium should be idle for the interframe space ; then a message is sent back, which takes time ; then another interframe space is needed, followed by the actual transmission of the message—the sending will take time units; after the message is received (hopefully) another interframe space is required before the acknowledgement is sent back.

Fig. 2.

The use of virtual channel sensing using CSMA/CA [3]

Process 2 remains essentially unchanged; it is merely equipped with the destination of the message that needs to be transmitted, and an additional timed variable . These variables are not used in this process, but required later on. Variable holds the point in time until the process should not transmit any or message. This period of silence is necessary as the node figures out that until time another node will transmit message(s).⁷

Process 5 is the modified version of Process 1. Identical to Process 1 it awaits an instruction from the network layer, or an incoming CSMA message destined for itself. Lines 1–3 are identical to Process 1. Lines 4–11 handle the two new message types. In case an message is received that is intended for another recipient () the node concludes that another node wants to use the medium for the amount of time units; the process updates the variable if needed, indicating the period the node should remain silent, by taking the maximum of the current value of , and , the point in time until the sender of the message requires the medium. The same behaviour occurs if a message is received that is not intended for the node itself (Line 4). If the incoming message is an message intended for the node itself (Line 6) by default the node answers with a clear-to-send message back to the sender (Line 9). However, when the receiver of the has knowledge about other nodes requiring the medium (), a clear-to-send cannot be granted, and the request is dropped (Line 6). Similar to the sending of an acknowledgement (Line 2), the process waits for the short interframe space () before sending the CTS (Line 6). Line 8 handles the case where the medium becomes busy () during this period; also here a clear-to-send cannot be granted, and the request is dropped.⁸ Only when the medium stays idle during the entire interframe space the node can inform the source of the message that the medium is clear to send; the is transmitted in Line 9. The time a receiver of this message has to be silent is adjusted by deducting the time elapsed before this happens. In Line 10 the process resets to remind itself not to issue any message until the present exchange has been completed.⁹

Process 6 is the modified version of Process 3. The goal of this process is to send an message (Line 22). Before it can start its work, it waits until the medium is idle, and any time it is required to be silent has elapsed (Line 11). Until this happens incoming data frames, or messages are treated just as in Process 5: Lines 1–10 copy Lines 2–11 of Process 5, except that afterwards the process returns to itself. Then Lines 12–20 are copied from Lines 7–15 from Process 3. Line 21 calculates the time other nodes ought to keep silent when receiving the message, and Line 23 passes control to the process , which awaits a response to the message transmitted in Line 22. The fourth argument of specifies the maximum time that process should wait for such a response; a good value for is .

Process listens for this time to a message with source and destination . In case the expected message arrives in time (Line 1), the node waits for a time (Line 2) and then transmits the data frame and proceeds to await an acknowledgement (Line 3). The fourth argument of specifies the maximum time the process should wait for such an acknowledgement; a good value for is . If the message does not arrive in time (Line 6), the process returns to to send another message, while incrementing the counter (Line 7). While waiting for the message, any incoming or message destined for another node is treated exactly as in Process 5 (Lines 4–5). Incoming data frames cannot arrive when this process is running, and incoming messages to are ignored.

Process 8 handles the receipt of an acknowledgement in response to a successful data transmission. If an acknowledgement arrives, it must be from the node to which has transmitted a data frame. In that case (Line 1), the network layer is informed that the sending of was successful and the process loops back to Process 5 (Line 2). Line 5 describes the situation where no acknowledgement message arrives and the process times out. Also here CSMA/CA retries to send the message; the counter is incremented. Lines 3–4 describe the usual handling of incoming or messages destined for another node.

5.4 The Exposed Station Problem

Another source of collisions in CSMA/CA is the well-known exposed station problem. This refers to a linear topology $A - B - C - D$, where an unending stream of messages between C and D interferes with attempts by A to get a message across to B. In the default CSMA/CA protocol as formalised in Sect. 5.1, transmissions from A to B may perpetually collide at B with transmissions from C destined for D. CSMA/CA with virtual carrier sensing mitigates this problem, for a sent by B in response to an sent by A will tell C to keep silent for the required duration. In fact, we can show that in the above topology, if then packet delivery holds with probability 1. A non-probabilistic guarantee cannot be given since nodes A and C could behave in the same way, meaning if one node is sending out a message the other does the same at the very same moment, and if one is silent the other remains silent as well. In this scenario all messages to be sent are doomed.

Based on our formalisation, we can prove that once the RTS/CTS handshake has been successfully concluded, meaning that all nodes within range of the intended recipient have received the , then packet delivery holds outright. So the only problem left is to achieve a successful RTS/CTS handshake. Since and messages are rather short, even by modest values of it becomes likely that such messages do not collide.

In spite of this, CSMA/CA with (or without) virtual channel sensing cannot achieve packet delivery with probability 1 for general topologies. Assume the following network topology

Here it may happen that one of the $C_i$s is always busy transmitting a large message to $D_i$; any given $C_i$ is occasionally silent (not sending any message), but then one of the others is transmitting. As $C_i$ is disconnected from $C_j$, for $j\ne i$, coordination between the nodes is impossible. As a consequence, the medium at A will always be busy, so that A cannot send an message from B.

6 Related Work

The CSMA protocol in its different variants has been analysed with different formalisms in the past.

Multiple analyses were performed for the CSMA/CD protocol (CSMA with collision detection), a predecessor of CSMA/CA that has a constant backoff, i.e. the backoff time is not increased exponentially, see [10, 11, 20, 21, 26]. In all these approaches frame collisions have to be modelled explicitly, as part of the protocol description. In contrast, our approach handles collisions in the semantics; thereby achieving a clear separation between protocol specifications and link layer behaviour.

Duflot et al. [10, 11] use probabilistic timed automata (PTAs) to model the protocol, and use probabilistic model checking (PRISM) and approximate model checking (APMC) for their analysis. The model explained in [26] is based on PTAs as well, but uses the model checker Uppaal as verification tool. These approaches, although formal, have very little in common with our approach. On the one hand it is not easy to change the model from CSMA/CD to CSMA/CA, as the latter requires unbounded data structures (or alike) to model the exponential backoff. On the other hand, as usual, model checking suffers from state space explosion and only small networks (usually fewer than ten nodes) can be analysed. This is sufficient and convenient when it comes to finding counter examples, but these approaches cannot provide guarantees for arbitrary network topologies, as ours does.

Jensen et al. [20] use models of CSMA/CD to compare the tools SPIN and Uppaal. Their models are much more abstract than ours. It is proven that no collisions will ever occur, without stating the exact conditions under which this statement holds.

To the best of our knowledge, Parrow [21] is the only one who used process algebra (CCS) to model and analyse CSMA. His untimed model of CSMA/CD is extremely abstract and the analysis performed is limited to two nodes only, avoiding scenarios such as the hidden station problem.

There are far fewer formal analyses techniques available when it comes to CSMA/CA (with and without virtual medium sensing). Traditional approaches to the analysis of network protocols are simulation and test-bed experiments. This is also the case for CSMA/CA (e.g. [4]). While these are important and valid methods for protocol evaluation, in particular for quantitative performance evaluation, they have limitations in regards to the evaluation of basic protocol correctness properties.

Following the spirit of the above-mentioned research of model checking CSMA, Fruth [15] analyses CSMA/CA using PTAs and PRISM. He considers properties such as the minimum probability of two nodes successfully completing their transmissions, and maximum expected number of collisions until two nodes have successfully completed their transmissions. As before, this analysis technique does not scale; in [15] the experiments are limited to two contending nodes only.

Beyond model checking, simulation and test-bed experiments, we are only aware of two other formal approaches. In [1] Markov chains are used to derive an accurate, analytical model to compute the throughput of CSMA/CA. Calculating throughput is an orthogonal task to our vision of proving (functional) correctness.

An approach aiming at proving the correctness of CSMA/CA with virtual carrier sensing (RTS/CTS), and hence related to ours, is presented in [3]. Based on stochastic bigraphs with sharing it uses rewrite rules to analyse quantitative properties. Although it is an approach that is capable to analyse arbitrary topologies, to apply the rewrite rules a particular topology needs to be modelled by a directed acyclic graph structure, which is part of the bigraph.

7 Conclusion

In this paper we have proposed a novel process algebra, called ALL, that can be used to model, verify and analyse link layer protocols. Since we aimed at a process algebra featuring aspects of the link layer such as frame collisions, as well as arbitrary data structures (to model a rich class of protocols), we could not use any of the existing algebras. The design of ALL is layered. The first layer allows modelling protocols in some sort of pseudo code, which hopefully makes our approach accessible for network and software researchers/engineers. The other layers are mainly for giving a formal semantics to the language. The layer of partial network expressions, the third layer, provides a unique and sophisticated mechanism for modelling the collision of frames. As it is hard-wired in the semantics there is no need to model collisions manually when modelling a protocol, as it was done before [21]. Next to primitives needed for modelling link layer protocols (e.g. transmit) and standard operators of process algebra (e.g. nondeterministic choice), ALL provides an operator for probabilistic choice.

This operator is needed to model aspects of link layer protocols such as the exponential backoff for the Carrier-Sense Multiple Access with Collision Avoidance protocol, the case study we have chosen to demonstrate the applicability of ALL. We have modelled and analysed two versions of CSMA/CA, without and with virtual carrier sensing. Our analysis has confirmed the hidden station problem for the version without virtual carrier sensing. However, we have also shown that the version with virtual carrier sensing overcomes not only this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.

To perform this analysis we had to formalise suitable liveness properties for link layer protocols specified in our framework.