Modeling and Analyzing CSMA/CA Protocol for Energy-Harvesting Wireless Sensor Networks

Abstract

Well-designed wireless sensor networks (WSNs) usually provide vital support for collecting, processing, and forwarding the real-time information in mission-critical applications where medium access control (MAC) protocols determine the channel access control capabilities and the energy consumption properties of these networks. This paper models the MAC protocol of CSMA/CA using timed automata on the message communication and the energy harvesting and analyzes the protocol through model checking of the major CTL properties. The modeling and analysis of CSMA/CA protocol with the comparative experiments give some performance results and also reveal that timing error may cause deadlock, and the accessibility is satisfied if no deadlock exists.

1. Introduction

Wireless sensor networks (WSNs) are multihop self-organizing networks consisting of sensor nodes through wireless communication and usually provide vital support for collecting, processing, and forwarding the real-time information in mission-critical applications, but the networks face many challenges for the limit energy, memory, and computing power in the sensor nodes [1]. One of these challenges is to design the effective medium access control (MAC) protocols, which determine the channel access control capabilities and the energy consumption properties of WSNs [2]. The MAC protocol of CSMA/CA (Carrier Sense Multiple Access with Collision Avoidance) for carrier transmission in WSNs avoids collisions by transmitting only when checking to be sure the channel is idle [3].

Bertocco et al. [4] analyzed the performance of CSMA/CA-based sensor networks for industrial monitoring using the experimental tests on a test bed, which consisted of a wireless sensor network, one personal computer, and a digital oscilloscope. Zhu et al. [5] presented a slotted CSMA/CA scheme MultiCSMA for WSNs and simulated the proposed scheme to validate the performance improvement using the NS2 network simulator. Youn et al. [6] presented a QoS mechanism supporting CSMA/CA for WSNs and theoretically analyzed the proposed method. Chen et al. [7] presented an analytical model for evaluating the CSMA/CA protocol and used NS2 to evaluate the protocol performance in the small-scale application of WSNs. The above-mentioned researches have many interesting discoveries on the CSMA/CA protocol, but we still need to be sure that all explicitly stated properties are satisfied in WSNs.

To more accurately verify the CSMA/CA protocol in energy-harvesting WSNs [8], this paper models CSMA/CA using timed automata and analyzes the protocol using the UPPAAL model checker [9]. The rest of the paper is organized into four sections. Section 2 briefly introduces related work on energy harvesting for WSNs. Section 3 proposes the timed automata models of the CSMA/CA protocol in energy-harvesting WSNs. Section 4 gives the results of UPPAAL model checking and the TinyOS-based comparative experiments. Finally, the conclusions are presented in Section 5.

2. Energy Harvesting for Wireless Sensor Networks

Sensor nodes with limited energy usually prevent WSNs used in many different application areas and may use energy-harvesting technologies to make WSNs perform their functions in long lifetimes [8]. Energy harvesting is a process of obtaining energy from renewable environmental resources such as solar, wind, heat, and vibration. In energy-harvesting WSNs, each sensor node is equipped with one or more collectors to harvest energy from the environment [10]. For example, when using the solar panels as an energy collector, each node can continuously gain energy during the day, which can effectively prolong the network lifetime [11, 12]. In only battery-powered WSNs, the energy of one sensor node gradually decreases over time, while the energy of one sensor node in energy-harvesting WSNs has sustainable power supply in a certain period of time until the node stops or fails.

The MAC protocols for energy-harvesting WSNs may be different from conventional battery-powered WSNs and need some different design criteria, such as environmental adaptability, backlog estimation, and frame length selection [13, 14]. CSMA/CA requires a delay in network activity after each transmission, which is proportionate to the priority level of each device. CSMA/CA may improve access control and serve to reduce collisions in carrier transmission of energy-harvesting WSNs.

3. Modeling CSMA/CA Using Timed Automata

We model CSMA/CA for energy-harvesting WSNs using time automata, which are finite state automata with clock constraints, can be seen as the abstract models of the real-time systems, and are widely used in verifying the correctness of the real-time systems [15].

