A Process Algebra for Link Layer Protocols

TL;DR

This paper introduces a process algebra tailored for link layer protocols, enabling formal modeling of frame collisions and analysis of CSMA/CA variants, revealing their strengths and limitations in handling specific network problems.

Contribution

It presents a novel process algebra for link layer protocols with mechanisms for modeling collisions and formalizes liveness properties, applied to analyze CSMA/CA protocols.

Findings

Virtual carrier sensing overcomes hidden and exposed station problems

Protocol cannot guarantee packet delivery even with probability 1

Analysis confirms effectiveness of virtual sensing in specific scenarios

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.

Tables

Table 1. Table 1: Structural operational semantics for sequential process expressions

Table 2. Table 2: Structural operational semantics for node expressions

Table 3. Table 3: Structural operational semantics for network expressions

Equations

$$X({\mathtt{var}}_1,\dots ,{\mathtt{var}}_n)\stackrel{def}{=}P,\text{vspace}-2pt$$

$$P$$

$$\alpha$$

$$\begin{array}[]{@{\hspace{-2pt}}c|c|c@{}}{\tt rfr}&\textit{ch}\/&{\tt rfr}\star\textit{ch}\/\\ \cline{1-3}\cr*&\underline{\smash{\texttt{conflict}}}&\underline{\smash{\texttt{conflict}}}\\ &\underline{\smash{\texttt{idle}}}&\underline{\smash{\texttt{idle}}}\\ &{\text{$m$}}{:}{\text{$1$}}&{\text{$m$}}{:}{\text{$1$}}\\ {\text{$m$}}{:}{\text{$c$}}&{\text{$m$}}{:}{\text{$c{+}1$}}&{\text{$m$}}{:}{\text{$c{+}1$}}\\ \textsl{rfr}&{\text{$m$}}{:}{\text{$c{+}1$}}&\underline{\smash{\texttt{conflict}}}\\ &&\hfill\mbox{ if~{}}\textsl{rfr}\neq{\text{$m$}}{:}{\text{$c$}}\!\!\!\!\\ \end{array}$$

$$(\mathcal{R}_{1}\uplus\mathcal{R}_{2})(id):=\left\{\begin{array}[]{l@{\quad}l}\underline{\smash{\texttt{conflict}}}&\mbox{if $id\in\texttt{dom}(\mathcal{R}_{1})\cap\texttt{dom}(\mathcal{R}_{2})$}\\ \mathcal{R}_{1}(id)&\mbox{if $id\in\texttt{dom}(\mathcal{R}_{1})-\texttt{dom}(\mathcal{R}_{2})$}\\ \mathcal{R}_{2}(id)&\mbox{if $id\in\texttt{dom}(\mathcal{R}_{2})-\texttt{dom}(\mathcal{R}_{1})$}\ .\end{array}\right.$$

$$(a,b)\in \{(\text{traffic}(\text{T1},\text{R1}),\text{traffic}(\text{T2},\text{R2}))\mid {\mathcal{R}}_1,{\mathcal{R}}_2,{\mathcal{T}}_1,{\mathcal{T}}_2\in \mathtt{ID}\rightharpoonup \mathtt{CHUNK}\}$$

$$\begin{array}[]{@{}r@{~\hspace{-.5pt}}c@{~\hspace{-.5pt}}l@{\quad}r}\displaystyle\xi,\bigoplus_{{\tt i}=0}^{n}\ P\,\mathrel{\mathrel{\hbox{$\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\tau$\hskip 2.5pt}\hfil}}$}}}\ \mathcal{U}_{i=0}^{\xi(\textit{n}\/)}~{}\xi{\mbox{\scriptsize$\left[\begin{array}[]{@{}l@{}}{\tt i}:=i\end{array}\right]$ }},P\end{array}$$

$${\bf G}\big{(}\textit{id}\/\mathop{:}\textbf{newpkt}({\text{$d$}},{\text{$\textit{dest}\/$}})\Rightarrow{\bf F}(\textit{dest}\/\mathop{:}\textbf{deliver}(\textit{d}\/))\big{)}$$

$$\begin{array}[]{c}{\bf G}\big{(}\textbf{cntd}(\textit{id}\/,\textit{dest}\/)\wedge\textit{id}\/\mathop{:}\textbf{newpkt}({\text{$d$}},{\text{$\textit{dest}\/$}})\Rightarrow\\ {\bf F}(\textit{dest}\/\mathop{:}\textbf{deliver}(\textit{d}\/)\vee\textbf{disconnect}(\textit{id}\/,\textit{dest}\/)\vee\textbf{disconnect}(\textit{dest}\/,\textit{id}\/))\big{)}\end{array}$$

$$\phi^{\it post}=\{\begin{array}[]{@{}l@{}}\textit{dest}\/\mathop{:}\textbf{deliver}(\textit{d}\/),\textbf{disconnect}(*,*),\textbf{connect}(*,*),\textbf{newpkt}({\text{$*$}},{\text{$*$}})\end{array}\}.$$

Full text

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 [19, 17] 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 Section 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 Section 3. In Section 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 Section 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 (Section 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.111As it is the nonprobabilistic fragment of a forthcoming algebra we do not name it. 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) [12, 13, 2], 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 now 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 now 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 TIME, DATA, MSG, CHUNK, ${\tt ID}$ and $\pow{({\tt ID})}$ 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 now of type TIME and ${\tt rfr}$ of type CHUNK. In addition, we assume a set of process names. Each process name $X$ comes with a defining equation

