# Model-Checking Driven Design of QoS-Based Routing Protocol for Wireless Sensor Networks

Authors: Zhi Chen; Ya Peng; Wenjing Yue
Journal: Journal of Sensors
 (2015)

---

## Abstract

Accurate and reliable routing protocols with Quality of Service (QoS) support determine the mission-critical application efficiency in WSNs. This paper proposes a model-checking design driven framework for designing the QoS-based routing protocols of WSNs, which involves the light-weight design process, the timed automata model, and the alternative QoS verification properties. The accurate feedback of continually model checking in the iterative design process effectively stimulates the parameter tuning of the protocols. We demonstrate the straightforward and modular characteristics of the proposed framework in designing a prototype QoS-based routing protocol. The prototype study shows that the model-checking design framework may complement other design methods and ensure the QoS implementation of the QoS-based routing protocol design for WSNs.


---

## Body

## 1. Introduction

Wireless sensor networks (WSNs) as the multihop self-organizing networks usually provide vital support for mission-critical applications [1] but have many design challenges such as routing [2], topology control [3], and coverage [4]. Quality of Service (QoS) support may determine the routing efficiency and effectiveness of real-time WSNs due to the constrained energy supply, bandwidth, and delay [5].In order to design the QoS-based routing protocols for WSNs, we usually verify and evaluate the correctness and performance of these protocols using testing, simulation, and formal verification. Testing usually analyzes the implementations of these protocols and finds the protocol defects, but it is often achieved at a cost and cannot analyze all the conditions of these protocols. Simulation is commonly used in QoS-based routing protocol analysis, but it cannot analyze all the protocol behaviors. Formal verification, for example, model checking, can describe and analyze QoS-based routing protocols accurately and can make up the deficiency of testing and simulation [6–8]. Moreover, model checking can drive the design of some applications and systems, such as the interactive systems [9] and the web application [10] and may design the QoS-based routing protocols from model driven engineering to verification driven engineering [11].In order to effectively design the QoS-based routing protocols for the mission-critical applications of WSNs, the paper proposes a model-checking driven design framework and demonstrates the effectiveness and advantages by the accurate feedback of continually model checking in the iterative design process. The rest of the paper is organized into five sections. Section2 briefly introduces related work. Section 3 presents the model-checking driven design framework. Section 4 introduces a prototype of the QoS-based routing protocol. Section 5 presents the protocol verification and design improvement. Finally, the conclusions are offered in Section 6.


## 2. Related Work

Akkaya and Younis [12] presented an energy-aware QoS routing protocol for WSNs with best-effort traffic and validated the effectiveness of the protocol through simulation. Ben-Othman and Yahya [13] proposed a QoS aware multipath routing protocol based on the concept of service differentiation to control the delay and then used the NS-2 simulations to evaluate the performance of the protocol for WSNs. Sun et al. [14] presented a game-theoretic approach to coordinate the QoS routing for WSNs and used NS-2 to verify its performance with simulations. Cheng et al. [15] used the geographic opportunistic routing for QoS provisioning in WSNs and evaluated the protocol through NS-2 simulations and tests on the hardware nodes. Hu et al. [16] proposed a multihop heterogeneous cluster-based optimization algorithm (MHCOA) for WSNs and also used NS-2 simulation to show the better performance of MHCOA in heterogeneous WSNs.Akbaş and Turgut [17] presented a routing protocol with QoS support for wireless sensor and actor networks and carried out a series of simulations in OPNET modeler to analyze the performance of the protocol. Hammoudeh and Newman [18] presented an adaptive routing protocol with QoS metrics to meet application requirements of WSNs and used the Dingo WSN simulator to evaluate the performance of the protocol. Tschirner et al. [19] presented the automata-based models for biomedical sensor networks (BSN) and successfully used the driven model-checking technique to complement the simulation techniques to validate QoS properties of BSN.In the above-mentioned related work, the simulation-based method is the main design verification technique for the QoS-based routing protocols of WSNs [20], but it is possible that some errors which may only occur under special conditions cannot be found in the simulations; thus the QoS metrics may not meet the routing requirements of WSNs in the mission-critical applications.


## 3. Model-Checking Driven Design Framework

To ensure that the QoS-based routing protocol can save energy, reduce the transmission delay, increase the probability of successful transmission to the sink node, and provide high QoS for WSNs we propose the model-checking driven design framework consisting of the design process, the timed automata model, and the verification properties.


### 3.1. Design Process

