Modelling and Verification of a Cluster-tree Formation Protocol Implementation for the IEEE 802.15.4 TSCH MAC Operation Mode

TL;DR

This paper models and verifies a cluster-tree formation protocol for IEEE 802.15.4 TSCH networks, revealing scalability issues and identifying scenarios where topology formation fails, using formal methods for analysis.

Contribution

It introduces a formal modeling and verification approach for the cluster-tree formation protocol in TSCH networks, highlighting scalability limitations.

Findings

The protocol has super linear time complexity.

Formal methods identify failure scenarios.

Scalability issues in large networks.

Abstract

Correct and efficient initialization of wireless sensor networks can be challenging in the face of many uncertainties present in ad hoc wireless networks. In this paper we examine an implementation for the formation of a cluster-tree topology in a network which operates on top of the TSCH MAC operation mode of the IEEE 802.15.4 standard, and investigate it using formal methods. We show how both the mCRL2 language and toolset help us in identifying scenarios where the implementation does not form a proper topology. More importantly, our analysis leads to the conclusion that the cluster-tree formation algorithm has a super linear time complexity. So, it does not scale to large networks.

Equations

$$C=\{recv|corecv\to received,send|cosend\to sent\}.$$

$$Node(1,1,\text{CLUSTER\_HEAD},0,0,[],0,0,0),$$

$$\mu X(n:\mathbb{N}:=1).\left([increase]X(n+1)\wedge [\overline{increase}]X(n)\wedge ⟨true⟩true\right)\vee (n\approx \text{MAX\_ID})$$

$$5+2h+\sum _{i=1}^{h-1}\left(7+2^{i}i\right)$$

Full text

1 Introduction

The IEEE 802.15.4 protocol standard is used for low-rate and low-powered Personal Area Networks (PANs). The IEEE 802.15.4e standard was released in 2012 to extend the IEEE 802.15.4 protocol to overcome limitations in performance and reliability [3, 6]. This extension was subsequently incorporated into the IEEE 802.15.4 standard in 2015, and among other changes introduces the Time-Slotted Channel Hopping (TSCH) MAC operation mode, with the goal of ensuring reliability by providing more structure to wireless communication, as well as scalability and robustness by channel hopping [4].

In the TSCH mode, robustness against noise and interference is provided by a mechanism for channel hopping in consecutive units of time called time-slots, and the reliability is provided by communicating according to a deterministic schedule over time-slots. The schedule is created by higher-layer protocols on the PAN coordinator, which is also in charge of initiating and maintaining the PAN.

For multi-hop applications, a logical structure is maintained which is called a topology, and is often a cluster-tree. This structure is used for multi-hop routing and often also for creating schedules. However, as networks become larger and/or denser the problem of designing an algorithm for forming the cluster-tree efficiently becomes non-trivial, and ensuring its correctness becomes difficult.

A problem is that the IEEE 802.15.4 protocol standard is not explicit about many of the operational details of the protocol, including the cluster-tree formation algorithm. Therefore, we used the description of an early implementation [5] and investigated its correctness using the mCRL2 toolset [2, 11]. Our findings were in line with results of simulations by the designers, with substantial saving of time in case of verification compared to simulations. Some, but not all, observations were incorporated in later implementations.

In order to investigate the implementation, we first model the lower layers (including the IEEE 802.15.4 TSCH mode protocol) in mCRL2. This model is presented in Section 3.2. We then model the cluster-tree formation protocol operating on TSCH. This model is quite large and can be found in the model repository. We formally analyse correctness using the mCRL2 model checker. We subsequently present a full argument on the scalability of the algorithm, based on the results derived by verification.

From our analysis we derived a number of guidelines on how to design a better cluster-tree formation protocol (in Section 6). But we do not devise such an alternative protocol, as the purpose of this paper is to show that with relatively little effort formal methods can be of great help in getting insight in the behaviour of protocols used in the realm of wireless networks.

2 Related work

When discussing cluster-trees, we are essentially referring to spanning trees, in which each node is a vertex in the tree, and for every pair of node identifiers ($A$,$B$) there is a unique path between the node with identifier $A$ and the node with identifier $B$ in the tree. The problem of forming a cluster-tree is directly related to the distributed minimum spanning tree (MST) algorithms in an asynchronous setting [14]. However, several assumptions by distributed MST algorithms are in conflict with the situation in wireless sensor networks: links between nodes should be reliable meaning that no collisions or message losses occur, and processes on nodes should have complete knowledge regarding the neighbours of the node. Moreover, in some versions of the distributed spanning tree algorithm the leader or the root node is elected during the course of execution [8, 9], while in the algorithms we consider the root node is fixed.