3.1. Message Communication

In energy-harvesting WSNs using CSMA/CA, one sensor node senses the information and transmits it to the sink node via multihop, during which the listen and sleep mechanism reduces the probability of packet collisions [3]. We set up a set of cursors $nodeid\_t$ to record all nodes. For each $id\in nodeid\_t$ , its action can be described with the timed automata models of $Sender(id)$ and the $Receiver(id)$ . $Sender(id)$ means message sending and $Receiver(id)$ means message receiving. Additionally, a timed automata model of $Clock$ is given for describing a time period.

The timed automata model of message sending is shown in Figure 1. In the model, the initial sleep state is $Down$ ; when receiving the signal $Idle?$ , the node goes into the $Idle$ state, $ActivePeriod$ represents the time period of one node activity, and we use an array $a[i]$ to identify if the channel is idle. $a[i]==-\mathrm{1}$ indicates that the channel of a neighbor node i is idle, and $a[i]==N$ shows that there is a collision between the node and its neighbor node i; that is, the channel is busy. If the channel is busy, the node returns to the state $Idle$ and continues to listen to the channel. If the channel is idle, the node waits for a random time and then sends data with weight value $bk[id]$ to represent a random time. Here, using the weight value can reduce the probability of packet collisions when sending one message.

Figure 1

Timed automata model of message sending $Sender(id)$ .

Figure 2 shows the timed automata model of message receiving. In the model, $Sync?$ indicates the synchronization with $Sender(id)$ . $col\_count$ records the number of collisions the node sends. There are two branches from the $Idle$ state to the $Receive$ state, in which the one branch indicates that the busy channel will increase the number of collisions, empty the channel $Clear(id)$ , and update the energy consumption value at the same time, and the other branch indicates the message will be received in a correct way.

Figure 2

Timed automata model of message receiving $Receiver(id)$ .

As shown in Figure 3, $Clock$ simulates a clock cycle, including the activity time and sleep time of one node, in which sending and receiving messages need to be completed. $Idle!$ represents the synchronization with $Sender(id)$ and $Receiver(id)$ .

Figure 3

Time automata model of $Clock$ .

3.2. Energy Harvesting

In energy-harvesting WSNs, the sensor nodes may have five states, including $Down$ , $Charging$ , $Listening$ , $Transmitting$ , and $Receive$ . As shown in Figure 4, in the initial state, the battery energy is the total energy of one node, and the node goes into $Charging$ at a certain probability. When the energy of the node reaches a standard value, energy charging is stopped and the node enters the $Listening$ state to detect if the channel is idle. If the channel is idle, the node sends data; otherwise, it goes into the waiting stage and listens again after a random time.

Figure 4

State transformations of energy harvesting.

The energy-harvesting WSNs obtain energy from the environment; so when modeling the energy harvesting of the sensor nodes, we need to consider the energy-harvesting rates, which are not uniformly changing as they may be affected by the changes of environmental factors and human interventions, such as the light intensity, the local climate conditions, and the buildings and trees in the shade. In the CSMA/CA using energy harvesting, we focus upon the charging process in energy harvesting and give the timed automata model of energy acquisition $Harvester(id)$ shown in Figure 5.

Figure 5

Time automata model of energy acquisition $Harvester(id)$ .

In Figure 5, the initial state of one node is $Down$ for the sleep status and it goes into $S\mathrm{1}$ with the probability $DC$ and into $S\mathrm{2}$ with the probability $DI$ . If the state of one node goes into $S\mathrm{1}$ and the node receives the broadcast message $GoIdle$ at the same time, the node will go into the $Idle$ state and the residual energy $energy[id]$ is updated, and if $energy[id]<\mathrm{0}$ , the node will die. After the node enters the $S\mathrm{2}$ state, due to the different rate of energy harvesting, the node periodically goes into the $Charging$ state and updates the energy collected from the environment, and when the collected energy from environment $s[id]$ reaches a certain value defined as $MAX$ , the node goes into the $Idle$ state; if $s[id]<\mathrm{M}\mathrm{A}\mathrm{X}$ , the node continues to harvest energy from the environment to charge. In Figure 6, the message $change!$ is broadcasted every $CHANGE\_PERIOD$ time and synchronizes with $change?$ in $Harvester(id)$ .

