Advertisement

A Process Algebra for Link Layer Protocols

  • Rob van GlabbeekEmail author
  • Peter Höfner
  • Michael Markl
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11423)

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.1 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 Open image in new window 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 Open image in new window 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 Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window and Open image in new window 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 Open image in new window of type Open image in new window and Open image in new window of type Open image in new window . In addition, we assume a set of process names. Each process name X comes with a defining equationin which Open image in new window , Open image in new window are variables and \(P\) is a sequential process expression defined by the grammar below. It may contain the variables Open image in new window as well as X. However, all occurrences of data variables in \(P\) have to be bound.2 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, Open image in new window a data expression of the same type as Open image in new window , \(\varphi \) a data formula, Open image in new window an assignment of a data expression Open image in new window to a variable Open image in new window of the same type, Open image in new window a data expression of type Open image in new window , and Open image in new window , Open image in new window data variables of types Open image in new window , Open image in new window respectively.

Given a valuation of the data variables by concrete data values, the sequential process Open image in new window 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 Open image in new window acts as \(P\), but under an updated valuation of the data variable  Open image in new window . 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 Open image in new window transmits (the data value bound to the expression) Open image in new window to all other network nodes within transmission range. The action Open image in new window models the injection by the network layer of a data packet Open image in new window to be transmitted to a destination Open image in new window . Technically, Open image in new window and Open image in new window are variables that will be bound to the obtained values upon receipt of a \(\mathbf{newpkt}\). Data is delivered to the network layer by Open image in new window . 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 Open image in new window to variables Open image in new window 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 Open image in new window , and agrees with \(\xi \) on all other variables, by Open image in new window . The valuation \(\xi _{|S}\) agrees with \(\xi \) on all variables Open image in new window and is undefined otherwise. Moreover we use Open image in new window as an abbreviation for Open image in new window , 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 Open image in new window 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 Open image in new window . The chunk Open image in new window indicates the c th fragment of a message m. Data conflicts—junk transmitted via the medium—is modelled by the special chunk Open image in new window , and the absence of an incoming chunk is modelled by Open image in new window .

Our process algebra maintains a variable Open image in new window of type Open image in new window , storing the fragment of the current message received so far.As a value of this variable, Open image in new window indicates that the first c chunks of message m have been received in order; Open image in new window indicates that the last incoming chunk was not the expected (next) part of a message in progress, and Open image in new window 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 Open image in new window evolves upon receiving a new chunk  Open image in new window .

Specifications may refer to the data type Open image in new window only through the Boolean functions Open image in new window —having a single argument Open image in new window of type Open image in new window —and Open image in new window , defined by Open image in new window and Open image in new window . A guard Open image in new window evaluates to true iff a new message Open image in new window has just been received; Open image in new window 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 Open image in new window of actions consists of Open image in new window , Open image in new window , Open image in new window , Open image in new window , and internal actions \(\tau \!\), for each choice of Open image in new window , Open image in new window , Open image in new window , Open image in new window and Open image in new window , where the first two actions are time consuming. On every time-consuming action, each process receives a chunk Open image in new window and updates the variable Open image in new window accordingly; moreover, the variable Open image in new window is incremented on all process expressions in a (complete) network synchronously.
Table 1.

Structural operational semantics for sequential process expressions

Besides the special variables Open image in new window and Open image in new window , the formal semantics employs an internal variable Open image in new window that enumerates the chunks of split messages and is used to identify which chunk needs to be sent next. The variables Open image in new window , Open image in new window and Open image in new window 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 Open image in new window .

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

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

The actions Open image in new window and Open image in new window are instantaneous and model the submission of data d from the network layer, destined for Open image in new window , and the delivery of data d to the network layer, respectively. The process Open image in new window 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 Open image in new window is updated.