In the model-checking driven design framework for the QoS-based routing protocols of WSNs, the model-checking driven design process shown in Pseudocode1 uses the iterative and incremental development. A QoS-based routing protocol of WSNs is designed through repeated cycles and in smaller parts at one time and iteratively enhanced through model checking until the full protocol is implemented. At each iteration, the design improvement is made and one new QoS metric is added.Pseudocode 1:Model-checking driven design process.
Input the network (0,1
,
…
,
n
-
1), QoS metrics (m
0
,
m
1
,
…
,
m
k
-
1)
Design QoSRP: the prototype of the QoS − based routing protocol with the metricm
0
i
←
0
while (i
<
k) do
Model QoSRP using Timed Automata
Verify QoSRP via Model Checking and Output the verification results
Evaluate the verification results and improve QoSRP
i
←
i
+
1
if (i
<
k)
Redesign QoSRP with the metricsm
0
,
…
,
m
i
endif
endwhile
Output QoSRPIn the model-checking driven design process, we assume there aren nodes in WSNs and m QoS metrics (
m
0
,
m
1
,
…
,
m
k
-
1
) from the application requirements of WSNs and, firstly, design one prototype of the QoS-based routing protocol using the QoS metric of m
0, namely, QoSRP, which we can react with and is simple enough to be understood and implemented easily; then QoSRP is modeled using timed automata [21, 22], verified via model checking, and improved as a result of evaluating the verification results. After taking the first iteration of the design improvement, we add one new QoS metric as the new feature to redesign QoSRP and continue to perform the process.


### 3.2. Timed Automata Model

In the model-checking driven design framework, we define the timed automata model, including the timed automaton of the sink node and the timed automaton of the sensor nodes according to the behavior of nodes in WSNs.The timed automaton of the sink node is formally described as(1)
Initial
,
y
<
=
INITIAL_DELAY
,
→
y
=
=
INITIAL_DELAY
Received
,
x
<
=
R
,
broad
!
,
(2)
Received
,
x
<
=
R
,
⟶
Initial
,
y
<
=
INITIAL_DELAY
,
stop
?
.The timed automaton of the sensor nodes is formally described as(3)
Listen
,
time
<
=
backoff
,
→
time
=
=
backoff
Broadcasting
,
,
broad
?
,
(4)
T
x
,
x
<
=
TRANSMIT
,
stop
!
⟶
Broadcasting,
,
,
(5)
Broadcast
,
WaitTime
<
=
TIMEOUT
,
→
WaitTime
=
=
TIMEOUT
T
x
,
x
<
=
TRANSMIT
,
,
(6)
Broadcast
,
WaitTime
<
=
TIMEOUT
,
⟶
Received
,
x
<
=
R
,
start
?
,
(7)
Received
,
x
<
=
R
,
⟶
Broadcasting
,
,
stop
?
.In the timed automata model of WSNs,b
r
o
a
d is the probe information sending channel of the sink node, s
t
a
r
t is the message transmitting starting channel of the sensor nodes, and s
t
o
p is the message transmitting ending channel of the sensor nodes. When the timed automata work, the clock values increase all with the same speed, and, along the state transitions in every automaton of the sink node or one sensor node, clock values being compared to integers form the guards, which may enable or disable state transitions and inhabit the possible behaviors in the mission-critical applications of WSNs.


### 3.3. Verification Properties

In the model-checking driven design framework, we select four CTL properties, including no deadlock, network connectivity, delivery rate of data packet, and transmission delay [19], which may be used for model checking.(1) No Deadlock. This property can be formally specified as follows:(8)
A
not  deadlock
.(2) Network Connectivity. Any node of WSNs should communicate with the sink node, no matter directly or through the multihop paths within a certain time, and the isolated nodes should not exist in theory. This property can be formally specified as follows:(9)
A
<
>
received
i
>
0
.(3) Packet Delivery Success Rate. The channel access failure, data packet collision, information transmission error caused by the thermal noise, and external interference may result in the loss of the packets. Packet delivery success rate refers to the ratio of the number of packets successfully received by the sink node and the number of packets sent to the sink node by the sensor nodes. For example, if the sensor nodes send 10 packets to the sink node, we need to verify the packet delivery rate reaching 90%, this property can be formally specified as follows:(10)
A
periods
X
>
=
10
imply
received
X
>
=
9
.(4) Transmission Delay. Transmission delay is the effectiveness of data packets, which must be transmitted to the sink node through the multihop paths in a bounded time. This property of the transmission delay time not exceeding M of sending a packet to the sink node by the sensor node i can be formally specified as follows:(11)
A
time
i
<
=
M
.


## 3.1. Design Process