The general strategy in distributed spanning tree algorithms is to start with a spanning forest, and consistently merge trees until eventually a single spanning tree is formed [14]. However, in IEEE 802.15.4 due to having a single initiator an essentially different approach is taken which forms a tree by a series of waves (i.e., floodings) sent through the network. Therefore, the algorithm presented here fits the definition of echo algorithms in the theory of distributed algorithms [7].

To our knowledge there have been relatively few attempts to rigorously verify the IEEE 802.15.4 protocol up until now. Recently, in [13] the authors used the UPPAAL framework to analyse inconsistencies in slot allocation in an implementation of the distributed synchronous multi-channel extension (DSME) mode of the IEEE 802.15.4 MAC layer protocol. Earlier, in [12] the authors modelled a part of the IEEE 802.15.4 specification using the MODEST language to investigate the influence of clock precision on energy consumption. In any case, this work is one of the first to formally analyse parts of the TSCH operation mode.

3 Modelling the TSCH MAC operation mode

In this section we introduce the service of the TSCH MAC layer as specified in [4]. We also sketch how we model protocols using this MAC protocol. We leave out the details of the channel hopping procedure from the TSCH MAC layer. The channel hopping procedure is an essential part of TSCH, which provides scalability and reliability in communication. However, as the correctness of channel hopping procedures is not a concern in this paper we abstract away all related concepts.

In what follows we first give an informal specification for the TSCH MAC operation mode in Section 3.1. Then, in Section 3.2 we show how the informal descriptions can be encoded formally.

3.1 The TSCH MAC operation mode

In IEEE 802.15.4, 16 channels are available for communication. The TSCH MAC operation mode is time-slotted, and divides time into equally sized chunks called time-slots. For each time-slot on each channel a node can be either a receiver, a transmitter, or not involved (e.g., if it is sleeping).

In TSCH, time-slots have two types: they are either dedicated, meaning that only one transmitter and one or more receivers are involved, or they are shared, meaning that there can be zero, one or more transmitters attempting to transmit a frame and multiple receivers listening. In case of shared time-slots conflicts between transmitters are resolved using CSMA-CA.

For communicating over time-slots, nodes must share a common schedule, which is designed such that their frames do not collide. Otherwise, collisions are a possibility. Let us assume that in a time-slot node $A$ is the transmitter (TX) and node $B$ is the receiver (RX), according to the schedule. The events occurring in the time-slot are as follows: at the beginning of the time-slot both $A$ and $B$ wait for a time period. After waiting, first $B$ starts listening on the channel, then $A$ becomes active and transmits its message. When $A$ is done transmitting the message, it stops and waits for some time. Next, $B$ stops listening and waits. After some time node $A$ starts listening on the channel. Then $B$ becomes active and if it has succeeded in receiving the frame, it transmits an acknowledgement. If not, it does no action. After a while (before the start of the next time-slot) $A$ stops listening. In this way by the end of the time-slot, $A$ and $B$ reliably know the outcome of the communication. Also note that listening starts before the expected transmission time and ends sometime after to allow possible synchronisation imperfections.

In TSCH, nodes have a common understanding of time, and agree on schedules. The schedules are repeated over slotframes, which are a collection of time-slots. A summary of these concepts and their relations is given in Figure 1.

3.2 The two layered model

In this section we outline the formal specification of the general behaviour of the network as a two layered model, with one representing the physical and the TSCH operation mode of the MAC layer of the protocol stack, and the other representing the upper layers. At the same time, we also introduce the mCRL2 formal specification language for specifying and verifying the behaviour of concurrent systems [2].

For the specification of the behaviour the following data types are needed. Let Message_Type be a sort which at least contains the element EMPTY. The inclusion of the element EMPTY is due to the fact that in our approach in modelling broadcasting, in each time-slot we require every node to submit a message to the physical layer. Define:

• [TABLE]

The above ${\bf sort}$ statement defines custom data types. The sort ${\it Message}$ stands for a structured sort, which can be constructed using the function ${\it message}$ applied to the elements that follow. The element ${\it src}$ in ${\it message}$ is the identifier of the transmitter of the message which belongs to the set of natural numbers, channel is the channel over which the message is transmitted, again belonging to the set of natural numbers, type is the type of the message, and data is a list of data carried by the message (payload), which belongs to the set of lists (sequences) of natural numbers.