In Rules 7 and 8, which define recursion, Open image in new window is the valuation that only assigns the values Open image in new window to the variables Open image in new window , for \(i=1,\ldots ,n\), and maintains the values of the variables Open image in new window , Open image in new window and Open image in new window . These rules state that a defined process X has the same transitions as the body p of its defining equation. In case of a Open image in new window -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 Open image in new window where Open image in new window is a data expression. The application of the rule depends on Open image in new window 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 Open image in new window , if \(P\) has the form Open image in new window , Open image in new window , Open image in new window or Open image in new window with either Open image in new window or Open image in new window or Open image in new window or some Open image in new window 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 Open image in new window and Open image in new window then \(P=P'\), \(Q=Q'\) and \(\zeta =\zeta '\).

The first rule of (12), describing the semantics of guards Open image in new window , is taken from AWN. Here Open image in new window 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 Open image in new window 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 Open image in new window .

2.2 A Language for Node Expressions

We model network nodes in the context of a (wireless) network by node expressions of the formHere Open image in new window is the address of the node, Open image in new window is a sequential process expression with a valuation \(\xi \), and Open image in new window is the range of the node, defined as the set of nodes within transmission range of Open image in new window . 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 Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window and \(\tau \), with partial functions Open image in new window , Open image in new window , and Open image in new window .
Table 2.

Structural operational semantics for node expressions

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

The actions Open image in new window and Open image in new window 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 Open image in new window and Open image in new window for Open image in new window 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 Open image in new window is in the range of node Open image in new window , meaning that Open image in new window can receive messages sent by Open image in new window , if and only if Open image in new window is in the range of Open image in new window . 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 Open image in new window receives its own transmissions depends on whether Open image in new window . Only if Open image in new window our process algebra will disallow the transmission from and to a single node Open image in new window at the same time, yielding a Open image in new window .

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 Open image in new window . Here \(M_S^T\) models a partial network describing the behaviour of all nodes Open image in new window . 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 Open image in new window —are unique.

The operational semantics of network expressions is given in Table 3. Internal actions \(\tau \) as well as the actions Open image in new window and Open image in new window 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 Open image in new window (Line 3), the only action that consumes time on the network layer, uses the union \(\uplus \) of partial functions. It is formally defined asThe synchronisation of the sets Open image in new window and Open image in new window has the following intuition: if a node identifier Open image in new window is in both Open image in new window and Open image in new window then there exist two nodes that transmit to node Open image in new window at the same time, and therefore a frame collision occurs. In our algebra this is modelled by the special chunk Open image in new window . The sos rules of Tables 2 and 3 guarantee that there cannot be collisions within the set of received chunks Open image in new window . The reason is that each node merely contributes to Open image in new window a chunk for itself; it can be the chunk Open image in new window though. Therefore we could have written Open image in new window instead of Open image in new window in the sixth rule of Table 3.

The last rule propagates a Open image in new window -action of a partial network M to a complete network [M]. By then Open image in new window consists of all chunks (after collision detection) that are being transmitted by any member in the network, and Open image in new window consists of all chunks that are received. The condition Open image in new window determines the content of the messages in Open image in new window . The Open image in new window -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 Open image in new window and Open image in new window .

More precisely, either Open image in new window , or Open image in new window or Open image in new window .

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

Open image in new window and

Open image in new window .

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, Open image in new window —as the original. It follows that Open image in new window , 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 Open image in new window  .

Proof

The operational rules for this operator fits a format presented in [6], guaranteeing associativity up to  Open image in new window . 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 Open image in new window , rules \(7_{(a,b)}\) forand rules \(7_{(c,c)}\) for Open image in new window . Moreover, the partial communication function Open image in new window is given by Open image in new window 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 Open image in new window nor of the form Open image in new window , 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 Open image in new window , 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 Open image in new window , where
  1. (i)

    S is a set of states

     
  2. (ii)

    Open image in new window is a set of actions

     
  3. (iii)

    Open image in new window , where Open image in new window 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 Open image in new window 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 Open image in new window for Open image in new window . 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 Open image in new window . 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. Open image in new window 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, Open image in new window and Open image in new window , then Open image in new window describes the distribution over node expressions that only has probability mass on nodes with address Open image in new window and range R, and for which the probability of Open image in new window 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 Open image in new window and Open image in new window . The typical liveness property expected of a link layer protocol is that if the network layer at node Open image in new window injects a data packet d for delivery at destination Open image in new window then this packet is delivered eventually. In terms of our process algebra, this says that every execution of the action Open image in new window ought to be followed by the action Open image in new window . This property can be formalised in Linear-time Temporal Logic [22] asfor any Open image in new window and Open image in new window . This formula has the shape Open image in new window , 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 Open image in new window and Open image in new window are not within transmission range of each other, the delivery of messages from Open image in new window to Open image in new window 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, Open image in new window needs to be connected to Open image in new window . We introduce the predicate Open image in new window to express this, and hence take \(\phi ^{ pre}\) to be Open image in new window . Secondly, we assume that the link between Open image in new window and Open image in new window 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 Open image in new window . Thus the liveness property we are after isWe now define the validity of eventuality properties Open image in new window . 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 Open image in new window that occur when the side condition Open image in new window is met, whereas Open image in new window is a set of actions.

A path in a pLTS Open image in new window 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 Open image in new window 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 Open image in new window , 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 Open image in new window 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 takingWe 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]4 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 Open image in new window , depicted in Process 1, is the protocol’s entry point.

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