In the model-checking driven design framework for the QoS-based routing protocols of WSNs, the model-checking driven design process shown in Pseudocode1 uses the iterative and incremental development. A QoS-based routing protocol of WSNs is designed through repeated cycles and in smaller parts at one time and iteratively enhanced through model checking until the full protocol is implemented. At each iteration, the design improvement is made and one new QoS metric is added.Pseudocode 1:Model-checking driven design process.
Input the network (0,1
,
…
,
n
-
1), QoS metrics (m
0
,
m
1
,
…
,
m
k
-
1)
Design QoSRP: the prototype of the QoS − based routing protocol with the metricm
0
i
←
0
while (i
<
k) do
Model QoSRP using Timed Automata
Verify QoSRP via Model Checking and Output the verification results
Evaluate the verification results and improve QoSRP
i
←
i
+
1
if (i
<
k)
Redesign QoSRP with the metricsm
0
,
…
,
m
i
endif
endwhile
Output QoSRPIn the model-checking driven design process, we assume there aren nodes in WSNs and m QoS metrics (
m
0
,
m
1
,
…
,
m
k
-
1
) from the application requirements of WSNs and, firstly, design one prototype of the QoS-based routing protocol using the QoS metric of m
0, namely, QoSRP, which we can react with and is simple enough to be understood and implemented easily; then QoSRP is modeled using timed automata [21, 22], verified via model checking, and improved as a result of evaluating the verification results. After taking the first iteration of the design improvement, we add one new QoS metric as the new feature to redesign QoSRP and continue to perform the process.


## 3.2. Timed Automata Model

In the model-checking driven design framework, we define the timed automata model, including the timed automaton of the sink node and the timed automaton of the sensor nodes according to the behavior of nodes in WSNs.The timed automaton of the sink node is formally described as(1)
Initial
,
y
<
=
INITIAL_DELAY
,
→
y
=
=
INITIAL_DELAY
Received
,
x
<
=
R
,
broad
!
,
(2)
Received
,
x
<
=
R
,
⟶
Initial
,
y
<
=
INITIAL_DELAY
,
stop
?
.The timed automaton of the sensor nodes is formally described as(3)
Listen
,
time
<
=
backoff
,
→
time
=
=
backoff
Broadcasting
,
,
broad
?
,
(4)
T
x
,
x
<
=
TRANSMIT
,
stop
!
⟶
Broadcasting,
,
,
(5)
Broadcast
,
WaitTime
<
=
TIMEOUT
,
→
WaitTime
=
=
TIMEOUT
T
x
,
x
<
=
TRANSMIT
,
,
(6)
Broadcast
,
WaitTime
<
=
TIMEOUT
,
⟶
Received
,
x
<
=
R
,
start
?
,
(7)
Received
,
x
<
=
R
,
⟶
Broadcasting
,
,
stop
?
.In the timed automata model of WSNs,b
r
o
a
d is the probe information sending channel of the sink node, s
t
a
r
t is the message transmitting starting channel of the sensor nodes, and s
t
o
p is the message transmitting ending channel of the sensor nodes. When the timed automata work, the clock values increase all with the same speed, and, along the state transitions in every automaton of the sink node or one sensor node, clock values being compared to integers form the guards, which may enable or disable state transitions and inhabit the possible behaviors in the mission-critical applications of WSNs.


## 3.3. Verification Properties

In the model-checking driven design framework, we select four CTL properties, including no deadlock, network connectivity, delivery rate of data packet, and transmission delay [19], which may be used for model checking.(1) No Deadlock. This property can be formally specified as follows:(8)
A
not  deadlock
.(2) Network Connectivity. Any node of WSNs should communicate with the sink node, no matter directly or through the multihop paths within a certain time, and the isolated nodes should not exist in theory. This property can be formally specified as follows:(9)
A
<
>
received
i
>
0
.(3) Packet Delivery Success Rate. The channel access failure, data packet collision, information transmission error caused by the thermal noise, and external interference may result in the loss of the packets. Packet delivery success rate refers to the ratio of the number of packets successfully received by the sink node and the number of packets sent to the sink node by the sensor nodes. For example, if the sensor nodes send 10 packets to the sink node, we need to verify the packet delivery rate reaching 90%, this property can be formally specified as follows:(10)
A
periods
X
>
=
10
imply
received
X
>
=
9
.(4) Transmission Delay. Transmission delay is the effectiveness of data packets, which must be transmitted to the sink node through the multihop paths in a bounded time. This property of the transmission delay time not exceeding M of sending a packet to the sink node by the sensor node i can be formally specified as follows:(11)
A
time
i
<
=
M
.