[TABLE]

in which $n\in\mathop{\rm I\mkern-2.5muN}\nolimits$, ${\tt var}_{i}$ are variables and $P$ is a sequential process expression defined by the grammar below. It may contain the variables ${\tt var}_{i}$ as well as $X$. However, all occurrences of data variables in $P$ have to be bound.222An occurrence of a data variable in $P$ is bound if it is one of the variables ${\tt var}_{i}$, one of the two special variables ${\tt now}$ or ${\tt rfr}$, a variable var occurring in a subexpression $\textbf{[\![}{\tt var}\mathop{:=}\textsl{exp}\textbf{]\!]}Q$, an occurrence in a subexpression $\mbox{{[}}\varphi\mbox{{]}}Q$ of a variable occurring free in $\varphi$, or a variable data or dest occurring in a subexpression $\textbf{newpkt}({\tt data},{\tt dest}).Q$. Here $Q$ is an arbitrary sequential process expression. 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:

[TABLE]

Here $X$ is a process name, $\textsl{exp}_{i}$ a data expression of the same type as ${\tt var}_{i}$, $\varphi$ a data formula, ${\tt var}\mathop{:=}\textsl{exp}$ an assignment of a data expression exp to a variable var of the same type, ms a data expression of type MSG, and data, dest data variables of types DATA, ID respectively.

Given a valuation of the data variables by concrete data values, the sequential process $\mbox{{[}}\varphi\mbox{{]}}P$ 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 $\textbf{[\![}{\tt var}\mathop{:=}\textsl{exp}\textbf{]\!]}P$ acts as $P$, but under an updated valuation of the data variable var. 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 $\textbf{transmit}(\textsl{ms})$ transmits (the data value bound to the expression) ms to all other network nodes within transmission range. The action $\textbf{newpkt}({\tt data},{\tt dest})$ models the injection by the network layer of a data packet ${\tt data}$ to be transmitted to a destination ${\tt dest}$. Technically, ${\tt data}$ and ${\tt dest}$ are variables that will be bound to the obtained values upon receipt of a newpkt. Data is delivered to the network layer by deliver$({\tt data})$. 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 $\xi({\tt var})$ to variables var 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 var, and agrees with $\xi$ on all other variables, by $\xi[{\tt var}:=v]$. The valuation $\xi_{|S}$ agrees with $\xi$ on all variables ${\tt var}\in S$ and is undefined otherwise. Moreover we

use $\xi[{\tt var}\mbox{{\,+\!+}}]$ as an abbreviation for $\xi[{\tt var}:=\xi({\tt var})\mathop{+}1]$, 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 ${\tt dur}\mathop{:}{\tt MSG}\rightarrow{\tt TIME}_{>0}$ 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 {\tt CHUNK}:=\{{\text{m}}{:}{\text{c}}\mid m\in{\tt MSG},1\leq c\leq{{\tt dur}(m)}\}\cup\{\underline{\smash{\texttt{conflict}}},\underline{\smash{\texttt{idle}}}\}. The chunk {\text{m}}{:}{\text{c}} indicates the $c$ th fragment of a message $m$. Data conflicts—junk transmitted via the medium—is modelled by the special chunk $\underline{\smash{\texttt{conflict}}}$, and the absence of an incoming chunk is modelled by $\underline{\smash{\texttt{idle}}}$.

Our process algebra maintains a variable ${\tt rfr}$ of type ${\tt CHUNK}$, storing the fragment of the current message received so far.

As a value of this variable, {\text{m}}{:}{\text{c}} indicates that the first $c$ chunks of message $m$ have been received in order; $\underline{\smash{\texttt{conflict}}}$ indicates that the last incoming chunk was not the expected (next) part of a message in progress, and $\underline{\smash{\texttt{idle}}}$ 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 ${\tt rfr}$ evolves upon receiving a new chunk ch.