The sort $\mathit{Traffic}$ is a list of messages. This models all the messages coming from all the sources travelling over all the channels at a certain point in time in the network.

Constants and functions are defined using the ${\bf map}$ statement:

• [TABLE]

The above statement defines two constants with values from the set of natural numbers, as mappings with zero arguments. We use the constant MAX_ID to indicate that $1,\ldots,\texttt{MAX\_ID}$ are identifiers of processes in the network, and the constant NUM_OF_CHANNELS indicates that the channels available are $1,\ldots,\texttt{NUM\_OF\_CHANNELS}$.

Based on the informal specification given in Section 3.1, the behaviour of the network depends on the type of time-slots (dedicated or shared). Here, we only define the behaviour for dedicated time-slots.

We model the physical and MAC layers of the network in a general fashion, such that it applies to any protocol implemented over the dedicated time-slots of TSCH. This is done using the process TSCH. The main purpose of defining this process is to model the peculiarities of phenomena such as broadcasting and collisions using mCRL2.

We model the transmission and receiving of messages using the following ${\bf act}$ statement:

• [TABLE]

Actions represent events occurring in the system, and are the building blocks in defining the behaviour of processes. The action $\mathit{received}$ indicates that a message has been received in the MAC layer and is handed over to the upper layer. Concretely, the MAC layer performs a $\mathit{corecv}$ action and the upper layer performs a $\mathit{recv}$ which synchronise into the $\mathit{received}$ action. Similarly, the action $\mathit{sent}$ means that the upper layer indicates that the MAC layer must send a message. This action is the result of the synchronisation of actions $\mathit{send}$ by the upper layer and $\mathit{cosend}$ by the MAC layer.

The synchronisations are made explicit by a communication set $C$:

[TABLE]

A synchronisation can only take place when both constituent actions are ready and have the same data of type message. The communication operator $\Gamma_{C}$ is used in the process to indicate that these communications are possible. The operator $\nabla_{V}$ only allows actions in the set $V$ to happen. It can be used to enforce communications by only allowing the result of a synchronisation and not the constituent actions. Concretely, when applying $\nabla_{\{\mathit{sent},\mathit{received}\}}$ the result is that actions ${\it cosend}$ and ${\it send}$ cannot be performed independently and must communicate to ${\it sent}$. The same applies to $\mathit{corecv}$, $\mathit{recv}$ and $\mathit{receive}$.

Assuming that the process ${\it TSCH}$ describes the physical and MAC layers and the processes ${\it Node}$ describe the upper layer, a TSCH network with $n=\texttt{MAX\_ID}$ nodes is specified by the process ${\it Network}$:

• [TABLE]

In the following two sections, we give the details on how processes ${\it TSCH}$ and ${\it Node}$ are specified.

3.2.1 Specification of the TSCH process

In this section, we specify the behaviour of the physical and the MAC layers using the mCRL2 language, as the process ${\it TSCH}$. We start out with the $\mathit{TSCH}$ process.

We first define the following functions which enable us to manipulate the traffic in the network:

• [TABLE]

The function $\mathit{findId}$ accepts a node identifier and a list of messages ($\mathit{Traffic}$), and returns the first message from a node with the mentioned identifier in this list, only if such a message exists. The function $\mathit{findChannel}$ accepts a channel number and a list of messages, and returns a list of messages sent on a certain channel. We specify the behaviour of ${\it TSCH}$ using two processes ${\it TSCH}_{1}$ and ${\it TSCH}_{2}$.

The process ${\it TSCH}_{1}$ represents the first stage of the events on the physical layer. In this stage, $\mathit{TSCH}_{1}$ collects from each node $i$ a message to be sent (using the action $\mathit{cosend}$) and adds it to the sent transmissions $\mathit{str}$ such that it will be transmitted in the second stage.

• [TABLE]

The notation $c{\rightarrow}p\Diamond q$ stands for the if-then-else. The operator $\lhd$ is used to put an element at the end of a list. Note that every node should send a message. Nodes which are only listening, communicate EMPTY messages to the TSCH in this stage.