## 4. A Prototype of the QoS-Based Routing Protocol: QoSRP

We design a prototype of the QoS-based routing protocol for WSNs, namely, QoSRP. Assuming there aren nodes in WSNs, including one sink node and n
-
1 sensor nodes, i represents one node, where i
∈
{
0,1
,
…
,
n
-
1
} and the node 0 is the sink node. w
(
i
,
j
) is the link cost between the node i and the node j, where w
(
j
,
i
)
=
w
(
i
,
j
), w
(
i
,
i
)
=
0, i
∈
{
0,1
,
…
,
n
-
1
}, and j
∈
{
0,1
,
…
,
n
-
1
}. d
[
i
] is the end-to-end optimal transmission cost of the node i and the sink node. We define G
=
(
V
,
S
), where V
∪
S
=
{
0,1
,
…
,
n
-
1
},  V represents the set of sensor nodes without the optimal next-hop neighbor nodes, and S is the set of sensor nodes with the optimal next-hop neighbor nodes.(1) Initialization. In an initial state, every node in WSNs broadcasts the “detecting” message consisting of its location information, ideal transmitting radius, and residual energy information by flooding communication and calculates the link costs between it and other nodes according to the received “detecting” messages in the network. We select two QoS metrics, including the transmitting delay and the residual energy over the data transfer paths for calculating the link costs. All link costs of w
(
i
,
j
) are stored in the node i and if the node i does not receive the “detecting” message of the node j, w
(
i
,
j
)
=
M
A
X
C
O
S
T, where M
A
X
C
O
S
T is the ideal maximum value. Then, the sink node starts the process of obtaining the least cost paths. At first, S
=
{
0
}, therefore, we can get(12)
d
i
=
w
i
,
0
,
i
≠
0
,
0
,
i
=
0
.(2) Iteratively Updating the End-to-End Optimal Transmission Costs. For the node i in WSNs, where i
∈
S, it updates its d
[
i
] according to (3). Consider(13)
d
i
=
min
⁡
d
i
,
d
k
+
w
k
,
j
,
k
∈
V
.According to (14), QoSRP selects k
∈
S as the node in the optimal path, removes k from S, and adds k into V. Consider(14)
d
k
=
min
⁡
d
i
i
∈
S
.(3) Finding the Optimal Path and Steadily Sending Data. The sink node periodically broadcasts a message to form one optimal path; other nodes select a node as the parent node within the set of V until all nodes can route to the sink node. After forming one optimal path, the sensor nodes steadily send data to the sink node via the path in one period.


## 5. Protocol Verification and Design Improvement

### 5.1. Protocol Modeling

We model QoSRP based on the timed automata model using the model checker UPPAAL [23]. In usual scenarios, all sensor nodes are modeled with the parametric timed automata in UPPAAL.First of all, we set up a set of identifiersn
o
d
e
_
i
d to record all nodes. Assuming that there are n sensor nodes in WSNs, n
o
d
e
_
i
d
=
{
0,1
,
2
,
…
,
n
-
1
}. In QoSRP, the identifier of the sink node is 0, and the identifier of one other node is i
d, where i
d
∈
{
1,2
,
…
,
n
-
1
}. The behaviors of one sensor node in WSNs can be described using two-timed automaton: S
i
n
k and N
o
d
e
(
i
d
). The timed automaton of S
i
n
k shown in Figure 1 describes the sink node, and the timed automaton of N
o
d
e
(
i
d
) shown in Figure 2 is responsible for message sending and receiving of other sensor nodes.Figure 1
Timed automaton model ofS
i
n
k.Figure 2
Timed automaton model ofN
o
d
e
(
i
d
).Not all nodes in a real-time system are turned on simultaneously, and we constrain the turn-on times of sensor nodes in[
0
,
I
N
I
T
I
A
L
_
D
E
L
A
Y
] during which any sensor node can be turned on. In Figure 1, a
c
k
[
0
]
[
t
m
p
] indicates whether an acknowledge message of the node t
m
p is received by the sink node and before the sink node receives the acknowledge message, a
c
k
[
0
]
[
t
m
p
]
=
0.s
t
a
r
t
[
n
o
d
e
_
i
d
] and s
t
o
p
[
n
o
d
e
_
i
d
], respectively, indicate that one node starts transmitting messages and ends a message transmission;s
t
a
r
t
[
n
o
d
e
_
i
d
]
? and s
t
o
p
[
n
o
d
e
_
i
d
]
? are synchronized with s
t
a
r
t
[
n
o
d
e
_
i
d
]
! and s
t
o
p
[
n
o
d
e
_
i
d
]
!. b
r
o
a
d
! means that the sink periodically sends probe information and is synchronization with b
r
o
a
d
?; t
o
p
o
l
o
g
y
[
n
o
d
e
_
i
d
]
[
n
o
d
e
_
i
d
] indicates the connection matrix of the nodes in WSNs. r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
] represents the number of packets sent to the sink node by the node n
o
d
e
_
i
d and also ensures that the node can eventually connect to the sink node if r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
]
>
0.In Figure2, the time automaton of N
o
d
e
(
i
d
) is divided into two phases. The first phase in N
o
d
e
(
i
d
) is to find out the minimum cost path from the node to the sink node, and the second phase is to the transmit data. In N
o
d
e
(
i
d
), r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
] represents the number of packets received by the node from the other node n
o
d
e
_
i
d, and p
e
r
i
o
d
s
[
n
o
d
e
_
i
d
] represents the number of packets sent by the node n
o
d
e
_
i
d. We can compare r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
] and p
e
r
i
o
d
s
[
n
o
d
e
_
i
d
] to illustrate the packet transmission success rate.In Figure2, P
[
N
o
d
e
_
i
d
] indicates the shortest distances of the node n
o
d
e
_
i
d to the sink node, and C
[
N
o
d
e
_
i
d
]
[
N
o
d
e
_
i
d
] is the link communication cost between two nodes. In N
o
d
e
(
i
d
), the variable of t
m
p records the identifier of the node sending messages. N
o
d
e
(
i
d
) follows the task processing mechanism of first-come, first-served in TinyOS [24] and considers the transmission delay in modeling message sending. Message transmission may need a few seconds, change the order of message sending and receiving, and affect the protocol implementation, so it cannot be ignored. Therefore we add the variable of x simulating the message delay, where x
≤
D
E
L
A
Y and DELAY is the maximum value of the message transmission delay.


