=Paper=
{{Paper
|id=Vol-1431/paper9
|storemode=property
|title=Model-Based Verification of the DMAMAC Protocol for Real-time Process Control
|pdfUrl=https://ceur-ws.org/Vol-1431/paper9.pdf
|volume=Vol-1431
|dblpUrl=https://dblp.org/rec/conf/vecos/SomappaPK15
}}
==Model-Based Verification of the DMAMAC Protocol for Real-time Process Control==
https://ceur-ws.org/Vol-1431/paper9.pdf
Model-Based Verification of the DMAMAC
Protocol for Real-time Process Control
Admar Ajith Kumar Somappa Andreas Prinz Lars M Kristensen
Bergen University College University of Agder Bergen University College
University of Agder andreas.prinz@uia.no lmkr@hib.no
aaks@hib.no
Medium Access Control (MAC) protocols are responsible for managing radio communication that constitute
the main energy consumer in wireless sensor-actuator networks. The Dual-Mode Adaptive MAC (DMAMAC)
protocol is a recently proposed MAC protocol for process control applications in industrial automation. The
goal of the DMAMAC protocol is to improve energy efficiency along with addressing real-time requirements
for process control applications. The DMAMAC protocol switches between two operational modes that
correspond to the two main states in process control: the transient state and the steady state. The state-
switch is a safety critical function of the DMAMAC protocol (along with other functional properties) motivating
the application of formal verification techniques. In this article, we use timed automata and the Uppaal tool to
verify the design of the DMAMAC protocol. We have created a time-based model in Uppaal that constitutes a
formal specification of the DMAMAC protocol. Using this model, we have successfully verified key properties
of the DMAMAC protocol, thereby increasing confidence in the design of the protocol.
Model checking, Timed automata, Medium Access Control Protocols, Wireless Sensor Actuator Networks
WSAN. MAC protocols govern the communication
and control the use of the radio on each node
1. INTRODUCTION in the network. The radio module is the dominant
consumer of energy in wireless nodes. The Dual-
A Wireless Sensor Actuator Network (WSAN) (Aky- Mode Adaptive MAC (DMAMAC) protocol is a
ildiz and Kasimoglu (2004)) consists of sensors and recently proposed MAC protocol in (Kumar S. et al.
actuators that use radio to send, relay, and receive (2014)) for process control applications. The protocol
information. WSANs are used in a wide range of is aimed to provide an energy efficient solution.
domains including process- and factory automation, The DMAMAC protocol was proposed for NCSs
smart home automation, and health-care. Feedback- with real-time and energy efficiency requirements. In
based control loops that use wired or wireless so- particular, it targets process control applications that
lutions are collectively known as Networked Con- fluctuate between two states of operation: steady
trol Systems (NCS) (Hespanha et al. (2007)). NCS and transient. Fig. 1 shows a typical process control
mainly use wired communication systems, but are with two states. The transient state corresponds to
increasingly adopting wireless communication. The the process state with large and frequent change
salient feature of a wireless solution is the reduction in measurements of physical quantities, resulting in
in cost and size compared to the use of wired net- a high data rate. The steady state refers to the
works. The use of wireless communication, however, process state with measurements contained within
also has shortcomings and it has not yet become the a controlled range of values, thus requiring less
de-facto replacement for wired solutions. The limi- data transfer. An example is process control for
tations of wireless solutions include low-bandwidth, chemical reactors. The varying physical quantities
energy efficiency, signal interference, and packet- are temperature and pressure which are measured
loss. Energy efficiency in particular is an important by sensors. This can be controlled by varying the
concern when devices are battery powered. inflow of chemicals to the chemical reactors and
Wireless solutions are made up of a collection of using coolants, controlled by actuators. The state-
protocols that cater for different functions. Medium switch is a safety critical feature of the DMAMAC
Access Control (MAC) is one of the functions that protocol and can benefit from formal verification to
are critical to the proper operation of the entire ensure proper functioning.
protocol, the slot scheduling is done statically
and offline prior to deployment. The focus of the
DMAMAC protocol is to provide an energy efficient
solution along with efficient switching between
the two operational modes. It requires a different
model to represent the features of the DMAMAC
protocol than the one used for the LMAC protocol.
In (Tschirner et al. (2008)), the authors have
focused mainly on modelling the Chipcon CC2420
transceiver. This work is related in terms of their
Figure 1: Process control states
use of a packet collision model and how collisions
are observed. We use a collision model similar
Model-checking is a powerful technique for verifica-
to (Tschirner et al. (2008); Fehnker et al. (2007)).
tion of protocol designs. Model-checking allows for
With the extension of Statistical Model-Checking
exhaustive verification and has been widely used on
(SMC) features, Uppaal can also be used to assess
related protocols (see, e.g., (Fehnker et al. (2012,
performance related queries as shown in the case
2007); Tschirner et al. (2008)). Verification in the
study (David et al. (2011)) of the Lightweight Medium
early design phase can be used to ensure the
Access Control (LMAC) protocol.
behavioral correctness of protocols. Model-checking
assists in discovering design faults by exhaustively 1.2. Outline
traversing all possible execution traces of a given
The rest of the article is organised as follows. In
model. Furthermore, model-checking tools can pro-
Sect. 2 we briefly introduce the DMAMAC protocol.
vide error-traces to failure states, thus assisting
For extensive details, we refer to (Kumar S. et al.
in resolving any discovered design issues. Uppaal
(2014)). Section 3 describes in detail the constructed
(David et al. (2011)) is a modelling and verification
Uppaal model of the DMAMAC protocol. As part
tool-suite that supports model checking of real-time
of this, we briefly introduce the constructs of timed
systems. In addition to model-checking and verifica-
automata as implemented in Uppaal, and perform
tion, Uppaal also supports simulation which can be
some initial validation of the protocol model. In Sect.
used to provide useful insights into the operation of
4 we complete the validation of the constructed
a protocol.
model. The verification of the protocol for different
In this article, we apply the Uppaal tool to analyze deployment configurations is discussed in Sect. 5.
qualitative features of the DMAMAC protocol. We Finally in Sect. 6 we sum up the conclusions and
present a formal specification of the DMAMAC discuss future work. The reader is assumed to be
protocol in the form of a network of timed automata familiar with the basic concepts and operation of
and verify safety properties related to the absence MAC protocols, including superframes and slots,
of faulty states. Additionally, we verify real-time and the principles of Time Division Multiple Access
properties including switch delay and maximum (TDMA) and Carrier Sense Multiple Access (CSMA).
data delay. The timed modelling of the DMAMAC
protocol is based on a Finite State Machine (FSM)
representation of the sensors, actuators, and the
sink node in the WSAN network configuration under 2. DMAMAC PROTOCOL
consideration. The DMAMAC protocol (Kumar S. et al. (2014))
1.1. Related Work has two operational modes catering for the two
states of process control applications: transient
Uppaal has been widely used to model and verify mode and steady mode. The protocol is based
communication protocols (see, e.g., (Fehnker et al. on Time-Division Multiple Access (TDMA) for
(2012); Tschirner et al. (2008); Fehnker et al. data communication and a Carrier Sense Multiple
(2007)). The Lightweight Medium Access Control Access (CSMA)-TDMA hybrid for alert message
(LMAC) (Fehnker et al. (2007)) protocol is the communication. The basic functioning of the protocol
closest MAC protocol modelling related to the is based on the GinMAC protocol (Suriyachai
work presented in this article. The LMAC and the et al. (2010)) proposed for industrial monitoring
DMAMAC protocols are two distinct protocols with and control. The network topology of the DMAMAC
distinct goals, and differ significantly in their base protocol consists of sensor nodes, actuator nodes,
features. The LMAC protocol is a self-organising and a sink. The sensor nodes are wireless nodes
protocol with nodes selecting their own slots i.e., with sensing capability which sense a given area
time duration allocated for data transfer. The focus and update the sink by sending the sensed data.
in the LMAC protocol verification is on efficient slot The actuator nodes are wireless nodes equipped
selection and collision detection. In the DMAMAC with actuators, which act on the data performing a
physical operation. It is also possible to have wireless
nodes with both sensors and actuators. The sink is
a computationally powerful (relative to the nodes)
wire powered node which collects the sensed data,
performs data processing on it, and then sends the
results to corresponding actuators.
Figure 3: The transient superframe of the DMAMAC
protocol
2.1. Transient mode
The transient mode is designed to imitate the tran-
sient state operation in process control. During tran-
sient state, the process changes rapidly generating
data at a faster rate relative to the steady mode.
During the transient mode operation, the DMAMAC
protocol uses the transient superframe shown in Fig.
3. The superframe includes a data part for data
transfer from the sensors to the sink, followed by a
data part with data being sent from the sink to the
actuators, and then a sleep part. The data part also
Figure 2: The network topology for DMAMAC protocol includes a notification message slot from the sink
to all nodes, and a sink processing slot. A typical
transient mode operation cycle is described below:
Similar to the GinMAC protocol, the network
deployment for the DMAMAC protocol is based on • A notification message is sent from the
a tree topology as shown in Fig. 2. The solid lines sink to all the nodes. The notification mes-
between nodes represent data communication. The sage includes control data like state-switch
dashed lines represent nodes which can hear each message and time-synchronization. Time-
other, but which have no direct data communication synchronization is an integral part of TDMA
with each other. Each level in the tree topology is based protocols.
ranked (marked with “R#”, # is 1 or 2), with the sink • The data part is executed with data transmis-
having the lowest rank number and the farthest leaf sion from sensors to sink and then to actuators.
nodes having the highest rank number. This ranking
• The sleep part is executed where all sensors
is exploited in the alert message sending procedure.
and actuators enter sleep mode in order to
Firstly, we discuss the key assumptions that were improve energy efficiency. This part represents
made to support the design of the protocol. Further, the situation where all nodes are in sleep
we explain in brief the working of the two operational mode. Individually, the nodes are in sleep
modes and the respective superframes they use. mode when they are not performing other
tasks.
• The nodes are assumed to be time synchro-
nized via an existing time synchronization pro- 2.2. Steady Mode
tocol. Thus, the time synchronization mecha-
The steady mode operation is designed to operate
nism is not defined as a part of the protocol.
during the steady state of the controlled process.
• The sink is assumed to be powerful, and it can The steady superframe used in the steady mode
reach all nodes in one hop. operation is shown in Fig. 4. In addition to the
• A pre-configured static network topology with parts that also exist in the transient superframe,
no mobility is assumed. the steady superframe contains an alert part. The
• A single slot accommodates both a data packet alert part is used to ensure that the state-switch
and a corresponding acknowledgement. from steady to transient occurs whenever a sensor
detects a threshold interval breach in its reading.
This threshold is set by the sink when the switch
from transient to steady is made. Note that w.r.t
Figure 4: The steady superframe of the DMAMAC protocol
(Kumar S. et al. (2014)) a slightly modified steady defines a threshold interval within which the sensor
mode superframe is used. There are notification readings should lie, and informs the sensors about
slots placed at the end of each transient (Nt) part. this threshold interval. During the entire steady
This is done to facilitate immediate application of mode operation, the sensors constantly monitor for a
alert, and making a state-switch. In the alert part, threshold breach. When there is a breach, the sensor
one slot is allocated to each level or to nodes with node waits until its alert slot, then notifies its parent,
the same rank. All the nodes in the same rank have which in turn forwards the alert towards the sink.
the possibility to send an alert message in this slot. The sink then informs the nodes in the network to
The alert sending method is described later. A typical switch to transient in its immediate next notification
steady mode operation cycle is as follows: message.
• A notification message is followed by the data 2.4. Alert Message
and the sleep part, similar to the working in
An alert message is the message created by the
transient mode operation.
sensor nodes to notify the sink that a state-switch is
• (Alert part) Sensor nodes that have alert mes- required. The sensor nodes choose a random delay
sages to be communicated use appropriate in the slot before transmitting the alert message. At
slots provided for each rank to notify parents the completion of the time duration of the random
about the alert. This is relayed towards the sink delay, the nodes sense the channel to prevent
which then makes the switch to the transient collision. If a node during channel assessment
state. In an absence of alert, sensor nodes still detects another node sending an alert message,
wake up on their alert receive slot and then then it just drops its alert message. Collisions are
enter sleep mode until the next notification slot. still possible, e.g., when two nodes choose the same
• In the alert part, the notification slot is placed random delay or when two senders cannot listen to
at the end. This is to ensure a quick transition each other but the receiver can listen to both. Nodes
between the two states. All regular nodes check for a change of operational mode following the
wake up in this slot, and receive a notification sending of the alert. If no change occurs (because of
message from the sink. Alert notification to collision) the nodes save the alert and send the alert
change superframes is sent here. again in the next alert slot.
2.3. Change of superframes
3. THE DMAMAC UPPAAL MODEL
A process switches between two states: transient
and steady. The DMAMAC protocol follows these Uppaal (David et al. (2011)) is a tool-set based
states via its transient and steady mode operation. on timed automata for model-checking of real-
There are two switches possible: transient to steady time systems. It is an integrated tool environment
and steady to transient. The latter is a critical that supports modeling, simulation, validation, and
switch since the data rate in transient is higher verification. An abstract representation of a real-time
and it is important to accommodate the higher data system in the form of a model is structured as a
rate in transient state. The switch from transient to network of timed automata. The query language of
steady is decided by the sink, which determines if Uppaal allows for verification of safety, reachability,
the process is in steady state based on previous liveness, and time-bounded properties. In Uppaal,
readings. When the sink decides to make the switch, models are constructed as a network of templates
it informs all the nodes in the network to change based on timed automata. Templates are used to
their mode of operation. The message is sent via represent independent entities (e.g. a sensor node).
a notification message from the sink. When the Uppaal consists of two simulators: a symbolic and a
sink node switches from transient to steady, it concrete simulator. The symbolic simulator is used to
inspect the execution of the model step by step. For CSMA procedure that may be used in
certain queries, Uppaal outputs traces which can be conjunction with DMAMAC.
viewed in the symbolic simulator. This is useful for
• The collision caused due to the use of CSMA
pin-pointing error locations and sequences of events
has effects on the state-switch procedure.
that lead to errors/faults. The symbolic simulator also
A simple collision model is used, where we
shows all the templates in the model and message
record collision when two or more nodes send
sequence charts (MSC) can be used to visualize
packets at the same time. Collision results in
communication between different processes. The
failure of the packets, thus affecting the state-
symbolic simulator also allows interactive step-wise
switch procedure.
simulation of the model. Along with features similar
to the symbolic simulator, the concrete simulator A channel synchronization variable choice is used
has the added advantages of firing transitions at a to force enabled transmissions. This is a modeling
specified time. For extensive detail on modeling in artifact and is not part of the protocol as such. In
Uppaal, we refer to (Behrmann et al. (2004)). Uppaal, execution of models can stay in a location
indefinitely even after outgoing edges are enabled.
3.1. Model design decisions and assumptions
To force the model execution to continue via enabled
We use a non-deterministic timed automata model outgoing edges, an urgent channel synchronization
to verify the properties of the DMAMAC protocol. is required.
The constructed model has several sources of non-
3.2. Sink Model
determinism including the delay for sending alert
messages in nodes, and the decision made by the The sink model is shown in Fig. 5. We have used
sink to change from the transient mode to the steady colors in the automaton locations to differentiate
mode. Given the design of alert messages, collisions between states. Both the sink and the node
are possible when sending alert messages. We use automata begin in an initial location Start. The
a simplified collision model, detailed later in this sink initiates the startup procedure of the network
section. The sink and sensor/actuator nodes have using a broadcast synchronization channel startup
separate timed automata models. Local clocks are on the edge towards the StateController location.
used for each automaton. A global clock is used for The function INITIALIZE () is used to set proper values
a common network time reflecting the assumption to local and global variables. The sink reaches
on time synchronisation between the nodes. The the StateController location upon having executed
main aim of the verification of the DMAMAC protocol the startup procedure of the network. The node
model is to check that the two modes of operations automata synchronize with the channel variable
are working correctly given the presence of non- startup, and reach the StateController location.
deterministic choices (like collision) during execution
The StateController location represents an event
and the delays that may occur.
handler for handling transition between different
Below, we discuss the assumptions and design states in the state-machine. The sink model uses
decisions made during the construction of the a local clock variable “x”, which is active in all
Uppaal model for the DMAMAC protocol. states indicated by “x0 == 1”. “x0 == 0” can be
used to pause the clock counter. This is used as
• Packets are abstractly modeled without pay-
an invariant on all states to represent continuously
load. The messages or packets exchange
running time. It also includes an invariant x ≤
mechanism is represented by channel syn-
currentM axSlots ∗ 10 to prevent it from being in
chronization in the Uppaal model.
the state beyond the maximum timeframe of the
• A time synchronization mechanism is provided active superframe (transient or steady). A typical
using clock variables in Uppaal. This can be slot time in WSANs is 10 milliseconds, and this we
considered as a way of implementing the time use the unit “ms” for time in our model. Given the
synchronization between nodes assumed by time unit of “ms”, the variable currentMaxSlots is
the DMAMAC protocol. multiplied by 10 to obtain the slot-time. The use of the
StateController location is also similar to the self-
• An exact model of CSMA results in a
message handler in the commonly used OMNeT++
rather complex model. Instead, we use
(Varga and Hornig (2008)) framework for MAC
a representative CSMA procedure, which
protocols. The function of this particular handler is
imitates the service and effects of actual
to check the self-message that it receives, and to
CSMA on the working of the protocol. The
act on the message by choosing an appropriate next
effects include skipping packet transmission
state. Also, it determines the next state which is then
on detection of ongoing transmission and
sent as a self-message. The automaton changes
also collision. This makes our model and
between the different locations (states) in the model
verification independent of the particular
Figure 5: Uppaal Model of the sink
based on the local variable currentSlot, and the local done via the edge with only one select statement
clock variable x. (change : int[0, 1]). As a symbolic representation, we
have used a guard x == (currentSlot ∗ 10) + 1 on
The Notification location is reached when the sink
these edges, and an invariant x ≤ (currentSlot ∗
is due to send a notification message. The notifi-
10) + 1 on location Notification to indicate a delay
cation message is sent by the sink, and received
of 1 ms for message transmission. Both these edges
by other nodes in the network. This is represented
use a function SINK R ESET (), which resets the sink
by the broadcast channel regNotify[change], where
variables at the beginning of a new superframe, and
change carries a message of the status of the
implements changing of superframes.
Boolean variable changeSuperframe. The change-
Superframe variable is true when the sink needs to The Sleep location is reached when the sink
indicate to the nodes a change in superframes to or nodes do not have any active operations to
switch the mode of operation. For both the steady to be conducted in the current slot. The edge to
transient switch and the transient to steady switch, Sleep is guarded by a Boolean function IS S LEEP ()
the sink uses changeSuperframe. which checks if the current slot is a sleep slot.
We use the urgent broadcast channel choice
The switch from transient to steady is decided
(model artifact) to force this transition whenever
by the sink. There are two separate notification
IS S LEEP () evaluates to true. In the absence of
edges for transient mode and steady mode. In the
this channel variable, the model can continue to
transient mode, the sink decides if it has to switch
be in the location StateController forever even
to steady mode based on the random selection
when IS S LEEP () is true. The location Sleep has an
statement (i : int[1, 10]) and the obtained change
invariant x <= currentSlot ∗ 10 which indicates that
value is sent over the channel. In the absence
during execution, the control can be in the location
of real inputs a random selection is used. The
as long as the time does not exceed the value
edge with select statements (i : int[1, 10]) and
currentSlot, which holds the value of the slot at which
(change : int[0, 1]) is used in transient mode.
the sink should wake up for its next event. This is set
The second select statement (change : int[0, 1])
by the function CALCULATE WAKEUP () when Sleep is
is a modeling artifact used to be able to send the
reached.
value of changeSuperframe over the channel via
the synchronization variable regNotify[change]. The The location Sent is reached when the sink
guard change == changeSuperf rame makes sure sends data in its data slot. The Received location
that the select statement selects the same value as is reached when the sink receives any sensor
the changeSuperframe variable. data, and then sends an ACK via channel
synchronization. Location Received has an invariant
In the steady mode, a switch is based on alert
x ≤ (currentSlot ∗ 10) + 2. This invariant is used
from nodes. The notification for the steady mode is
Figure 6: Uppaal Model of a regular sensor/actuator node
to add a delay of 2 ms as a representation for the the node is in its notification slot (receive) in
time required for data communication. A follow up either of the two types of superframes. The
guard on the ACK sending edge x == (currentSlot∗ nodes then synchronize on the channel variable
10) + 2 makes sure that the delay is applied. Upon regNotify[change] from the sink, and reset the node
sending or receiving of ACK synchronization, the variables using the function NODE R ESET () based on
local variable currentSlot is incremented. the value of the variable change.
Lastly, the location ReceiveAlert is reached when The node model works similar to the sink model for
it is the sink’s turn to receive an alert. This sleep, sent (data), received (data), and alert receive.
is determined by the alert levels defined in the This means that in locations Sleep, Sent, Received,
myLevel array variable represented by the guard and ReceiveAlert the node and the sink model have
rxSlot[currentSlot] == myLevel[sinkId]. The sink the same modeling elements. Further, the location
stays in the location for an entire slot duration (10 SendAlert which handles the crucial part of alert
ms), and waits for any alerts from nodes it can message sending is required by the protocol for the
listen to. The CAN L ISTEN ( I ) function is used as a switch of operational mode from steady to transient.
guard to make sure that the sink listens to alerts Based on the protocol specification, a node can send
from only those nodes that are in its listening range an alert message when the sensed data crosses the
(same function used for nodes). The variable i given threshold interval. This threshold interval is set by
as input to the function is the result of a select the sink depending on the particular process being
statement i : nodeid t, which allows the node to controlled. We imitate this event using a probability
listen to any node that is transmitting. The guard weight-based selection for sending alert messages
makes sure that the sink can listen to that particular as reflected in the edge towards SendAlert (shown
node. At the completion of the alert slot, the sink with dashed lines). The edge with probability weight
checks if any collision has occurred via the function 90 represents no alert to be sent. The one with
CHECK C OLLISION (), and gives back the control to probability weight 10 represents the choice to send
the StateController. an alert. The guards on the edge make sure it is
the alert slot of the node, and that the node does
3.3. Sensor/Actuator Node Model
not already have an alert to be sent. When the node
The sensor/actuator node model is shown in Fig. chooses to send an alert, a delay is chosen within the
6. The node model is similar to the sink model interval [0, 8] via the select statement i : int[0, 8]. The
except for the notification handling procedure. Also, chosen value is assigned to the alertDelay variable.
the node template consists of an extra location for The node then waits in the location SendAlert
sending alert messages. The notification part of the for the duration of the delay and performs carrier
node model is simpler, since nodes only receive sense prior to sending the alert message. This is
notifications. Location Notification is reached when represented by the edge with the guard function
Figure 7: Message sequence chart for carrier sense during Alert
Listing 1: Carrier Sense trace
(Sleep , receiveAlert , ReceiveAlert , ReceiveAlert , Sleep , StateController , StateController , Sleep)
choice : Node(5)[][3]−> // Delay of 3 ms chosen by node 5
(Sleep , ReceiveAlert , ReceiveAlert , ReceiveAlert , Sleep ,SendAlert, StateController , Sleep)
choice : Node(6)[][3]−> // Delay of 3 ms chosen by node 6
(Sleep , ReceiveAlert , ReceiveAlert , ReceiveAlert , Sleep ,SendAlert,SendAlert, Sleep)
ALERT[5]: Node(5)−> Node(1)[5]Node(2)[5]Node(6)[5] // Alert send by node 5 is heard by node 2 and node 6
(Sleep , ReceiveAlert , ReceiveAlert , ReceiveAlert , Sleep , StateController , StateController , Sleep)
CAN L ISTEN ( I ), where the node synchronizes to the delay chosen by each node in the given round.
broadcast channel ALERT[i] sent by other nodes This is used to check if a collision has occurred. In
in the vicinity (listening range) to skip sending a certain cases when the alert messages fail to reach
message. the sink due to collision, the savedAlert variable
is used to save the alert, that is sent again in
We use a representative carrier sense mechanism
the next round. During this, the probability edge is
in the model. Nodes skip sending an alert when
not used. Instead, the nodes directly move to the
another node within their listening range is sending
location SendAlert via the edge (solid line) with
with the same delay. In reality, carrier sense would
the guard (alertReceived||savedAlert). The variable
involve listening to the channel for a small duration
alertReceived represents the case when nodes
before sending the packets. Also, in a case where
have to forward an alert received from other nodes
two nodes start carrier sense at the same instant,
towards the sink. The nodes then choose a new
their packets would collide since they would start
delay value from the interval [0, 8] for sending the
sending at the same instant after the carrier sense
alert message again.
delay. In the carrier sense mechanism presented
here, we represent a case in which two nodes can 3.4. Collision
hear each other and have the same delay by one
We use a simple collision model similar to the
of the two nodes skipping the sending the alert
one used in (Tschirner et al. (2008)) and (Fehnker
message. When the nodes do not hear each other
et al. (2007)). In the LMAC (Fehnker et al. (2007))
and the receiver can hear both, the packets collide
protocol, when two nodes send a packet in the same
at the receiver. An example message sequence of
slot it is considered as a collision. In the DMAMAC
carrier sense is shown in Fig. 7. In this example,
protocol model, collision is counted when a node
Node(5) and Node(6) are trying to send alert with
receives at least two alert messages with the same
the same delay (3ms) as shown in List. 1. In the
delay in the same alert slot. In our model, we assume
listing, we have added comments with prefix “//” to
that apart from its child nodes, the parents can
add more detail. When Node(5) begins to send the
also listen to nodes in the vicinity (similar to real
alert, Node(6) senses the sending and skips sending
networks). We define statically which other nodes a
alert via the edge guarded by CAN L ISTEN ( I ) function.
given node can listen to. Based on the representative
In a case where the channel is free, the nodes send carrier sense model, the collision occurs at a node
an alert at the time instant after the chosen delay. only when it receives two alert messages from nodes
The sending is represented using the send part (of the same rank) that cannot listen to each other,
of the broadcast channel variable ALERT[id]!. The and had chosen the same delay within the alert
local variable currentSlot is updated, along with the slot. A message sequence chart showing a collision
variable sentAlert, and function UPDATE R ECORD (). occurrence at the sink is shown in Fig. 8.
The variable sentAlert is used by the node to
The trace corresponding to the Message Sequence
remember that it has sent an alert. In a case where
Chart in Fig. 8 is shown in List. 2. In the considered
no superframe change occurs after an alert was
scenario, Node(1) and Node(3) choose the same
sent, a node updates its local variable savedAlert.
delay of 7 (ms) independently. Since they cannot
The UPDATE R ECORD () function updates a global
listen to each other their alert packets end up
array variable alertTimeRecord[] which stores the
Figure 8: Message sequence chart for collision at the sink
Listing 2: Collision Trace
( ReceiveAlert , StateController , Notification , StateController , Sleep , Sleep , Sleep , Sleep)
choice : Node(1)[][7]−> // Delay of 7 ms chosen by node 1
( ReceiveAlert ,SendAlert, Notification , StateController , Sleep , Sleep , Sleep , Sleep)
choice : Node(3)[][7]−> // Delay of 7 ms chosen by node 3
( ReceiveAlert ,SendAlert, Notification ,SendAlert,Sleep , Sleep , Sleep , Sleep)
ALERT[1]: Node(1)−> Sink[1] // Alert sent by node 1 to the sink
( ReceiveAlert , StateController , Notification ,SendAlert,Sleep , Sleep , Sleep , Sleep)
ALERT[3]: Node(3)−> Sink[3] // Alert sent by node 3 to the sink
( ReceiveAlert , StateController , Notification , StateController , Sleep , Sleep , Sleep , Sleep)
colliding at the sink. This prevents a change of vicinity. A real node has a listening range based on
the superframe (mode of operation). Node(1) and its receiver sensitivity, and distance with other nodes
Node(3) detect this and save the alert. The saved in the vicinity that varies with topology. Given that our
alert is used to resend the alert in the next round main aim is to check the working of the protocol, we
(with a new delay) to make sure the superframe define the listening range in the topology manually
changes. Note that there could be a situation where instead of calculating it dynamically based on
collision occurs at lower levels (and even at the sink), multiple factors like node position, path-loss, and
but still the change of superframe occurs because receiver sensitivity as is typically done in network
of another alert message reaching the sink. For our simulators for quantitative analysis.
model, we have created the topology in such a way
In the topology used for the evaluation of the
that both cases exist in different configurations as
DMAMAC protocol the functionalities that need to be
discussed in Sect. 5. In reality, the receiver nodes do
verified are covered. The DMAMAC protocol is used
not detect collision: in certain cases nodes receive
for applications with offline scheduling. This means
parts of packets that collide (difficult to decode them)
that scheduling is done prior to deployment and all
and in other cases they receive nothing at all. In
slot allocations are known prior to deployment. The
that respect, we rely on a representative model of
topology in general is well-planned, and no random
collision detection designed to be consistent with the
deployment is used. A real topology would be much
effects of collision on the change of superframe.
larger than the one considered here. In the current
3.5. Network Topology topology, we have 3 levels and a maximum of 2
hops. For a qualitative analysis this covers the error
The node topology used for the verification of the
scenarios that could potentially exist with multiple-
models is shown in Fig. 9. We use 5 sensor
hops.
nodes, 2 sensor-actuator nodes, and a sink in
the tree topology considered. We consider a small The schedule for the considered node topology
topology to keep the state-space small which is is shown in Fig. 10. The schedule shows both
needed in order to conduct exhaustive verification. sender/receiver identification (node/sink). The send-
The current node topology has 3 ranks but since ing part is marked by TX and receiving part is
the sink only listens (and does not send alerts), marked by RX. For notification messages, only the
we have 2 alert slots in the DMAMAC protocol. sender identification (sink) is marked. The schedule
This representative topology allows for both carrier only represents the steady superframe. In the tran-
sense and collision, has both sensors and actuators sient superframe only the first Nt part is used with
with data communication for both types of nodes, the alert parts replaced by sleep. Note that we use
and also has multiple hops. A topology based 10 milliseconds (“ms”) as slot duration similar to slot
assumption for listening range is that a higher level sizes used in general practise.
(lower rank) node is listening to all of its children
nodes, and also sometimes to other nodes in the
Figure 9: Node topology
the interval only means that in transient mode there
is a 50% probability to switch to steady mode, and
thus does not affect the qualitative results.
4. MODEL VALIDATION
We first validate the constructed Uppaal model of
the DMAMAC protocol by checking some basic
behavioural properties related to the operation of the
Figure 10: Superframe structure based on the schedule model. The purpose is to obtain a high degree of
and node topology confidence in the constructed model prior to verifying
key properties of the protocol in the next section.
During construction of the DMAMAC protocol, we
3.6. Configurations validated the operation of the model via MSCs
obtained from step-by-step execution of the model
Multiple configurations of the DMAMAC protocol
in the Uppaal simulator. These properties were
can be analysed based on values that can be
related to data transmission between nodes, data
varied in the model. Firstly, the Uppaal model can
transmission between the nodes and the sink,
start in either steady or transient mode and this
sending/receiving of alert message, possibility of
could have an effect on some of the verification
collision, and carrier sense when sending alert
properties (as discussed in Sect. 5). Another
messages.
important factor affecting the configurations is the
range of possibilities for the variable alertDelay. Below we validate properties of the model related
In the protocol, we have used the range [0,8] to to data communication and collisions using the
reduce collision. Due to state-space issues we use verification engine of Uppaal. For this, we express
only alertDelay[1, 1] for exhaustive queries, e.g., the properties to be validated in the form of Uppaal
deadlock query. The alertDelay[1, 1] in itself covers queries. Queries in Uppaal are written in a restricted
all possibilities including possibility of state-switch, variant of Computation Tree Logic (CTL) in which
collision and CSMA, and hence all the qualitative path formulas cannot be nested. Specifically, the
aspects of the protocol. For other non-exhaustive following path formulae are supported by Uppaal:
queries, we use up to alertDelay[1, 4] configurations A (always globally), A♦ (always eventually), E♦
to further validate the verification procedure. The (reachable), and E (exists globally).
only difference between alertDelay[1, 1] and the
For validation purposes, we first check the operation
other considered configurations is the applicability
of the model with respect to data communication
of property sink mode and consistent node mode of
between neighbouring nodes and between the
the verification properties and is further discussed
sink and its neighbouring nodes. We check that
in Sect. 5. Also, the select statement interval [1, 10]
if two nodes i and j are such that the parent
used to decide the switch from transient to steady
node of node j is i, then these will eventually
mode by the sink is reduced to [1, 2] to keep the
communicate. Furthermore, it should be such that
state-space low for all the queries. The reduction of
any child node of the sink node should eventually consider properties specific for the transient mode
communicate with the sink. Formally, these two case followed by properties specific for the steady
properties can be expressed as the set of queries mode case. Finally, we verify two real-time properties
below. Here, nodeid t is the type used to represent of the protocol related to upper bounds on mode
node identifiers in the model, parent[i] is used to switch delay and data transmission delay.
obtain the parent node of node i, and sinkId denotes
5.1. Common Properties
the identity of the sink. The property is expressed by
reference to the location Sent and location Received Given the dual-mode operation of the DMAMAC
which are reached by the communicating nodes protocol, the important properties relate to the
upon synchronization over the channel DATA. nodes operating in different modes, and switching
between them. Firstly, we check the operating mode
Node data communication
properties. We make sure that the sink is exclusively
∀ i,j ∈ nodeid t such that parent[j]==i:
either in the steady mode or in the transient mode
A♦ (Node(i).Sent && Node(j).Received)
at all times. Following this, we check that all nodes
Sink data communication follow the operating mode of the sink consistently.
∀ i ∈ nodeid t such that parent[i]==sinkId: Formally, these properties are expressed as follows:
A♦ (Node(i).Sent && Sink.Received)
Sink mode
It should be noted that we do not check the A (Sink.steady && !Sink.transient) ||
property that two neighbouring nodes always have (!Sink.Steady && Sink.transient)
the possibility to communicate. This is due to the fact
Consistent node mode
that Uppaal does not support nesting of CTL path
∀ i ∈ nodeid t:
formulae.
A (Node(i).transient == Sink.transient ||
The second property that we validate is related Node(i).steady == Sink.steady)
to collisions which play an important role in the
Next, we investigate properties of the protocol
DMAMAC protocol in relation to the sending of
related to collision and its effect on the change
alert messages. In this case, we check that it is
of operational modes. The queries refer to the
possible to have collision happening on all nodes
changeSuperframe variable which indicates whether
and on the sink. Collision cannot be guaranteed to
the network should change mode in the next
happen and hence we verify only the possibility of
superframe. Collisions may have different effects
collision occurring. Formally, these two properties
depending on the configuration under consideration.
are expressed as the following set of queries:
For configurations with alertDelay[1, 1] where all
Node collisions ∀ i ∈ nodeid t : E♦ Node(i).collision the nodes will pick the same delay, collision
at the sink should not result in a change of
Sink collisions E♦ Sink.collision
superframe or operational modes. For configuration
Finally, we also validate that there are no deadlocks with alertDelay[1, 2], we may have both collision
in the model. In Uppaal, this can be expressed via and change of superframe since, e.g., two nodes
the query below where deadlock is a built-in state may pick a delay of 1 (which will result in a
property in Uppaal. collision) while a single third node picks a delay
of 2. The latter choice will result in the sink being
No deadlock A !deadlock
notified of a required change of mode. Formally,
properties related to collisions and change of mode
The above queries related to data communication, are specified as follows:
collision, and deadlocks were all verified on both the
Collision and mode switch
transient and the steady variant of the model. This in
E♦(Sink.collision && Sink.changeSuperframe)
turn increased confidence in the proper operation of
the model. Collision and no mode switch
E♦(Sink.collision && !Sink.changeSuperframe)
5. PROTOCOL VERIFICATION Following the discussion above, we expect that the
We now consider verification of the key functional first property is false in configurations where all
properties of the DMAMAC protocol. As explained nodes must choose the same delay while it is true
earlier, the constructed model comes in two variants: in configurations where different alert delays can
one variant with the protocol starting in the transient be chosen. This implies that the protocol design
mode and one variant with the protocol starting in the ensures that the DMAMAC protocol can change
steady mode. We first consider common properties mode even in the presence of collisions. The second
that are independent of whether the protocol starts property is expected to be true as we may (in all
in the transient or in the steady mode. Then we configurations) have the situation that the choice
Listing 3: Collision and change of superframe together
( ReceiveAlert , StateController , StateController , StateController , Sleep , Sleep , Sleep , Sleep)
choice : Node(1)[][1]−> // Node 1 chose delay of 1 ms
( ReceiveAlert ,SendAlert, StateController , StateController , Sleep , Sleep , Sleep , Sleep)
choice : Node(3)[][1]−> // Node 3 chose delay of 1 ms
( ReceiveAlert ,SendAlert, StateController ,SendAlert,Sleep , Sleep , Sleep , Sleep)
choice : Node(2)[][2]−> // Node 2 chose delay of 2 ms
( ReceiveAlert ,SendAlert,SendAlert,SendAlert,Sleep , Sleep , Sleep , Sleep)
ALERT[3]: Node(3)−>Sink[3] // Node 3 sends alert
( ReceiveAlert ,SendAlert,SendAlert, StateController , Sleep , Sleep , Sleep , Sleep)
ALERT[1]: Node(1)−>Sink[1] // Node 1 sends alert
( ReceiveAlert , StateController ,SendAlert, StateController , Sleep , Sleep , Sleep , Sleep)
ALERT[2]: Node(2)−>Sink[2] // Lastly, Node 2 sends alert with a delay of 2 ms (higher than others two)
( ReceiveAlert , StateController , StateController , StateController , Sleep , Sleep , Sleep , Sleep)
of delay (alert) causes collisions such that the sink given query below checks if there is a path where the
may not be notified of the required change of mode system invariantly is in the transient mode.
in the current superframe. Of course, the sink may
Remain transient E transient
be notified via retransmission of the alert in a later
superframe, eventually causing a mode switch (see The second property represents the reachability of
below). steady mode from the starting state, i.e., that it
is possible for the system to change mode from
An example trace demonstrating co-existence of
transient to steady.
collisions and change of superframe is shown in List.
3. In this example, the nodes 1 and 3 choose the Steady switch E♦ steady
same delay (1 ms) and cannot listen to each other.
5.3. Steady model variant
The transmissions therefore collide at the sink. But
node 2 which has chosen a different delay (2 ms) For the variant of the model that starts in the steady
successfully alerts the sink thus inducing change mode, we verify the dual properties of the variant that
of superframe. This delay choice is done when the starts in the transient mode. These two properties
model changes location from StateController to are listed below:
SendAlert.
Remain steady E steady
Finally, we verify a property related to the critical
Transient switch E♦ transient
change of state in the protocol from steady to
transient. When the data requirement is higher, The two properties check that it is possible to remain
the protocol should be able to detect and switch in steady mode and that it is possible to switch to
accordingly. Also, when a switch fails due to transient mode.
collisions, there should be a possibility to re-use the
5.4. Real-time properties
failed alert to induce change of operational modes.
The failed alert is used as a saved alert in the next We now consider real-time properties related to
alert round. We use the query which searches for mode switch delay and data communication delay.
one example where this occurs. In order to verify these properties, we use a modified
version of the Uppaal model where we have included
Critical change of state
the use of two watch templates (Watch1 and Watch2)
∃ i ∈ nodeid t:
in order to record elapsed time.
E♦ Node(i).savedAlert && Sink.steady &&
Sink.changeSuperframe The first real-time property that we consider is the
switch delay, i.e., the time difference between a
It should be noted that given the nature of the model,
detection of threshold breach and the mode switch
the collisions could occur forever preventing the
happening. This switch is required to happen within
change of superframe. This means that we cannot
the duration of a superframe (transient superframe
show that a state switch will eventually happen.
length). This property is specified as follow:
5.2. Transient model variant
Switch delay
We now consider properties specific for the variant A Watch1.switchDelay ≤ superframeLength
of the model where the sink and nodes starts
We verified the switch delay property by considering
in transient mode. In the model, transient and
a single node farthest from the sink. By symmetry,
steady are boolean variables. In the case where
the property applies to other nodes at the same level,
the controller process stays in the transient state
and also to the parent nodes which (by the tree
permanently, the protocol needs to stay in transient
topology) will have a smaller maximum switch delay.
mode of operation to suit the application needs. The
The second real-time property concerns the data We have validated the basic operation of the
communication delay. It is the time elapsed between constructed model using message sequence charts
the first data sent in the superframe until the last highlighting the most important features, and
data received. This is required to be within the same operations of the protocol including data transfer,
superframe. The property is expressed as follows: alert message functioning, carrier sense, and
possibility of collision. Further, we validated the
Data delay
proper operation of the model using the verification
A Watch2.dataDelay ≤ superframeLength
engine of Uppaal. The validated model was
All properties listed above evaluate to the expected then verified for the switch procedure and safety
results. Details on the execution time for the properties, including absence of deadlock and other
queries based on different configurations of the faulty states. The key real-time properties in the
model are shown in table 1. The verification was form of upper bounds on switch delay and data
conducted on a PC with 4 GB RAM, 2.30 GHz delay were also verified. Two variants of the model
2-core processor. The query Collision and mode were used for verification and validation, one starting
switch could be verified only on the configuration with the transient mode of operation and the other
with alertDelay[1, 1] and resulted in memory starting with steady mode. Different configurations
exhaust in other configurations. Other queries were of the model with varying alert delay were used as
verified also on configuration alertDelay[1, 2], and a basis for the verification. For the verification, we
alertDelay[1, 4] with i : int[1, 2]. used a representative node topology that covers all
important features of the protocol including existence
6. CONCLUSION AND PERSPECTIVES of sensors and actuators, multi-hop, alert messages,
and possibility of collision. The DMAMAC protocol
In this article, we have detailed the modelling and model in Uppaal satisfied the properties considered
verification process of the DMAMAC protocol. The which increases confidence on the design of the
DMAMAC protocol is designed for process control protocol. As a proposed future work, a stochastic
applications and we have used the Uppaal model- model of the DMAMAC protocol to verify the
checking tool for modelling and verification. The quantitative properties including collision probability,
model consists of a network of timed automata with expected switch delay, and energy consumption
multiple nodes and a sink operating according to the could provide further insights to the working of the
DMAMAC protocol. protocol.
We have explained the model in Uppaal including Currently, we are also in the process of developing a
its modelling elements and templates in detail. The prototype implementation of the DMAMAC protocol
constructed timed automata model includes generic on real hardware. The Uppaal model constructed
MAC slot operations including data sending and in this paper serve as an important specification
receiving, notification, and sleep. This means that in terms of ensuring the proper and correct
the model can be extended to represent other MAC implementation of the protocol logic and frame
protocols with similar (and extra) slotting within processing.
their superframe. To illustrate the generality of the
constructed model, the finite state machine for the
REFERENCES
protocol model and the possible extensions are
shown in Fig. 11. The diagram is divided into Akyildiz, I. F. and Kasimoglu, I. H. (2004),
three parts: the generic part, DMAMAC extensions, ‘Wireless Sensor and Actor Networks: Research
and other possible extensions. The generic part challenges’, Ad Hoc Networks 2(4), 351–367.
consists of notification and data transfer, which is
generally part of a wide range of MAC protocols Behrmann, G., David, A. and Larsen, K. (2004), A
for WSANs. The DMAMAC extensions with alert tutorial on Uppaal, in M. Bernardo and F. Corradini,
sending and receiving parts are specifically relevant eds, ‘Formal Methods for the Design of Real-Time
for DMAMAC. Given the generic structure, the model Systems’, Vol. 3185 of Lecture Notes in Computer
can be extended to include other MAC protocol Science, Springer Berlin Heidelberg, pp. 200–236.
slot types or state types including Channel Sense, David, A., Larsen, K. G., Legay, A., Mikucionis, M.,
Backoff and Link establishment. S-MAC (Ye et al. Poulsen, D. B., Vliet, J. and Wang, Z. (2011),
(2002)) is a one such MAC protocol that uses Statistical Model Checking for networks of Priced
Request To Send (RTS), Clear To Send (CTS), Timed Automata, in ‘Proceedings of the 9th
and carrier sense. The current model can be easily International Conference on Formal Modeling and
extended to model S-MAC with re-use of generic Analysis of Timed Systems (FORMATS)’, Vol.
parts. 6919 of LNCS, Springer Berlin Heidelberg, pp. 80–
96.
Figure 11: Generic model with possible extensions
Fehnker, A., van Glabbeek, R., Hfner, P., McIver, Varga, A. and Hornig, R. (2008), An overview
A., Portmann, M. and Tan, W. (2012), Automated of the OMNeT++ simulation environment, in
analysis of AODV using Uppaal, in ‘Tools and ‘SIMUTOOLS’, pp. 60:1–60:10.
Algorithms for the Construction and Analysis of
Systems’, Vol. 7214 of Lecture Notes in Computer Ye, W., Heidemann, J. and Estrin, D. (2002), An
Science, Springer Berlin Heidelberg, pp. 173–187. energy-efficient mac protocol for wireless sensor
networks, in ‘INFOCOM 2002. Twenty-First Annual
Fehnker, A., van Hoesel, L. and Mader, A. (2007), Joint Conference of the IEEE Computer and
Modelling and Verification of the LMAC protocol Communications Societies. Proceedings. IEEE’,
for Wireless Ssensor Networks, in J. Davies and Vol. 3, pp. 1567–1576 vol.3.
J. Gibbons, eds, ‘Integrated Formal Methods’,
Vol. 4591 of Lecture Notes in Computer Science,
Springer Berlin Heidelberg, pp. 253–272.
Hespanha, J. P., Naghshtabrizi, P. and Xu, Y. (2007),
A survey of recent results in Networked Control
Systems, Vol. 95, pp. 138–162.
Kumar S., A. A., Øvsthus, K. and M. Kristensen, L.
(2014), Towards a Dual-Mode Adaptive Mac Pro-
tocol (DMA-MAC) for feedback-based Networked
Control Systems, in ‘The 2nd International Work-
shop on Communications and Sensor Networks’.
Suriyachai, P., Brown, J. and Roedig, U. (2010),
Time-critical data delivery in Wireless Sensor
Networks, in ‘Proceedings of DCOSS’, pp. 216–
229.
Tschirner, S., Xuedong, L. and Yi, W. (2008), Model-
based Validation of QoS properties of Biomedical
Sensor Networks, in ‘Proceedings of the 8th ACM
International Conference on Embedded Software’,
EMSOFT ’08, ACM, New York, NY, USA, pp. 69–
78.
Property / Query Result CPU Time (s ) Resident Mem. (KB) Virtual Mem. (KB)
Configuration : alertDelay[1,1], i:[1,2]
Common queries
Sink mode Not Satisfied 718.837 1,795,596 3,595,148
Consistent node mode Satisfied 876.586 1,772,436 3,573,820
Collision and mode switch Not Satisfied 711.287 1,797,488 3,599,136
Collision and no mode switch Satisfied 3.214 21,044 49,512
Critical change of state Satisfied 33.868 113,084 238,116
Transient specific queries
Remain transient Satisfied 0.015 13,820 56,924
Steady switch Satisfied 0.64 13,888 40,168
Steady specific queries
Remain steady Satisfied 0.032 17,424 58,892
Transient switch Satisfied 1.965 19,308 48,796
Real-time queries
Switch delay Satisfied 273.048 440,676 891,152
Data delay Satisfied 231.302 450,664 905,284
Configuration: alertDelay[1,2], i:[1,2]
Common queries
Sink mode N/A N/A Memory exhausted Memory exhausted
Consistent node mode N/A N/A Memory exhausted Memory exhausted
Collision and mode switch Satisfied 8.331 62,292 128,008
Collision and no mode switch Satisfied 8.346 61,616 129,064
Critical change of state N/A N/A Memory exhausted Memory exhausted
Transient specific queries
Remain transient Satisfied 0.02 13,836 40,092
Steady switch Satisfied 0.562 13,848 57,012
Steady specific queries
Remain steady Satisfied 0.046 36,596 82,700
Transient switch Satisfied 16.708 66,116 137,096
Real-time queries
Switch delay Satisfied 1200.225 1,799,596 3,601,164
Data delay Satisfied 1068.014 1,799,624 3,622,604
Table 1: Performance of the protocol verification using Uppaal