While transmitting messages, collisions may occur on the physical layer. A collision occurs over a channel $c$ if there are at least two messages $m_{1}$ and $m_{2}$ which are on the same channel $c$. In case of a collision on channel $c$, none of the messages sent over channel $c$ are readable and therefore they need to removed when the sent transmissions become the received transmissions in $\mathit{TSCH}$. This behaviour is described using a function ${\it removeCollision}$:

• [TABLE]

The function ${\it removeCollision}$ processes all the messages in the traffic over all channels, and for each channel determines which message is broadcast. The message is then added to the list of results. In case of collision on a channel $c$, an EMPTY message over $c$ is added to the resulting list.

In the second stage, the process ${\it TSCH}_{2}$ checks the channel each node $i$ is operating on using the expression $channel({\it findId}(i,str))$, and picks a message from that channel in the list $rtr$ and delivers it to the node.

• [TABLE]

Upon finishing this stage, the behaviour changes back to process ${\it TSCH}_{1}$. The process ${\it TSCH}$ which represents the complete behaviour of the lower layers is then defined as:

• [TABLE]

3.2.2 General specification of process Node

The general structure of the processes ${\it Node}$ is as follows:

• [TABLE]

In the process $\mathit{Node}$, the number $\mathit{id}$ is the identifier of the node. The parameter $\mathit{ch}$ is the channel the node operates on. The parameter $\mathit{d}$ of sort $\mathit{Data}$ is a placeholder for the rest of the state of a node. In the concrete description of $\mathit{Node}$ $d$ is replaced by $7$ concrete parameters.

Each process $\mathit{Node}$ represents a wireless node with a single antenna which at any time can only be in a transmit mode or a receive mode, based on which the behaviour of a node is split into two main parts, represented by the two summations.

The set $I$ is a finite set of indices $i$ of all conditions $\gamma_{i}$ under which the custom-defined protocol transmits a message. Similarly, the set $J$ is the set of indices $j$ of all conditions $\gamma_{j}$ under which the custom-defined protocol waits for a message. The first summation (choosing over set $I$) represents the behaviour of nodes in the transmit mode. In this mode, if condition $\gamma_{i}$ with data $d$ holds, the node sends a message of type $t_{i}$ over ${\it ch}$, containing data $g_{i}(id,d)$. The antenna is passively exposed to any signal occurring over channel ${\it ch}$ and this is reflected by the subsequent recv action, which records the messages broadcast at the same time over the operating channel. However, being in transmit mode, the node cannot react to this message. Therefore the values of functions $\sigma_{i}$ and $\delta_{i}$ which determine the next state of the node are not affected by the received data.

The second summation (choosing over set $J$) shows the behaviour of nodes in the receive mode. In this mode, a node does not transmit any messages. This particular behaviour is shown by a ${\it send}$ action of a message of type EMPTY over channel $\mathit{ch}$. The ${\it send}$ action is only to inform the ${\it TSCH}$ process of the value of ${\it ch}$. The main part of the behaviour is then expressed by the ${\it recv}$ action. Functions $\sigma^{\prime}_{i}$ and $\delta^{\prime}_{i}$ express the change to the state of the node based on the received data and the previous state.

Note that despite the fact that two communications occur in each time-slot in TSCH, namely transmission of a frame and its acknowledgement, we do not explicitly enforce them in our model. Therefore the user defined protocol may choose to include the acknowledgement in its behaviour by specifying two rounds of communication per time-slot, or to leave the acknowledgements out.

4 The cluster-tree formation protocol

In this section, we specify the cluster-tree formation protocol using mCRL2, and then we present the results of the verification of this protocol which shows the flaws in its design.

4.1 Informal specification

A slotframe in the cluster-tree formation protocol consists of 12 time-slots, out of which two are reserved for the operation of the cluster-tree formation protocol. The idea is that the protocol establishes and maintains a cluster-tree topology in these two time-slots while the network is doing its normal operation in the rest of the time-slots.

Nodes can have one of 4 types. They can be either a cluster head (CH), a cluster slave (CS), a tentative cluster head (TCH), or a free node (FN). In the scenarios that we are interested in, the network starts with one cluster head node and the rest are free nodes. The original cluster head is a gateway node receiving commands from an external source, and it initiates the cluster-tree formation protocol.

The cluster-tree formation protocol takes a distance based approach. For each node, nodes in its broadcast range fall into two categories: close nodes, and other nodes in range. A node estimates the distance of another node based on its received signal strength (RSSI). Upon receipt of a message, a node measures the power of the signal, and compares it to a power threshold and determines the category of the transmitter.