Specifications may refer to the data type ${\tt CHUNK}$ only through the Boolean functions new—having a single argument msg of type ${\tt MSG}$—and idle, defined by $\mbox{\sc new}(\textit{msg}\/):=({\tt rfr}=(\textit{msg}\/:{{\tt dur}(\textit{msg}\/)})$ and $\mbox{\sc idle}:=({\tt rfr}=\underline{\smash{\texttt{idle}}})$. A guard $[\mbox{\sc new}(\textit{msg}\/)]$ evaluates to true iff a new message msg has just been received; $[\mbox{\sc idle}]$ 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 Act of actions consists of \textbf{transmit}({\text{{\text{$m$}}}}{:}{\text{{\text{$c$}}}},{\text{\textit{ch}/}}), $\textbf{wait}(\textit{ch}\/)$, $\textbf{newpkt}(\textit{d}\/,\textit{dest}\/)$, $\textbf{deliver}(\textit{d}\/)$, and internal actions $\tau\!$, for each choice of $m\mathop{\in}{\tt MSG}$, $c\mathop{\in}\{1,\dots,{{\tt dur}(m)}\}$, $\textit{ch}\/\in{\tt CHUNK}$, $\textit{d}\/\mathop{\in}{\tt DATA}$ and $\textit{dest}\/\mathop{\in}{\tt ID}$, where the first two actions are time consuming. On every time-consuming action, each process receives a chunk ch and updates the variable ${\tt rfr}$ accordingly; moreover, the variable ${\tt now}$ is incremented on all process expressions in a (complete) network synchronously.

Besides the special variables ${\tt now}$ and ${\tt rfr}$, the formal semantics employs an internal variable ${\tt cntr}\mathop{\in}\mathop{\rm I\mkern-2.5muN}\nolimits$ that enumerates the chunks of split messages and is used to identify which chunk needs to be sent next. The variables now, rfr and cntr 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 ${\tt RO}=\{{\tt now},{\tt rfr},{\tt cntr}\}$.

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

[FIGURE:]

The first two rules describe the sending of a message ms. Remember that ${{\tt dur}(\textsl{ms})}$ calculates the time needed to send ms. The counter ${\tt cntr}$ keeps track of the time passed already. The action \textbf{transmit}({\text{{\text{$m$}}}}{:}{\text{{\text{$c$}}}},{\text{\textit{ch}/}}) occurs when the node transmits the fragment {\text{m}}{:}{\text{c}}; simultaneously, it receives the fragment ch.333Normally, a node is in its own transmission range. In that case the received chunk ch will be either the chunk {\text{m}}{:}{\text{c}} it is transmitting itself, or conflict in case some other node within transmission range is transmitting as well. The counter cntr is [math] before a message is sent, and is incremented before the transmission of each chunk. So, each chunk sent has the form {\text{\xi(\textsl{ms})}}{:}{\text{\xi({\tt cntr}){+}1}}. To ease readability we abbreviate ${\xi({\tt cntr}){+}1}$ by c+. In case the (already incremented) counter c+ is strictly smaller than the number of chunks needed to send $\xi(\textsl{ms})$, another transmit-action is needed (Rule 1); if the last fragment has been sent ($\texttt{c+}={{\tt dur}(\xi(\textsl{ms}))}$) the process can continue to act as $P$ (Rule 2).

The actions \textbf{newpkt}({\text{d}},{\text{\textit{dest}/}}) and $\textbf{deliver}(\textit{d}\/)$ are instantaneous and model the submission of data $d$ from the network layer, destined for dest, and the delivery of data $d$ to the network layer, respectively. The process \textbf{newpkt}({\text{d}},{\text{\textit{dest}/}}).P 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 var is updated.

In Rules 7 and 8, which define recursion, $\xi_{|{\tt RO}}[{\tt var}_{i}:=\xi(\textsl{exp}_{i})]_{i=1}^{n}$ is the valuation that only assigns the values $\xi(\textsl{exp}_{i})$ to the variables ${\tt var}_{i}$, for $i=1,\ldots,n$, and maintains the values of the variables ${\tt now}$, ${\tt rfr}$ and ${\tt cntr}$. These rules state that a defined process $X$ has the same transitions as the body $p$ of its defining equation. In case of a wait-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 $\xi(\textsl{exp})$ where exp is a data expression. The application of the rule depends on $\xi(\textsl{exp})$ 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 $\xi(p)\mathord{\uparrow}$, if $P$ has the form $\textbf{transmit}(\textsl{ms}).P$, $\textbf{deliver}({\tt data}).P$, $\textbf{[\![}{\tt var}:=\textsl{exp}\textbf{]\!]}P\,$ or $\,X(\textsl{exp}_{1},\ldots,\textsl{exp}_{n})$ with either $\xi(\textsl{ms})$ or $\xi({\tt data})$ or $\xi(\textsl{exp})$ or some $\xi(\textsl{exp}_{i})$ 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 \xi,P\mathrel{\mathrel{\hbox{\mathop{\hbox to30.27782pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\textbf{wait}(\textit{ch}\/)$\hskip 2.5pt}}}}}\zeta,P^{\prime} and \xi,Q\mathrel{\mathrel{\hbox{\mathop{\hbox to30.27782pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\textbf{wait}(\textit{ch}\/)$\hskip 2.5pt}}}}}\zeta^{\prime},Q^{\prime} then $P=P^{\prime}$, $Q=Q^{\prime}$ and $\zeta=\zeta^{\prime}$.

The first rule of (12), describing the semantics of guards $\mbox{{[}}\varphi\mbox{{]}}$, is taken from AWN. Here $\xi\stackrel{{\scriptstyle\varphi}}{{\rightarrow}}\zeta$ 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 \xi\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\varphi\;$\hskip 2.5pt}\hfil}}}}} 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 $\textbf{wait}(\textit{ch}\/)$.

2.2 A Language for Node Expressions

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

$\textit{id}\/\!:\!(\xi,P)\!:\!R\ .$

