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