Cluster heads in the network are connected to each other (they form a tree) in a setting in which every cluster head has one parent and a number of children. The original cluster head is an exception and has no parent. Based on this a cluster head is assigned a tier, which shows its distance from the original cluster head, with the original cluster head being assigned tier 0. In addition, each cluster head operates on only two channels: one to communicate with its parent cluster head, and one to communicate with its children. We call these channels the parent channel and the assigned channel respectively.

A cluster head broadcasts a BEACON message on its assigned channel to advertise its presence in the network, according to the scheme that follows. Cluster heads with even-numbered tiers advertise on the first time-slot reserved for cluster-tree formation in a slotframe, and cluster heads with odd-numbered tiers advertise on the second time-slot reserved for cluster-tree formation. Therefore every cluster head gets the chance to advertise once in each slotframe. The BEACON message includes the tier of the transmitter node.

The message is received by all the nodes which are within transmission range, and are listening on the assigned channel of the cluster head. When a free node receives the message, it estimates its distance from the transmitter, and if it is close then it sends an ASSOCIATE message in response and requests to become a cluster slave. A cluster slave operates on the same channel as its parent. Otherwise if the node is not close to the cluster head, it responds with a BEACON_ACK to the request, and the cluster head then sends an ACK_RESPONSE message which contains a wait_time.

When an ACK_RESPONSE message is received by a free node, it becomes a tentative cluster head. A tentative cluster head scans other channels one by one (staying in each for 2 time-slots) until either wait_time expires, or it receives a BEACON from a cluster head which is close and has the same tier. In such a case the node becomes a cluster slave of the close cluster head, as previously explained. This is to achieve approximately the smallest tree in the network which covers all of the nodes.

If a tentative cluster head fails to find a close cluster head and wait_time expires, it moves back to the channel of its parent and listens for a BEACON message. This time it sends an ASSOCIATE message in response and requests to become a child cluster head. The parent then forwards this message to the original cluster head. The original cluster head finds a suitable and possibly unoccupied channel, and sends an ASSOCIATE_ACK message containing the assigned channel to the sender of the request, which is then forwarded to the tentative node, officially granting it the status of a cluster head.

We assume that the network is well connected, meaning that for each two nodes $A$ and $B$ in the network it is possible to deliver a message from $A$ to be $B$ in one or more hops. The main requirements that the above protocol should satisfy in such a network is the following:

• •

Eventually every node in the network becomes either a cluster head or a cluster slave.

Below we present our method to check this property.

4.2 Formal specification of the cluster-tree formation protocol in mCRL2

In this section we explain how the cluster-tree formation protocol introduced in Section 4.1 can be formally specified. Based on the informal specification, we define data types Node_Type and Message_Type as follows:

• [TABLE]

Next, we model the physical topology of the network using the distance of nodes with respect to each other and by declaring the functions inRange and inClose.

• [TABLE]

For two node identifiers $A$ and $B$ the value of the term $\mathit{inClose}(A,B)$ is true if and only if node $A$ is within range of node $B$, and is closer than the threshold. The term $\mathit{inRange}(A,B)$ is true, if and only if node $A$ is within range of node $B$ but farther away than the threshold.

Using these data types, and the general definition of a TSCH node, the basic declaration of the process modelling a node is:

• [TABLE]

In this process, if a node is of type cluster head or cluster slave, $\mathit{pid}$ is the identifier of the parent of the node and $\mathit{pc}$ is the channel over which the parent of the node operates. Given type ${\it Pair}$ which defines any pair of natural numbers, a cluster head keeps a record of all its children and their assigned channels as a list of pairs of natural numbers. The parameter ${\it tier}$ is the tier of the cluster head or cluster slave and ${\it state}$ is the internal state of the node which in general holds information such as the node’s history and what the node should do next. Finally, ${\it timeslot}$ is the information regarding the clock of the node, which is used by the node to keep its actions in sync with the rest of the network.

We model a TSCH network in which the original cluster head is initialised to the state:

[TABLE]

and every other node with identifier $n\in\{2,\ldots,\texttt{MAX\_ID}\}$ is initialised to: $\mathit{Node}(n,c_{n},\texttt{FREE},0,0,[],0,0,0)$, where $c_{n}$ is a channel number, chosen based on a scenario of interest. The process $\mathit{Network}$ given in Section 3.2 then models a network of $n$ nodes running the cluster-tree formation protocol.

4.3 Verification of the cluster-tree formation protocol in mCRL2