Here $\textit{id}\/\in{\tt ID}$ is the address of the node, $P$ is a sequential process expression with a valuation $\xi$, and $R\in\pow({\tt ID})$ is the range of the node, defined as the set of nodes within transmission range of id. 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 \textbf{traffic}({\text{\mathcal{T}}},{\text{\mathcal{R}}}), $\textit{id}\/\mathop{:}\textbf{deliver}(\textit{d}\/)$, \textit{id}\/\mathop{:}\textbf{newpkt}({\text{d}},{\text{\textit{id/}/^{\prime}}}), $\textbf{connect}({\textit{id}\/},{\textit{id\/}\/^{\prime}})$, $\textbf{disconnect}({\textit{id}\/},{\textit{id\/}\/^{\prime}})$ and $\tau$, with partial functions $\mathcal{T},\mathcal{R}\mathop{:}{\tt ID}\rightharpoonup{\tt CHUNK}$, $\textit{id}\/,\textit{id\/}\/^{\prime}\in{\tt ID}$, and $d\in{\tt DATA}$.

All time-consuming actions on process level (\textbf{transmit}({\text{{\text{$m$}}}}{:}{\text{{\text{$c$}}}},{\text{!\textit{ch}/}}) and $\textbf{wait}(\textit{\!ch}\/)$) are transformed into an action \textbf{traffic}({\text{\mathcal{T}}},{\text{\mathcal{R}}}) on node level: the first argument $\mathcal{T}$ maps dest to {\text{m}}{:}{\text{c}} if and only if the chunk {\text{m}}{:}{\text{c}} is transmitted to dest. The second argument $\mathcal{R}$ maps id to {\text{m}}{:}{\text{c}} if and only if the chunk {\text{m}}{:}{\text{c}} is received on process level at node id. For the sos-rules of Table 2 we use the set-theoretic presentation of partial functions. The two rules for wait set $\mathcal{T}:=\emptyset$, as no chunks are transmitted; the rules for transmit allow a transmitted chunk $m$:$c$ to travel to all nodes within transmission range: \mathcal{T}:=\{(r,{\text{m}}{:}{\text{c}})\!\mid\!r\in R\}. In case that during the transmission or waiting no chunk is received ($\textit{ch}\/=\underline{\smash{\texttt{idle}}}$) we set $\mathcal{R}=\emptyset$; otherwise $\mathcal{R}=\{(\textit{id}\/,\textit{ch}\/)\}$, indicating that chunk ch is received by node id.

The actions \textit{id}\/\mathop{:}\textbf{newpkt}({\text{d}},{\text{\textit{dest}/}}) and $\textit{id}\/\mathop{:}\textbf{deliver}(\textit{d}\/)$ 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 $\textbf{connect}(\textit{id}\/,\textit{id\/}\/^{\prime})$ and $\textbf{disconnect}(\textit{id}\/,\textit{id\/}\/^{\prime})$ for $\textit{id}\/,\textit{id\/}\/^{\prime}\mathop{\in}{\tt ID}$ 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 $\textit{id\/}\/^{\prime}$ is in the range of node id, meaning that $\textit{id\/}\/^{\prime}$ can receive messages sent by id, if and only if id is in the range of $\textit{id\/}\/^{\prime}$. 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 $\textit{id}\/\!:\!P\!:\!R$ receives its own transmissions depends on whether $\textit{id}\/\in R$. Only if $\textit{id}\/\in R$ our process algebra will disallow the transmission from and to a single node id at the same time, yielding a conflict.

2.3 A Language for Networks

A partial network is modelled by a parallel composition $\|$ 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.

The syntax of networks is described by the following grammar:

N::=[M_{T}^{T}]\qquad M_{S_{1}\mathbin{\mathchoice{\leavevmode\vtop{\halign{\hfil\m@th\displaystyle#\hfil\cr\cup\cr\mbox{\Large\cdot}\crcr}}}{\leavevmode\vtop{\halign{\hfil\m@th\textstyle#\hfil\cr\cup\cr\mbox{\Large\cdot}\crcr}}}{\leavevmode\vtop{\halign{\hfil\m@th\scriptstyle#\hfil\cr\cup\cr\mbox{\Large\cdot}\crcr}}}{\leavevmode\vtop{\halign{\hfil\m@th\scriptscriptstyle#\hfil\cr\cup\cr\mbox{\Large\cdot}\crcr}}}}S_{2}}^{T}::=M_{S_{1}}^{T}\|M_{S_{2}}^{T}\qquad M_{\{\textit{id}\/\}}^{T}::=\textit{id}\/\!:\!(\xi,P)\!:\!R\ ,

with $\{\textit{id}\/\}\cup R\subseteq T\subseteq{\tt ID}$. Here $M_{S}^{T}$ models a partial network describing the behaviour of all nodes $\textit{id}\/\in S$. 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 $\textit{id}\/\!:\!P\!:\!R$—are unique.

The operational semantics of network expressions is given in Table 3. Internal actions $\tau$ as well as the actions $\textit{id}\/\mathop{:}\textbf{deliver}(\textit{d}\/)$ and \textit{id}\/\mathop{:}\textbf{newpkt}({\text{d}},{\text{!\textit{id}/}}) 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 traffic (Line 3), the only action that consumes time on the network layer, uses the union $\uplus$ of partial functions. It is formally defined as

[TABLE]

The synchronisation of the sets $\mathcal{R}_{i}$ and $\mathcal{T}_{i}$ has the following intuition: if a node identifier $\textit{id}\/\in{\tt ID}$ is in both $\texttt{dom}(\mathcal{T}_{1})$ and dom($\mathcal{T}_{2}$) then there exist two nodes that transmit to node id at the same time, and therefore a frame collision occurs. In our algebra this is modelled by the special chunk $\underline{\smash{\texttt{conflict}}}$. The sos rules of Tables 2 and 3 guarantee that there cannot be collisions within the set of received chunks $\mathcal{R}$. The reason is that each node merely contributes to $\mathcal{R}$ a chunk for itself; it can be the chunk $\underline{\smash{\texttt{conflict}}}$ though. Therefore we could have written $\mathcal{R}_{1}\cup\mathcal{R}_{2}$ instead of $\mathcal{R}_{1}\uplus\mathcal{R}_{2}$ in the sixth rule of Table 3.

The last rule propagates a \textbf{traffic}({\text{\mathcal{T}}},{\text{\mathcal{R}}})-action of a partial network $M$ to a complete network $[M]$. By then $\mathcal{T}$ consists of all chunks (after collision detection) that are being transmitted by any member in the network, and $\mathcal{R}$ consists of all chunks that are received. The condition $\mathcal{R}=\mathcal{T}$ determines the content of the messages in $\mathcal{R}$. The \textbf{traffic}({\text{\mathcal{T}}},{\text{\mathcal{R}}})-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 N\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle a$\hskip 2.5pt}\hfil}}}}} and a\not\in\{\textbf{connect}(\textit{id}\/,\textit{id\/}\/^{\prime}),\textbf{disconnect}(\textit{id}\/,\textit{id\/}\/^{\prime}),\textit{id}\/\!:\!{\tt newpkt}({\text{\textit{d}/}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{\textit{dest}/}})\}.