In case of an incoming Open image in new window destined for this node (the third argument carrying the destination is Open image in new window ) (Line 2)—any other incoming message is ignored by this process—the Open image in new window is handed over to the network layer ( Open image in new window ) followed by the transmission of an acknowledgement back to the sender of the message ( Open image in new window ). CSMA/CA requires a short period of idling medium before sending the acknowledgement: in [19] this interval is called short interframe space ( Open image in new window ). 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 Open image in new window , e.g. due to data collision; therefore Open image in new window could send the same message again (see Process 4) and Open image in new window could deliver the same data to the network layer again.
The process Open image in new window (Process 2) initiates the sending of a message via the medium. Next to the variable Open image in new window , which is maintained by all processes, it maintains the variable Open image in new window and Open image in new window : Open image in new window stores the number of attempts already made to send message Open image in new window . When the process is called the first time for a message Open image in new window (Line 1 of Process 1) the value of Open image in new window is 0.

The constant Open image in new window 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 Open image in new window 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 Open image in new window , a.k.a. backoff time. Open image in new window is calculated in Line 2; it increases exponentially.5 After Open image in new window is determined, the process Open image in new window 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 Open image in new window . 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 ( Open image in new window ), which is usually small,6 but larger than Open image in new window , 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 Open image in new window 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 Open image in new window that will await an acknowledgement from the recipient of Open image in new window (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 Open image in new window —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 Open image in new window 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 Open image in new window 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 Open image in new window 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, Open image in new window 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 Open image in new window (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 Open image in new window . The reason is that a hidden node, which could interfere with the sending of Open image in new window will receive the CTS message from the designated recipient of Open image in new window , and the hidden node will remain silent until the Open image in new window 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 Open image in new window and Open image in new window messages, respectively. The signature of both is Open image in new window . 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 Open image in new window is transmitted, the time period Open image in new window 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 Open image in new window message has been received the medium should be idle for the interframe space Open image in new window ; then a Open image in new window message is sent back, which takes time Open image in new window ; then another interframe space is needed, followed by the actual transmission of the message—the sending will take Open image in new window 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 Open image in new window of the message that needs to be transmitted, and an additional timed variable Open image in new window . These variables are not used in this process, but required later on. Variable Open image in new window holds the point in time until the process should not transmit any Open image in new window or Open image in new window message. This period of silence is necessary as the node figures out that until time Open image in new window another node will transmit message(s).7

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 Open image in new window message Open image in new window is received that is intended for another recipient ( Open image in new window ) the node concludes that another node wants to use the medium for the amount of Open image in new window time units; the process updates the variable Open image in new window if needed, indicating the period the node should remain silent, by taking the maximum of the current value of Open image in new window , and Open image in new window , the point in time until the sender Open image in new window of the Open image in new window message requires the medium. The same behaviour occurs if a Open image in new window message is received that is not intended for the node itself (Line 4). If the incoming message is an Open image in new window 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 Open image in new window has knowledge about other nodes requiring the medium ( Open image in new window ), 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 ( Open image in new window ) before sending the CTS (Line 6). Line 8 handles the case where the medium becomes busy ( Open image in new window ) during this period; also here a clear-to-send cannot be granted, and the request is dropped.8 Only when the medium stays idle during the entire interframe space the node Open image in new window can inform the source of the Open image in new window message that the medium is clear to send; the Open image in new window 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 Open image in new window to remind itself not to issue any Open image in new window message until the present exchange has been completed.9

Process 6 is the modified version of Process 3. The goal of this process is to send an Open image in new window 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, Open image in new window or Open image in new window 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 Open image in new window message, and Line 23 passes control to the process Open image in new window , which awaits a Open image in new window response to the Open image in new window message transmitted in Line 22. The fourth argument of Open image in new window specifies the maximum time that process should wait for such a response; a good value for Open image in new window is Open image in new window .

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

Footnotes

  1. 1.

    As it is the nonprobabilistic fragment of a forthcoming algebra we do not name it.

  2. 2.

    An occurrence of a data variable in \(P\) is bound if it is one of the variables Open image in new window , one of the two special variables Open image in new window or Open image in new window , a variable Open image in new window occurring in a subexpression Open image in new window , an occurrence in a subexpression Open image in new window of a variable occurring free in \(\varphi \), or a variable Open image in new window or Open image in new window occurring in a subexpression Open image in new window . Here \(Q\) is an arbitrary sequential process expression.

  3. 3.

    Normally, a node is in its own transmission range. In that case the received chunk Open image in new window will be either the chunk Open image in new window it is transmitting itself, or Open image in new window in case some other node within transmission range is transmitting as well.

  4. 4.

    The primary medium access control (MAC) technique of IEEE 802.11 [19] is called distributed coordination function (DCF), which is a CSMA/CA protocol.

  5. 5.

    A typical value for Open image in new window is 16; it must satisfy Open image in new window .

  6. 6.

    Recommended values for the constant Open image in new window are given in [19].

  7. 7.

    After a successful RTS/CTS exchange, communicating nodes proceed with transmitting the data and an acknowledgement regardless of the value of Open image in new window .

  8. 8.

    The condition Open image in new window prevents the process from dropping the request in the very first time slice that Open image in new window is running. Here the medium counts as busy, but only because we have just received an Open image in new window message.

  9. 9.

    A case Open image in new window is not required as a Open image in new window message is only expected in case an Open image in new window was sent, and hence handled in process Open image in new window .

Notes

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.

References

  1. 1.
    Bianchi, G.: Performance analysis of the IEEE 802.11 distributed coordination function. IEEE J. Sel. Areas Commun. 18(3), 535–547 (2000).  https://doi.org/10.1109/49.840210CrossRefGoogle Scholar
  2. 2.
    Bres, E., van Glabbeek, R.J., Höfner, P.: A timed process algebra for wireless networks with an application in routing. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 95–122. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49498-1_5CrossRefGoogle Scholar
  3. 3.
    Calder, M., Sevegnani, M.: Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Aspects Comput. 26(3), 537–561 (2014).  https://doi.org/10.1007/s00165-012-0270-3MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Chhaya, H.S., Gupta, S.: Performance modeling of asynchronous data transfer methods of IEEE 802.11 MAC Protocol. Wirel. Netw. 3, 217–234 (1997).  https://doi.org/10.1023/A:1019109301754CrossRefGoogle Scholar
  5. 5.
    Comer, D.: Computer Networks and Internets. Pearson Education Inc., UpperSaddle River (2009)Google Scholar
  6. 6.
    Cranen, S., Mousavi, M.R., Reniers, M.A.: A rule format for associativity. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 447–461. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85361-9_35CrossRefGoogle Scholar
  7. 7.
    De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995).  https://doi.org/10.1145/201019.201032MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C., Zhang, C.: Remarks on testing probabilistic processes. In: Cardelli, L., Fiore, M., Winskel, G. (eds.) Computation, Meaning, and Logic: Articles Dedicated to Gordon Plotkin, Electronic Notes in Theoretical Computer Science, vol. 172, pp. 359–397. Elsevier (2007).  https://doi.org/10.1016/j.entcs.2007.02.013
  9. 9.
    Deng, Y., van Glabbeek, R.J., Morgan, C.C., Zhang, C.: Scalar outcomes suffice for finitary probabilistic testing. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 363–378. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71316-6_25CrossRefGoogle Scholar
  10. 10.
    Duflot, M., et al.: Probabilistic model checking of the CSMA/CD, protocol using PRISM and APMC. In: Automated Verification of Critical Systems (AVoCS 2004). Electronic Notes in Theoretical Computer Science Series, vol. 128, pp. 195–214 (2004).  https://doi.org/10.1016/j.entcs.2005.04.012
  11. 11.
    Duflot, M., et al.: Practical applications of probabilistic model checking to communication protocols. In: Gnesi, S., Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 133–150. IEEE (2013).  https://doi.org/10.1002/9781118459898.ch7
  12. 12.
    Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 295–315. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28869-2_15CrossRefGoogle Scholar
  13. 13.
    Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical report 5513, NICTA (2013). http://arxiv.org/abs/1312.7645
  14. 14.
    Friend, G.E., Fike, J.L., Baker, H.C., Bellamy, J.C.: Understanding Data Communications, 2nd edn. Howard W. Sams & Company, Indianapolis (1988)Google Scholar
  15. 15.
    Fruth, M.: Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Leveraging Applications of Formal Methods, Second International Symposium (ISoLA 2006), pp. 290–297. IEEE Computer Society (2006).  https://doi.org/10.1109/ISoLA.2006.34
  16. 16.
    IEEE: IEEE standard for ethernet (2016).  https://doi.org/10.1109/IEEESTD.2016.7428776
  17. 17.
    IEEE: IEEE standard for low-rate wireless networks (2016).  https://doi.org/10.1109/IEEESTD.2016.7460875
  18. 18.
    ISO/IEC 7498–1: Information technology—open systems interconnection—basic reference model: The basic model (1994). https://www.iso.org/standard/20269.html
  19. 19.
    ISO/IEC/IEEE 8802–11: Information technology—telecommunications and information exchange between systems—local and metropolitan area networks—specific requirements—part 11: Wireless LAN medium access control (MAC) and physical layer (PHY) specifications (2018). https://www.iso.org/standard/73367.html
  20. 20.
    Jensen, H.E., Larsen, K.G., Skou, A.: Modelling and analysis of a collision avoidance protocol using Spin and Uppaal. In: The Spin Verification System. Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 33–50. DIMACS/AMS (1996).  https://doi.org/10.7146/brics.v3i24.20005
  21. 21.
    Parrow, J.: Verifying a CSMA/CD-protocol with CCS. In: Aggarwal, S. (eds.) IFIP Symposium on Protocol Specification, Testing and Verification (PSTV 1988), North-Holland, pp. 373–384 (1988)Google Scholar
  22. 22.
    Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (FOCS 1977), pp. 46–57. IEEE (1977).  https://doi.org/10.1109/SFCS.1977.32
  23. 23.
    de Simone, R.: Higher-level synchronising devices in Meije-SCCS. TCS 37, 245–267 (1985).  https://doi.org/10.1016/0304-3975(85)90093-3MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Simpson, W.: The point-to-point protocol (PPP). RFC 1661 Internet Standard (1994). http://www.ietf.org/rfc/rfc1661.txt
  25. 25.
    Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75, 440–469 (2010).  https://doi.org/10.1016/j.scico.2009.07.008MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Zhao, J., Li, X., Zheng, T., Zheng, G.: Removing irrelevant atomic formulas for checking timed automata efficiently. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 34–45. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-40903-8_4CrossRefGoogle Scholar

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  • Rob van Glabbeek
    • 1
    • 2
    Email author
  • Peter Höfner
    • 1
    • 2
  • Michael Markl
    • 1
    • 3
  1. 1.Data61CSIROSydneyAustralia
  2. 2.Computer Science and EngineeringUniversity of New South WalesSydneyAustralia
  3. 3.Institut für InformatikUniversität AugsburgAugsburgGermany

Personalised recommendations