We want to verify the property: “eventually every node in the network is either a cluster head or a cluster slave”. In order to check the state of the whole network throughout its operation, we introduce a new action ${\it increase}$. In the specification of the process ${\it Node}$, every time the type of the node changes to CLUSTER_HEAD or CLUSTER_SLAVE, the action ${\it increase}$ is performed. Then the property “eventually every node in the network is either a cluster head or a cluster slave” can be expressed as “for every possible computation at some finite point in the future the action ${\it increase}$ has occurred $\texttt{MAX\_ID}-1$ times”. This statement formulated in the modal $\mu$-calculus looks as follows:

[TABLE]

For a network of 3 nodes, we manually generated all the topologies in which the network is well connected. For all those cases, we verified the ${Network}$ process against property (1) using the mCRL2 model checker. The toolset generated a number of counterexamples for the property.

Below we present three basic scenarios in which the network does not behave as desired. In our representation of topologies that follow, we use dashed lines to show two nodes being in range and full lines to show two nodes being close. Moreover, we give the type of the nodes by annotating them by CH, CS, F and T which stand for cluster head, cluster slave, free and tentative respectively.

Collision of acknowledgements. In the cluster-tree formation protocol whenever a free node receives a BEACON message, it responds with an acknowledgement right away. However, in the physical topology given to the right, since the BEACON is sent by broadcast there could be more than one node responding on the same channel, and this leads to collision.

CHFF

Collision of associate messages. Once a tentative cluster head reaches the timeout without finding a closer cluster head, it returns to the parent channel and sends an associate message to the parent. However, in the physical topology given here it is likely that two nodes send associate messages at the same time to the same cluster head. This leads to a collision, and in such a case the specification does not state how the tentative cluster heads should proceed.

CHTT

Narrow bridge problem. Consider the physical topology to the right, in which the connection of the original cluster head to the rest of the nodes in the network is only possible through a close node. In this case, the direct child of the cluster head becomes a cluster slave. Subsequently since the cluster slave does not send out BEACON messages in its vicinity, the rest of the network never joins the tree. This problem arises due to the fact that the condition for becoming a cluster slave does not take the importance of the position of a node into account.

CHCSF

For certain topologies, the narrow bridge problem is inevitable for every possible execution. Moreover, given some fixed topologies and the initial conditions in which all nodes start on the same channel, collision of acknowledgements is also inevitable for every possible execution. This means that in these cases, there is no execution of the protocol in which a full cluster-tree is achieved.

4.4 Scalability of the cluster-tree formation protocol

The main problem with the cluster-tree formation protocol however is its performance. In this section we give an argument for how the performance scales when the number of nodes in the network grows, by finding lower bounds on the termination time of the cluster-tree formation protocol. In order to proceed with our investigation we consider topologies in which the narrow bridge problem does not arise, and we solve the issue of collision of acknowledgements by changing the protocol as follows. After a free node receives a BEACON message, it does not acknowledge it, but instead it generates a random waiting time. If the cluster head is close, the free node waits for the random time and then it associates with the cluster head and becomes a cluster slave. Otherwise, it directly changes its type to tentative and follows the procedure we earlier specified.

In the next step we take some of the witnesses of property (1), i.e., paths in the state space over which the property holds, and we calculate the amount of time it takes for the procedure to complete in a network of three nodes, with the physical topology given in Figure 2(a). In order to find witnesses we use the lpsxsim tool, which given a linearised mCRL2 process specification allows the manual generation of traces. Using this tool and our knowledge of the protocol we look for the smallest sequence of actions for which property (1) is satisfied.

Let $\texttt{MAX\_ID}=3$, $\texttt{NUM\_OF\_CHANNELS}=3$ and the minimum time for nodes to remain tentative be 2. We find an initial configuration for which the network model satisfies property (1), and has the smallest trace for a witness. In the witness we find the minimum time for the formation of the cluster is 8 time-slots. In the setting of a slotframe which reserves 2 out of 12 time-slots for cluster-tree formation and maintenance, this means that the cluster-tree formation takes at least 3 slotframes to complete. Suppose that a time-slot is 120 milliseconds long, then it takes 5760 milliseconds for the algorithm to form a tree.