More precisely, either N\mathrel{\mathrel{\hbox{\mathop{\hbox to16.47224pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\bf tick$\hskip 2.5pt}}}}}, or N\mathrel{\mathrel{\hbox{\mathop{\hbox to42.35284pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\textit{id}\/\mathop{:}\textbf{deliver}(\textit{d}\/)$\hskip 2.5pt}}}}} or N\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\tau$\hskip 2.5pt}\hfil}}}}}.*

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

$\T_{\xi}(\textbf{deliver}(\textsl{data}).P)=\textbf{deliver}(\xi(\textsl{data})).\T_{\xi}(P)$ and

\T_{\xi}(\textbf{[\![}{\tt var}:=\textsl{exp}\textbf{]\!]}P)=\tau.\T_{\xi{\mbox{\scriptsize\left[\begin{array}[]{@{}l@{}}{\tt var}:=\xi(\textsl{exp})\end{array}\right] }}}(P).

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, \mathop{\,\raisebox{1.29167pt}{\underline{\makebox[6.99997pt]{$\leftrightarrow$}}}} —as the original. It follows that \mathop{\,\raisebox{1.29167pt}{\underline{\makebox[6.99997pt]{$\leftrightarrow$}}}}\,, 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]. ∎

Theorem 2.3

The operator $\|$ is associative and commutative, up to \mathop{\,\raisebox{1.29167pt}{\underline{\makebox[6.99997pt]{$\leftrightarrow$}}}} .

Proof

The operational rules for this operator fits a format presented in [6], guaranteeing associativity up to \mathop{\,\raisebox{1.29167pt}{\underline{\makebox[6.99997pt]{$\leftrightarrow$}}}}. 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 $\|$ of Table 3 are of types $1$, $2$ and $7$, respectively. To be precise, it has rules $1_{a}$ and $2_{a}$ for $a\in\{\tau$, $\textit{id}\/\mathop{:}\textbf{deliver}(\textit{d}\/)$, \textit{id}\/\mathop{:}\textbf{newpkt}({\text{d}},{\text{\textit{dest}/}})\}, rules $7_{(a,b)}$ for

[TABLE]

and rules $7_{(c,c)}$ for $c\in\{\textbf{connect}({\textit{id}\/},{\textit{id\/}\/^{\prime}}),\textbf{disconnect}({\textit{id}\/},{\textit{id\/}\/^{\prime}})\mid\textit{id}\/,\textit{id\/}\/^{\prime}\in{\tt ID}\}$. Moreover, the partial communication function $\gamma:\textrm{Act}\times\textrm{Act}\rightharpoonup\textrm{Act}$ is given by \gamma(\textbf{traffic}({\text{\mathcal{T}{1}}},{\text{\mathcal{R}{1}}}),\textbf{traffic}({\text{\mathcal{T}{2}}},{\text{\mathcal{R}{2}}}))=\textbf{traffic}({\text{\mathcal{T}{1}\uplus\mathcal{T}{2}}},{\text{\mathcal{R}{1}\uplus\mathcal{R}{2}}}) 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

$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)})\ .$

Here $1_{a}$ says that rule $1_{a}$ is present, etc. This condition is trivially met for $\|$ as there neither exists a rule of the form 1_{\textbf{traffic}({\text{\mathcal{T}!}},{\text{\mathcal{R}}})} nor of the form 2_{\textbf{traffic}({\text{\mathcal{T}!}},{\text{\mathcal{R}}})}, 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 $\underline{\smash{\texttt{conflict}}}$, it is straightforward to prove associativity of $\gamma$.

Commutativity of $\|$ follows by symmetry of the sos rules. ∎

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 $(S,\textrm{Act},\rightarrow)$, where

1. (i)

$S$ is a set of states 2. (ii)

Act is a set of actions 3. (iii)