### 5.2. Protocol Verification

We verify QoSRP about the properties such as no deadlock, network connectivity, delivery rate of data packet, and transmission delay [19]. Table 1 is the verification results in the first iteration in which the QoS metric is the residual energy over the data transfer paths, and it shows that the performance properties were not satisfied if the sensor nodes send fewer packets to the sink node, and the packet successful delivery rates did not satisfy the network QoS requirements.Table 1
Verification results in the first iteration.
Property
Network size
Results
CPU (s)
Memory (MB)
A
[
] not deadlock
5
Y
258.23
31.36
A
[
] not deadlock
6
Y
5640.44
1933.5
A<>  received[2] > 0
5
Y
326.67
93.45
A<> received[2] > 0
6
Y
633.52
530.5
A
[
] periods[1] < 6
5
N
12.24
112.56
A
[
] periods[1] < 7
5
Y
13.34
112.55
A
[
] periods[3] < 2
5
N
11.86
112.62
A
[
] periods[3] < 3
5
Y
12.11
112.58
A
[
] periods[5] < 2
5
N
12.56
112.62
A
[
] periods[5] < 3
5
Y
12.97
112.55
A
[
] periods[1] < 5
6
N
12.83
112.57
A
[
] periods[2] < 3
6
N
56.74
630.29
A
[
] (periods[2] >= 10) imply (received[2] >= 8)
5
Y
11.64
112.59
A
[
] (periods[2] >= 10) imply (received[2] >= 9)
5
N
5.25
107.63
A
[
] (periods[2] >= 10) imply (received[3] >= 7)
5
Y
11.58
112.53
A
[
] (periods[2] >= 10) imply (received[3] >= 8)
5
N
4.12
106.66
A
[
] (periods[2] >= 10) imply (received[4] >= 5)
5
Y
11.63
112.64
A
[
] (periods[2] >= 10) imply (received[4] >= 6)
5
N
4.95
106.68
A
[
]
time[2] < 50
5
N
0.763
26.02
A
[
]
time[2] < 80
5
N
63.63
161.99
A
[
]
time[2] < 100
5
Y
360.5
431.13


### 5.3. Design Improvement