We now give our argument on how performance scales for larger networks. First, consider a tentative node with $\textit{id}=A$ which wants to join a cluster head in tier $t$. Since every association needs to be handled by the original cluster head, the cluster head on tier $t$ has to forward the association request to its parent on tier $t-1$, and so forth until it reaches the original cluster head. In the same manner the association response needs to travel back to node $A$. However, in case other requests arrive at a cluster head which is involved in this process at the same time, the performance of the protocol quickly deteriorates. Therefore for a node at tier $t$ the association procedure takes at least $2t$ to complete.

For simplicity consider the physical topology to be according to a balanced binary tree of height $h$. An example of such a network is given in Figure 2(b), in which node $1$ is the original cluster head. The edges in this tree indicate the pairs of nodes that are in range of each other. The tree structure resulting from the protocol in such a case is identical to the physical topology.

We decompose the balanced binary tree into triples of nodes, as shown in Figure 2(b). Let $0<i<h$, each triple consists of a parent with node height $i-1$ and its children with node height $i$. Consider a point in the execution of the cluster-tree formation protocol in which the parent node has already joined the network but its two children are still free. Using the witness we derived earlier, we see that excluding the messages ASSOCIATE and ASSOCIATE_ACK the minimum time required for message exchange inside the triple (BEACON message and tentative waiting time) is 5 time-slots. Therefore, following our earlier observation for a single node with node height $i$, the time for the completion of the procedure is $5+2i$, and for two nodes this time is $5+4i$.

Consider the ideal case in which: all messages avoid collisions, every cluster head is involved in at most one association at a time and every free node listens on the channel of its future parent exactly as soon as the parent sends a beacon. Since in a balanced binary tree the number of nodes with node height $i<h$ is exactly $2^{i}$ the association of all the nodes with height $i$ takes $5+2^{i+1}i$ time-slots to complete.

There is one exception for simultaneous handling of associations which happen in the two separate subtrees of the original cluster head. In this case two associations which arrive at the original cluster head only within $2$ time-slots from each other can be processed by the original cluster head. By using this insight the minimum time for association of all nodes of height $i$ becomes $7+2^{i}i$.

And lastly, we know that a balanced binary tree of height $h$ has at least 1 node with node height $h$, therefore the lower bound on the number of time-slots needed for the formation of the cluster-tree in such a topology is given by the formula:

[TABLE]

As an example, consider a network with 500 nodes. A balanced binary tree with 500 nodes has height $h=8$. This means that the formation of the cluster-tree in such a network takes at least $27$ minutes to complete in the extremely ideal case. With the introduction of collisions, random back-offs, and the increase of the number of channels this time increases substantially.

Based on the lower bound given by formula (2), we conclude that for a network of $n$ nodes the optimal time for the execution of the cluster-tree formation protocol is $\Omega(n\log(n))$, and hence super linear.

5 Further details on modelling and verification

The activities of modelling and verification of the cluster-tree formation protocol was done in a period of five weeks, with approximately 100 hours of effort. This included becoming familiar with the domain and consultation with the designers and domain experts. The generated state spaces are so small that tool effort for verification is negligible.

Our models and the modal formula are included in the model repository:

ClusterFormation.mcrl2: the mCRL2 specification corresponding to Sections 4.1 and 3.2.

• -

ClusterFormation_NoAcks.mcrl2: the mCRL2 specification of the protocol with no BEACON acknowledgements, as described in Section 4.4.

• -

property1.mcf: the correctness property of the protocol (formula (1)).

6 Conclusion

In this paper we showed how specification and verification of a network protocol by the mCRL2 language and toolset can give insights to the operation of wireless network protocols. Remarkably, by only modelling a few number of nodes (3 nodes in our case) we were able to detect issues in the protocol design such as scalability. The key message here is that by modelling on a suitable abstraction level and with a sufficient number of components, one can effectively reason about the performance and correctness of wireless network protocols.

Based on our findings, we formulate a number of guidelines which can help in the general design of protocols using the IEEE 802.15.4 TSCH MAC layer operation mode:

• •

Broadcast messages should not be acknowledged (which is already common knowledge).

• •

Any other sort of communication triggered by single shared events (like a broadcast), should use back-off schemes or channel sensing strategies to promote robustness.

The following guidelines are specific to the design of an improved cluster-tree formation protocol:

• •

A node should collect information regarding its neighbours before becoming a cluster slave.

• •

To achieve better performance, the cluster-tree formation should be done during a dedicated, intensive period with no slotframe, in which only cluster-tree formation messages are exchanged.

• •

The association requests should not be forwarded one by one to the original cluster head.