${\rightarrow}\subseteq S\times\textrm{Act}\times\mathcal{D}(S)$, where $\mathcal{D}(S)$ is the set of all (discrete) probability distributions over $S$: functions $\Delta:S\rightarrow[0,1]$ with $\sum_{s\in S}\Delta(s)=1$.

As with LTSs, we usually write s\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}\Delta instead of $(s,\alpha,\Delta)\in{\rightarrow}$. The point distribution $\delta_{s}$, for $s\in S$, is the distribution with $\delta_{s}(s)=1$. We simply write s\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}t for s\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}\delta_{t}. 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 $\mathcal{U}_{i=0}^{n}s_{i}$. 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. Act 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^{\prime}$ (or $\zeta,Q^{\prime}$) is replaced by an arbitrary distribution $\Delta$. Add to those the following rule for the probabilistic choice operator:

[TABLE]

Here the data variable $i$ may occur in $P$. The rules of Tables 2 and 3 are adapted to ALL unchanged, except that $P^{\prime}$, $M^{\prime}$ and $N^{\prime}$ 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 $\Delta$ is a distribution over sequential processes, $\textit{id}\/\in{\tt ID}$ and $R\subseteq{\tt ID}$, then $\textit{id}\/\!:\!\Delta\!:\!R$ describes the distribution over node expressions that only has probability mass on nodes with address id and range $R$, and for which the probability of $\textit{id}\/\!:\!P\!:\!R$ is $\Delta(P)$. Likewise, if $\Delta$ and $\Theta$ are distributions over network expressions, then $\Delta\|\Theta$ is the distribution over network expressions of the form $M\|N$, where $(\Delta\|\Theta)(M\|N)=\Delta(M)\cdot\Theta(N)$.

4 Formalising Liveness Properties of Link Layer Protocols

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

[TABLE]