According to the verification results shown in Table1, the performance of the current QoSRP still requires to be improved, so we continue to tune the parameters shown in Figures 1 and 2, such as I
N
I
T
I
A
L
_
D
E
L
A
Y, T
R
A
N
S
M
I
T, M
A
X
_
M, T
I
M
E
O
U
T, and M
A
X
_
P
R
I
C
E, and optimize QoSRP through model checking.Now we combine the two QoS metrics of the transmitting delay and the residual energy over the data transfer paths to redesign QoSRP. The pseudocode of the redesigned QoSRP in one period is given in Pseudocode2. According to the model-checking driven design framework, the new QoSRP is reevaluated through model checking and Table 2 presents the verification results which show a better performance of the protocol.Table 2
Verification results in one next iteration.
Property
Network size
Results
CPU (s)
Memory (MB)
A
[
] not deadlock
5
Y
259.15
32.36
A
[
] not deadlock
6
Y
5587.29
2001.5
A<> received[2] > 0
5
Y
324.65
94.66
A<> received[2] > 0
6
Y
613.37
535.12
A
[
] periods[1] < 6
5
Y
13.16
112.55
A
[
] periods[1] < 7
5
Y
13.55
112.79
A
[
] periods[3] < 2
5
Y
11.59
112.16
A
[
] periods[3] < 3
5
Y
12.51
113.69
A
[
] periods[5] < 2
5
Y
12.97
112.79
A
[
] periods[5] < 3
5
Y
12.48
112.28
A
[
] periods[1] < 5
6
Y
12.65
112.32
A
[
] periods[2] < 3
6
N
56.29
631.55
A
[
] (periods[2] >= 10) imply (received[2] >= 8)
5
Y
12.15
114.43
A
[
] (periods[2] >= 10) imply (received[2] >= 9)
5
Y
5.65
108.63
A
[
] (periods[2] >= 10) imply (received[3] >= 7)
5
Y
12.01
113.18
A
[
] (periods[2] >= 10) imply (received[3] >= 8)
5
Y
4.23
105.08
A
[
] (periods[2] >= 10) imply (received[4] >= 5)
5
Y
12.03
111.98
A
[
] (periods[2] >= 10) imply (received[4] >= 6)
5
Y
4.98
105.76
A
[
]
time[2] < 50
5
N
0.754
25.92
A
[
]
time[2] < 80
5
Y
63.78
162.03
A
[
]
time[2] < 100
5
Y
361.4
430.18Pseudocode 2:Pseudocode of the redesign QoSRP.
Input the network (0,1
,
…
,
n
-
1), QoS metrics (Residual_Energy,  Transmitting_Delay)
Ouput QoSRP: the impoved prototype of the QoS − based  routing  protocol
BEGIN
for node (i
←
0  to  n
-
1)
Broadcast Detecting_Message(L
o
c
a
t
i
o
n
i, T
r
a
n
s
m
i
t
t
i
n
g
_
r
a
d
i
u
s
i, R
e
s
i
d
u
a
l
_
e
n
e
r
g
y
i)
endfor
for node (i
←
0  to  n
-
1)
for node (j
←
0  to  n
-
1)
// Calculatew
(
i
,
j
)  only for verifications
w
i
,
j
=
T
r
a
n
s
m
i
t
t
i
n
g
_
r
a
d
i
u
s
R
e
s
i
d
u
a
l
_
e
n
e
r
g
y
i // ⋅  for the normalization function
endfor
for node (i
←
1  to  n
-
1)
Updated
[
i
]
endfor
repeat
AdjustG
←
(
V
,
S
)
Evalute QoS
until Find one optimal path
for node (i
←
1  to  n
-
1)
Sending data via the optimal path
endfor
END


## 5.1. Protocol Modeling