Figure 6

Time automata model of periodically harvesting energy.

4. Analyzing CSMA/CA Using UPPAAL

We analyze the CSMA/CA protocol in energy-harvesting WSNs using the UPPAAL model checker [9] about the CTL properties such as no deadlock, reachability, and performance factors. The performance is also comparatively evaluated through experiments on TOSSIM simulator [16], which simulates the state-of-the-art TinyOS-based CSMA/CA real applications [13, 14, 17, 18] with the SolarCastalia energy-harvesting model [19]. In the following UPPAAL model checking and experiments, the amount of energy harvested $E_H$ is calculated by (1) [19]; the transmission energy $E_{TX}$ for transmitting K bits of information between two sensor nodes is calculated by (2) [20]; the consumed energy $E_{RX}$ for receiving K bits of information by one sensor node is calculated by (3) [20]. The parameters in analyzing CSMA/CA are shown in Table 1:

$$\begin{array}{cc}& E_H={{\displaystyle \int }}_{t_{\mathrm{1}}}^{t_{\mathrm{2}}}{\lambda }_H{D}_t\hspace{0.17em}dt,\end{array}$$

(1)

$$\begin{array}{cc}& E_{TX}=K\times E_{\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{c}}+{\epsilon }_{fs}\times K\times d^{\mathrm{2}},\end{array}$$

(2)

$$\begin{array}{cc}& E_{RX}=K\times E_{\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{c}},\end{array}$$

(3)

Table 1

Parameters used in analyzing CSMA/CA.

Parameter	Value
Network size in real experiments	≤100
Network size in UPPAAL model checking	≤10
Communication radius	10 m~30 m
Packet length: K	100 bits
Node initial energy: $E_{\mathrm{0}}$	100000 mJ
$${\lambda }_H$$	1
$$E_{\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{c}}$$	100 nJ/bit
$${\epsilon }_{fs}$$	200 pJ/bit/m2

where $D_t$ is the actual measurement energy value, ${\lambda }_H$ is the energy-harvesting weighting value [18], $[t_{\mathrm{1}},t_{\mathrm{2}}]$ is the energy-harvesting time interval, $E_{\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{c}}$ is the energy consumed by the electronics in the transmitter or receiver, and ${\epsilon }_{fs}$ is the energy consumption of the signal power amplifier per square meter.

4.1. No Deadlock

Deadlock refers to blocking between processes. In UPPAAL, the property can be specified by the CTL formula as

$$\begin{array}{cc}& A\left[\right]\mathit{\text{not}}\hspace{0.17em}\hspace{0.17em}deadlock\mathrm{o}\mathrm{r}A\left[\right]!\mathit{\text{deadlock}}.\end{array}$$

(4)

In the energy-harvesting WSNs, we verify the property of CSMA/CA with different timing strategies, which decide the parameter values of $ActivePeriod$ , $MAX$ , and $CHANGE\_PERIOD$ in our proposed models. The UPPAAL and experimental results show that when setting up the correct timing strategies, CSMA/CA has no deadlock; otherwise, the timing errors may cause deadlock.

4.2. Reachability

Reachability refers to the fact that if there are sensor nodes sending message, the nodes receiving the message must exist. In UPPAAL, the property can be specified by the CTL formula as

$$\begin{array}{cc}& \phantom{{{}_{p}F}_q^{}}A\left[\right]\hspace{0.17em}\hspace{0.17em}\mathit{\text{forall}}\hspace{0.17em}\hspace{0.17em}\left(i:\mathit{\text{Nodes}}\right)\mathit{\text{\hspace{0.17em}forall}}\hspace{0.17em}\hspace{0.17em}\left(j:\mathit{\text{Nodes}}\right)\mathit{\text{Sender}}\left(i\right).\mathit{\text{Sent\hspace{0.17em}\hspace{0.17em}\&\&\hspace{0.17em}\hspace{0.17em}Neighbor}}\left(i,j\right)\mathit{\text{imply\hspace{0.17em}Receiver}}\left(j\right).\mathit{\text{Receive}}.\end{array}$$