for any $\textit{id}\/,\textit{dest}\/\mathbin{\in}{\tt ID}$ and $d\mathbin{\in}{\tt DATA}$. This formula has the shape \mathbf{G}\big{(}\phi^{\it pre}\Rightarrow\mathbf{F}\phi^{\it post}\big{)}, and is called an eventuality property in [22]. It says that whenever we reach a state in which the precondition $\phi^{\it pre}$ is satisfied, this state will surely be followed by a state were the postcondition $\phi^{\it 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^{\it pre}$ and $\phi^{\it post}$.

Formula (1) is too strong and does not hold in general: in case the nodes id and dest are not within transmission range of each other, the delivery of messages from id to dest 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, id needs to be connected to dest. We introduce the predicate $\textbf{cntd}(\textit{id}\/,\textit{dest}\/)$ to express this, and hence take $\phi^{\it pre}$ to be \textbf{cntd}(\textit{id}\/,\textit{dest}\/)\wedge\textit{id}\/\mathop{:}\textbf{newpkt}({\text{d}},{\text{\textit{dest}/}}). Secondly, we assume that the link between id and dest does not break until the message is delivered. As remarked in [13], such a side condition can be formalised by taking $\phi^{\it post}$ to be $\textit{dest}\/\mathop{:}\textbf{deliver}(\textit{d}\/)\vee\textbf{disconnect}(\textit{id}\/,\textit{dest}\/)$. Thus the liveness property we are after is

[TABLE]

We now define the validity of eventuality properties \mathbf{G}\big{(}\phi^{\it pre}\Rightarrow\mathbf{F}\phi^{\it post}\big{)}. Here $\phi^{\it pre}$ and $\phi^{\it post}$ denote sets of transitions and actions, respectively, and hold if one of the transitions or actions in the set occurs. In (2), $\phi^{\it pre}$ denotes the transitions with label \textit{id}\/\mathop{:}\textbf{newpkt}({\text{d}},{\text{\textit{dest}/}}) that occur when the side condition $\textbf{cntd}(\textit{id}\/,\textit{dest}\/)$ is met, whereas $\phi^{\it post}=\{\textit{dest}\/\mathop{:}\textbf{deliver}(\textit{d}\/),\textbf{disconnect}(\textit{id}\/,\textit{dest}\/),\linebreak[2]\textbf{disconnect}(\textit{dest}\/,\textit{id}\/)\}$ is a set of actions.

A path in a pLTS $(S,\textrm{Act},\rightarrow)$ 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 s_{i}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.96707pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.87495pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha_{i+1}$\hskip 2.5pt}}}}}\Delta_{i+1} with $\Delta_{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 \mathbf{G}\big{(}\phi^{\it pre}\Rightarrow\mathbf{F}\phi^{\it post}\big{)}, with $\phi^{\it pre}$ and $\phi^{\it post}$ denoting sets of transitions and actions, holds outright if all complete paths starting with a reachable transition from $\phi^{\it pre}$ contain a transition with a label from $\phi^{\it 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^{\it 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 $\mathit{Prob}(t,\phi^{\it 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^{\it post}$. Now in a pLTS with an initial state, an eventually formula \mathbf{G}\big{(}\phi^{\it pre}\Rightarrow\mathbf{F}\phi^{\it post}\big{)} holds with probability at least $p$ if for all reachable transitions $t$ in $\phi^{\it pre}$ we have $\mathit{Prob}(t,\phi^{\it post})\geq 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

[TABLE]

We will refer to this version of (2) as the weak packet delivery property. Packet delivery is the strengthening without $\textbf{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) [19, 17]444The primary medium access control (MAC) technique of IEEE 802.11 [19] is called distributed coordination function (DCF), which is a CSMA/CA protocol. 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 Section 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 CSMA, depicted in Process 1, is the protocol’s entry point.

This process maintains a single data variable id in which it stores its own identity. It waits until either it receives a request from the network layer to transmit a packet ${\tt data}$ to destination ${\tt dest}$, 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 ${\tt INIT}$ is called; this process (described below) initiates the sending of the message via the medium. When passing the message on to ${\tt INIT}$ we use a function ${\tt dataframe}\mathop{:}{\tt DATA}\times{\tt ID}\times{\tt ID}\rightarrow{\tt MSG}$ that generates a message in a format used by the protocol: next to the header fields (from which we abstract) it contains the injected data as well as the designated receiver ${\tt dest}$ and the sender ${\tt id}$—the current node.

In case of an incoming ${\tt dataframe}$ destined for this node (the third argument carrying the destination is ${\tt id}$) (Line 2)—any other incoming message is ignored by this process—the data is handed over to the network layer ($\textbf{deliver}({\tt data})$) followed by the transmission of an acknowledgement back to the sender of the message (${\tt src}$). CSMA/CA requires a short period of idling medium before sending the acknowledgement: in [19] this interval is called short interframe space (sifs). 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 ${\tt src}$, e.g. due to data collision; therefore src could send the same message again (see Process 4) and id could deliver the same data to the network layer again.

The process ${\tt INIT}$ (Process 2) initiates the sending of a message via the medium. Next to the variable id, which is maintained by all processes, it maintains the variable ${\tt tries}$ and ${\tt dframe}$: ${\tt tries}$ stores the number of attempts already made to send message ${\tt dframe}$. When the process is called the first time for a message ${\tt dframe}$ (Line 1 of Process 1) the value of ${\tt tries}$ is [math].

The constant $\underline{\smash{\texttt{max\_retransmit}}}$ 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 ${\tt dframe}$ 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 ${\tt cw}$, a.k.a. backoff time. cw is calculated in Line 2; it increases exponentially.555A typical value for $\underline{\smash{\texttt{cwmin}}}$ is $16$; it must satisfy $\underline{\smash{\texttt{cwmin}}}>0$. After ${\tt cw}$ is determined, the process CCA 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 ${\tt dframe}$. 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 ($\underline{\smash{\texttt{difs}}}\in{\tt TIME}$), which is usually small,666Recommended values for the constant $\underline{\smash{\texttt{difs}}}$ are given in [19]. but larger than $\underline{\smash{\texttt{sifs}}}$, 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 ${\tt b}$ 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 ${\tt ACKRECV}$ that will await an acknowledgement from the recipient of ${\tt dframe}$ (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 ${\tt b}$—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 ${\tt dframe}$ 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 ${\tt tries}$ 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 $\underline{\smash{\texttt{max\_retransmit}}}{=}\infty$ 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, $\underline{\smash{\texttt{max\_retransmit}}}$ 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.

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 Figure 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 data (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 data. The reason is that a hidden node, which could interfere with the sending of data will receive the CTS message from the designated recipient of data  and the hidden node will remain silent until the data 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 ${\tt rts}$ and ${\tt cts}$ messages, respectively. The signature of both is ${\tt ID}\times{\tt ID}\times{\tt TIME}\to{\tt MSG}$. 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 {\tt rts}({\text{{\tt src}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt dest}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt d}}}) is transmitted, the time period d is calculated by

{{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\textbf{[\![}{\tt d}:=\underline{\smash{\texttt{sifs}}}\hskip 0.95pt{+}\hskip 0.95pt\underline{\smash{\texttt{dur\_cts}}}\hskip 0.95pt{+}\hskip 0.95pt\underline{\smash{\texttt{sifs}}}\hskip 0.95pt{+}\hskip 0.95pt{{\tt dur}({\tt dataframe}({\text{{\tt data}}}\mathop{\text{\hskip-0.90005pt,\hskip-0.90005pt}}{\text{{\tt id}}}\mathop{\text{\hskip-0.90005pt,\hskip-0.90005pt}}{\text{{\tt dest}}}))}\hskip 0.95pt{+}\hskip 0.95pt\underline{\smash{\texttt{sifs}}}\hskip 0.95pt{+}\hskip 0.95pt\underline{\smash{\texttt{dur\_ack}}}\textbf{]\!]}}} ​.

The calculation is straightforward as it follows the protocol logic and determines the amount of time needed until the acknowledgement would be

received (see Figure 2). After the ${\tt rts}$ message has been received the medium should be idle for the interframe space $\underline{\smash{\texttt{sifs}}}$; then a ${\tt cts}$ message is sent back, which takes time $\underline{\smash{\texttt{dur\_cts}}}$; then another interframe space is needed, followed by the actual transmission of the message—the sending will take {{\tt dur}({\tt dataframe}({\text{{\tt data}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt id}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt dest}}}))} time units; after the message is received (hopefully) another interframe space is required before the acknowledgement is sent back.

Process 2 remains essentially unchanged; it is merely equipped with the destination ${\tt dest}$ of the message that needs to be transmitted, and an additional timed variable ${\tt nav}\in{\tt TIME}$. These variables are not used in this process, but required later on. Variable ${\tt nav}$ holds the point in time until the process should not transmit any ${\tt rts}$ or ${\tt cts}$ message. This period of silence is necessary as the node figures out that until time ${\tt nav}$ another node will transmit message(s).777After a successful RTS/CTS exchange, communicating nodes proceed with transmitting the data and an acknowledgement regardless of the value of ${\tt nav}$.

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 ${\tt rts}$ message {\tt rts}({\text{{\tt src}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt dest}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt d}}}) is received that is intended for another recipient (${\tt dest}\neq{\tt id}$) the node concludes that another node wants to use the medium for the amount of ${\tt d}$ time units; the process updates the variable ${\tt nav}$ if needed, indicating the period the node should remain silent, by taking the maximum of the current value of ${\tt nav}$, and ${\tt now}{+}{\tt d}$, the point in time until the sender ${\tt src}$ of the ${\tt rts}$ message requires the medium. The same behaviour occurs if a ${\tt cts}$ message is received that is not intended for the node itself (Line 4). If the incoming message is an ${\tt rts}$ 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 ${\tt rts}$ has knowledge about other nodes requiring the medium (${\tt now}\leq{\tt nav}$), 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 (sifs) before sending the CTS (Line 6).

Line 8 handles the case where the medium becomes busy ($\neg\mbox{\sc idle}$) during this period; also here a clear-to-send cannot be granted, and the request is dropped.888The condition ${\tt now}>{\tt timeout}{-}\underline{\smash{\texttt{sifs}}}$ prevents the process from dropping the request in the very first time slice that CSMA is running. Here the medium counts as busy, but only because we have just received an ${\tt rts}$ message. Only when the medium stays idle during the entire interframe space the node ${\tt id}$ can inform the source of the ${\tt rts}$ message that the medium is clear to send; the ${\tt cts}$ 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 ${\tt nav}$ to remind itself not to issue any ${\tt rts}$ message until the present exchange has been completed.999A case \mbox{\sc new}({\tt cts}({\text{{\tt src}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt dest}}}\mathop{\text{\hskip-1.00006pt,\hskip-1.00006pt}}{\text{{\tt d}}}))\wedge{\tt dest}={\tt id} is not required as a ${\tt cts}$ message is only expected in case an ${\tt rts}$ was sent, and hence handled in process RTSREACT.