We model QoSRP based on the timed automata model using the model checker UPPAAL [23]. In usual scenarios, all sensor nodes are modeled with the parametric timed automata in UPPAAL.First of all, we set up a set of identifiersn
o
d
e
_
i
d to record all nodes. Assuming that there are n sensor nodes in WSNs, n
o
d
e
_
i
d
=
{
0,1
,
2
,
…
,
n
-
1
}. In QoSRP, the identifier of the sink node is 0, and the identifier of one other node is i
d, where i
d
∈
{
1,2
,
…
,
n
-
1
}. The behaviors of one sensor node in WSNs can be described using two-timed automaton: S
i
n
k and N
o
d
e
(
i
d
). The timed automaton of S
i
n
k shown in Figure 1 describes the sink node, and the timed automaton of N
o
d
e
(
i
d
) shown in Figure 2 is responsible for message sending and receiving of other sensor nodes.Figure 1
Timed automaton model ofS
i
n
k.Figure 2
Timed automaton model ofN
o
d
e
(
i
d
).Not all nodes in a real-time system are turned on simultaneously, and we constrain the turn-on times of sensor nodes in[
0
,
I
N
I
T
I
A
L
_
D
E
L
A
Y
] during which any sensor node can be turned on. In Figure 1, a
c
k
[
0
]
[
t
m
p
] indicates whether an acknowledge message of the node t
m
p is received by the sink node and before the sink node receives the acknowledge message, a
c
k
[
0
]
[
t
m
p
]
=
0.s
t
a
r
t
[
n
o
d
e
_
i
d
] and s
t
o
p
[
n
o
d
e
_
i
d
], respectively, indicate that one node starts transmitting messages and ends a message transmission;s
t
a
r
t
[
n
o
d
e
_
i
d
]
? and s
t
o
p
[
n
o
d
e
_
i
d
]
? are synchronized with s
t
a
r
t
[
n
o
d
e
_
i
d
]
! and s
t
o
p
[
n
o
d
e
_
i
d
]
!. b
r
o
a
d
! means that the sink periodically sends probe information and is synchronization with b
r
o
a
d
?; t
o
p
o
l
o
g
y
[
n
o
d
e
_
i
d
]
[
n
o
d
e
_
i
d
] indicates the connection matrix of the nodes in WSNs. r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
] represents the number of packets sent to the sink node by the node n
o
d
e
_
i
d and also ensures that the node can eventually connect to the sink node if r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
]
>
0.In Figure2, the time automaton of N
o
d
e
(
i
d
) is divided into two phases. The first phase in N
o
d
e
(
i
d
) is to find out the minimum cost path from the node to the sink node, and the second phase is to the transmit data. In N
o
d
e
(
i
d
), r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
] represents the number of packets received by the node from the other node n
o
d
e
_
i
d, and p
e
r
i
o
d
s
[
n
o
d
e
_
i
d
] represents the number of packets sent by the node n
o
d
e
_
i
d. We can compare r
e
c
e
i
v
e
d
[
n
o
d
e
_
i
d
] and p
e
r
i
o
d
s
[
n
o
d
e
_
i
d
] to illustrate the packet transmission success rate.In Figure2, P
[
N
o
d
e
_
i
d
] indicates the shortest distances of the node n
o
d
e
_
i
d to the sink node, and C
[
N
o
d
e
_
i
d
]
[
N
o
d
e
_
i
d
] is the link communication cost between two nodes. In N
o
d
e
(
i
d
), the variable of t
m
p records the identifier of the node sending messages. N
o
d
e
(
i
d
) follows the task processing mechanism of first-come, first-served in TinyOS [24] and considers the transmission delay in modeling message sending. Message transmission may need a few seconds, change the order of message sending and receiving, and affect the protocol implementation, so it cannot be ignored. Therefore we add the variable of x simulating the message delay, where x
≤
D
E
L
A
Y and DELAY is the maximum value of the message transmission delay.


## 5.2. Protocol Verification

We verify QoSRP about the properties such as no deadlock, network connectivity, delivery rate of data packet, and transmission delay [19]. Table 1 is the verification results in the first iteration in which the QoS metric is the residual energy over the data transfer paths, and it shows that the performance properties were not satisfied if the sensor nodes send fewer packets to the sink node, and the packet successful delivery rates did not satisfy the network QoS requirements.Table 1
Verification results in the first iteration.
Property
Network size
Results
CPU (s)
Memory (MB)
A
[
] not deadlock
5
Y
258.23
31.36
A
[
] not deadlock
6
Y
5640.44
1933.5
A<>  received[2] > 0
5
Y
326.67
93.45
A<> received[2] > 0
6
Y
633.52
530.5
A
[
] periods[1] < 6
5
N
12.24
112.56
A
[
] periods[1] < 7
5
Y
13.34
112.55
A
[
] periods[3] < 2
5
N
11.86
112.62
A
[
] periods[3] < 3
5
Y
12.11
112.58
A
[
] periods[5] < 2
5
N
12.56
112.62
A
[
] periods[5] < 3
5
Y
12.97
112.55
A
[
] periods[1] < 5
6
N
12.83
112.57
A
[
] periods[2] < 3
6
N
56.74
630.29
A
[
] (periods[2] >= 10) imply (received[2] >= 8)
5
Y
11.64
112.59
A
[
] (periods[2] >= 10) imply (received[2] >= 9)
5
N
5.25
107.63
A
[
] (periods[2] >= 10) imply (received[3] >= 7)
5
Y
11.58
112.53
A
[
] (periods[2] >= 10) imply (received[3] >= 8)
5
N
4.12
106.66
A
[
] (periods[2] >= 10) imply (received[4] >= 5)
5
Y
11.63
112.64
A
[
] (periods[2] >= 10) imply (received[4] >= 6)
5
N
4.95
106.68
A
[
]
time[2] < 50
5
N
0.763
26.02
A
[
]
time[2] < 80
5
N
63.63
161.99
A
[
]
time[2] < 100
5
Y
360.5
431.13