(5)

The UPPAAL and experimental results of our proposed models show that these models satisfy the reachability if no deadlock exists.

4.3. Collision Probability over Time

The property of collision probability over time can be specified in UPPAAL by the CTL formula as

$$\begin{array}{cc}& \mathrm{Pr}\left[time\le \mathrm{160}\right]\left(<>collision\_times>\mathrm{0}\right)\end{array}$$

(6)

which shows the probability of the fact that there are more than zero collisions if the time is shorter than 160 s.

After 738 times, the confidence value is 0.95 when the probability is in 0.0713, 0.1705. In Figures 7 and 8, the line charts of UPPAAL results show two cases of the collision probability versus time in two different backoff times represented by $bk[id]$ in our proposed models and indicate that the collision probability is growing over time and has different values in different backoff times, which are also presented by the scattered plots of the experimental results.

Figure 7

Case  1 of collision probability versus time.

Figure 8

Case  2 of collision probability versus time.

4.4. Probability of Collision Times

The property of the probability of collision times can be specified in UPPAAL by the CTL formula as

$$\begin{array}{cc}& \mathrm{Pr}\left[collisions\le \mathrm{50000}\right]\left(<>time\ge \mathrm{1000}\right)\end{array}$$

(7)

which shows the probability of the collision times is smaller than 50000 and time is longer than 1000 s.

After 738 times, the confidence value is 0.95 when the probability is in 0.95, 1. In Figure 9, the line chart of UPPAAL results shows one case of the probability distribution of different collision times and indicates that the probability is growing over collision times and the probability of having one collision at least is less than 96%, which are also verified by the scattered plots of the experimental results.

Figure 9

One case of the probability of collision times.

4.5. Probability of Energy Consumption

The property of the probability of energy consumption can be specified in UPPAAL by the CTL formula as

$$\begin{array}{cc}& \mathrm{Pr}\left[power\le \mathrm{50000}\right]\left(<>time\ge \mathrm{1000}\right),\end{array}$$

(8)

where $power=sum(energy\left[i\right]\hspace{0.17em}|\hspace{0.17em}i:nodeid\_t)$ .

The property shows the probability of the power is smaller than 50000 and time is longer than 1000 s. In Figures 10 and 11, the line charts of UPPAAL results show two cases of the probability distribution of energy consumption in two different backoff times represented by $bk[id]$ in our proposed models and indicate that the probability is growing over energy consumption and has different values in different backoff times, which are also verified by the scattered plots of the experimental results.

Figure 10

Case  1 of probability distribution of energy consumption.

Figure 11

Case  2 of probability distribution of energy consumption.

According to the verification results shown in Table 2, we may get the reasonable retreat backoff time through continual adjustments, which cannot only reduce the probability of collision but also reduce energy consumption.

Table 2

Verification results.

Property	Verification result
(1)	It is satisfied when setting up the correct timing strategies.
(2)	It is satisfied if no deadlock exists.
(3)	Collision probability is growing over time and has different values in different backoff time.
(4)	Probability is growing over collision times and the probability of having one collision at least is less than 96%.
(5)	Probability is growing over energy consumption and has different values in different backoff times.

5. Conclusions

The CSMA/CA protocol in energy-harvesting WSNs determines the distribution of channel and communication resources and constructs the underlying network structure which has a great influence upon the network performance. We propose the timed automata models of message sending, message receiving, and energy acquisition in CSMA/CA of energy-harvesting WSNs. The results of analyzing the protocol through UPPAAL model checking reveal some performance trends and show that timing error may cause deadlock, and the accessibility is satisfied if no deadlock exists. In the future work, we will verify and analyze other aspects of the CSMA/CA protocol, such as the collision processes, and help researchers to model, automatically verify, and evaluate the performance more comprehensively.