Process 6 is the modified version of Process 3. The goal of this process is to send an ${\tt rts}$ 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, ${\tt rts}$ or ${\tt cts}$ 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 ${\tt rts}$ message, and Line 23 passes control to the process CTSRECV, which awaits a ${\tt cts}$ response to the ${\tt rts}$ message transmitted in Line 22. The fourth argument of CTSRECV specifies the maximum time that process should wait for such a response; a good value for $\underline{\smash{\texttt{max\_cts\_wait}}}$ is $\underline{\smash{\texttt{sifs}}}+\underline{\smash{\texttt{dur\_cts}}}$.

Process CTSRECV listens for this time to a ${\tt cts}$ message with source ${\tt dest}$ and destination ${\tt id}$. In case the expected ${\tt cts}$ message arrives in time (Line 1), the node waits for a time $\underline{\smash{\texttt{sifs}}}$ (Line 2) and then transmits the data frame and proceeds to await an acknowledgement (Line 3). The fourth argument of ACKRECV specifies the maximum time the process should wait for such an acknowledgement; a good value for $\underline{\smash{\texttt{max\_ack\_wait}}}$ is $\underline{\smash{\texttt{sifs}}}+\underline{\smash{\texttt{dur\_ack}}}$. If the ${\tt cts}$ message does not arrive in time (Line 6), the process returns to INIT to send another ${\tt rts}$ message, while incrementing the counter ${\tt tries}$ (Line 7). While waiting for the ${\tt cts}$ message, any incoming ${\tt rts}$ or ${\tt cts}$ 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 ${\tt rts}$ messages to ${\tt id}$ 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 ${\tt id}$ has transmitted a data frame. In that case (Line 1), the network layer is informed that the sending of ${\tt dframe}$ 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 ${\tt tries}$ is incremented. Lines 3–4 describe the usual handling of incoming ${\tt rts}$ or ${\tt cts}$ 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 Section 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 cts sent by $B$ in response to an rts sent by $A$ will tell $C$ to keep silent for the required duration. In fact, we can show that in the above topology, if $\underline{\smash{\texttt{max\_retransmit}}}{=}\infty$ 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 cts, then packet delivery holds outright. So the only problem left is to achieve a successful RTS/CTS handshake. Since rts and cts messages are rather short, even by modest values of $\underline{\smash{\texttt{max\_retransmit}}}$ 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

B$$A$$C_{1}$$D_{1}$$C_{2}$$D_{2}$$C_{3}$$D_{3}

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\neq i$, coordination between the nodes is impossible. As a consequence, the medium at $A$ will always be busy, so that $A$ cannot send an rts message to $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, 26, 20, 21]. 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 uses 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.

Acknowledgement:

We thank Tran Ngoc Ma for her involvement in this project in a very early phase. We also like to thank the German Academic Exchange Service (DAAD) that funded an internship of the third author at Data61, CSIRO.