## 5.3. Design Improvement

According to the verification results shown in Table1, the performance of the current QoSRP still requires to be improved, so we continue to tune the parameters shown in Figures 1 and 2, such as I
N
I
T
I
A
L
_
D
E
L
A
Y, T
R
A
N
S
M
I
T, M
A
X
_
M, T
I
M
E
O
U
T, and M
A
X
_
P
R
I
C
E, and optimize QoSRP through model checking.Now we combine the two QoS metrics of the transmitting delay and the residual energy over the data transfer paths to redesign QoSRP. The pseudocode of the redesigned QoSRP in one period is given in Pseudocode2. According to the model-checking driven design framework, the new QoSRP is reevaluated through model checking and Table 2 presents the verification results which show a better performance of the protocol.Table 2
Verification results in one next iteration.
Property
Network size
Results
CPU (s)
Memory (MB)
A
[
] not deadlock
5
Y
259.15
32.36
A
[
] not deadlock
6
Y
5587.29
2001.5
A<> received[2] > 0
5
Y
324.65
94.66
A<> received[2] > 0
6
Y
613.37
535.12
A
[
] periods[1] < 6
5
Y
13.16
112.55
A
[
] periods[1] < 7
5
Y
13.55
112.79
A
[
] periods[3] < 2
5
Y
11.59
112.16
A
[
] periods[3] < 3
5
Y
12.51
113.69
A
[
] periods[5] < 2
5
Y
12.97
112.79
A
[
] periods[5] < 3
5
Y
12.48
112.28
A
[
] periods[1] < 5
6
Y
12.65
112.32
A
[
] periods[2] < 3
6
N
56.29
631.55
A
[
] (periods[2] >= 10) imply (received[2] >= 8)
5
Y
12.15
114.43
A
[
] (periods[2] >= 10) imply (received[2] >= 9)
5
Y
5.65
108.63
A
[
] (periods[2] >= 10) imply (received[3] >= 7)
5
Y
12.01
113.18
A
[
] (periods[2] >= 10) imply (received[3] >= 8)
5
Y
4.23
105.08
A
[
] (periods[2] >= 10) imply (received[4] >= 5)
5
Y
12.03
111.98
A
[
] (periods[2] >= 10) imply (received[4] >= 6)
5
Y
4.98
105.76
A
[
]
time[2] < 50
5
N
0.754
25.92
A
[
]
time[2] < 80
5
Y
63.78
162.03
A
[
]
time[2] < 100
5
Y
361.4
430.18Pseudocode 2:Pseudocode of the redesign QoSRP.
Input the network (0,1
,
…
,
n
-
1), QoS metrics (Residual_Energy,  Transmitting_Delay)
Ouput QoSRP: the impoved prototype of the QoS − based  routing  protocol
BEGIN
for node (i
←
0  to  n
-
1)
Broadcast Detecting_Message(L
o
c
a
t
i
o
n
i, T
r
a
n
s
m
i
t
t
i
n
g
_
r
a
d
i
u
s
i, R
e
s
i
d
u
a
l
_
e
n
e
r
g
y
i)
endfor
for node (i
←
0  to  n
-
1)
for node (j
←
0  to  n
-
1)
// Calculatew
(
i
,
j
)  only for verifications
w
i
,
j
=
T
r
a
n
s
m
i
t
t
i
n
g
_
r
a
d
i
u
s
R
e
s
i
d
u
a
l
_
e
n
e
r
g
y
i // ⋅  for the normalization function
endfor
for node (i
←
1  to  n
-
1)
Updated
[
i
]
endfor
repeat
AdjustG
←
(
V
,
S
)
Evalute QoS
until Find one optimal path
for node (i
←
1  to  n
-
1)
Sending data via the optimal path
endfor
END


## 6. Conclusions

The QoS-based routing protocols are the mission-critical application requirements of WSNs and involve many verification and evaluation techniques such as testing, simulation, and formal verification. This paper proposes a model-checking driven framework for designing these protocols, including the iterative design process, the timed automata model, and the alternative verification properties. We design a prototype of the QoS-based routing protocol and demonstrate continuing improving the protocol using the proposed framework and UPPAAL model checking. The results of the prototype study show that the model-checking driven design framework is a straightforward and modular method and supports the light-weight iterative redesign for designing QoS-based routing protocols of WSNs, and the feedback of continually model checking accurately drives the performance improving of the protocols of real-time WSNs.



---

*Source: 716561-2015-06-22.xml*