=Paper= {{Paper |id=Vol-1689/paper3 |storemode=property |title=Statistical Model Checking of CSMA/CA in WSNs |pdfUrl=https://ceur-ws.org/Vol-1689/paper3.pdf |volume=Vol-1689 |authors=Zohra Hmidi,Laid Kahloul,Saber Benharzallah,Cherifa Othmane |dblpUrl=https://dblp.org/rec/conf/vecos/HmidiKSO16 }} ==Statistical Model Checking of CSMA/CA in WSNs== https://ceur-ws.org/Vol-1689/paper3.pdf

STATISTICAL MODEL CHECKING of
CSMA/CA in WSNs

Zohra Hmidi1 , Laid Kahloul2 , Saber Benhazrallah3 , and Cherifa Othmane4

LINFI Laboratory, Computer Science Departement, Biskra University, Algeria
1
zohra hmidi@yahoo.fr, 2 kahloul2006@yahoo.fr, 3 sbharz@yahoo.fr,
4
major2010 ca@hotmail.com

Abstract. CSMA/CA (carrier sense multiple access with collision avoid-
ance) reminds the basic method used in MAC level protocol in WSNs
(wireless sensors network). Several extensions were proposed to enhance
this method and to deal with specific problems in WSNs as energy con-
sumption. The complexity of this method and its criticality motivate the
formal specification and verification of its basic algorithms. In the cur-
rent work, we opt for a stochastic formal model which provides more real-
ism because it provides probabilistic aspect that often dominates several
random events: collisions on the transmission medium, frame loss, loss
of acknowledgements, possible disconnections, and loss of nodes. Hence,
it is not enough to analyse qualitative properties where the answer will
be yes or no, it is more appropriate to investigate whether certain prop-
erties are safe under particular constraints and with what probability; so
that one seeks to evaluate the system and its probabilistic performance.
Indeed, we model the protocol using probabilistic timed automata, a
formalism in which both non-deterministic and probabilistic choice can
be represented. Then a qualitative and quantitative verification of this
protocol is made using the statistical model checking in the UPPAAL
tool.

Keywords: WSNs, CSMA/CA, Statistical Model Checking, Probabilistic Au-
tomata, UPPAAL

1 Introduction
A Wireless Sensor Network (WSN) is a distributed system of cooperating de-
vices that perform distributed monitoring applications in a physical environment
over a self-organised wireless network topology (Intana et al. 2014)(Hai 2015).
Unlike traditional networks, a WSN has its own design and resource constraints.
Resource constraints include a limited amount of energy, short communication
range, low bandwidth, and limited processing and storage in each node. Design
constraints are application dependent, so that the WSN design is inherent to
the monitored environment (Yick et al. 2008). Maximizing the network lifetime
is a common objective of sensor network researchers. The MAC protocols have
gained a lot of importance in the last few years because of their influence on
the lifetime of sensor nodes of WSN. Major source of energy waste in WSN is
basically the collision. When a transmitted packet is corrupted due to interfer-
ence, it has to be discarded and the follow on retransmissions increase energy
consumption. Although collisions cannot always be prevented, randomized ex-
ponential backoff rules are used in the retransmission scheme of CSMA/CA to
minimize the likelihood of repeated collisions (Patil et al. 2013).
In this paper, we illustrate a modelling approach tailored to the automatic
verification of CSMA/CA protocol for wireless sensor networks. Specifically, we
use probabilistic timed automata to model the protocol; we then describe how
model analysis can be performed through SMC (statistical model checking) im-
plemented in the UPPAAL tool version 1.4.19 (Uppaal 2016).
The remainder of this paper is organised as follows: In the next section, we
report related work, in Section 3, we introduce the syntax and the semantics of
probabilistic timed automata. Section 4 explains the modelling formalism used in
UPPAAL SMC and the model checking queries. In section 5, we give an informal
description of the CSMA-CA contention resolution protocol. Section 6 presents
the modelling approach, the probabilistic timed automata of the protocol and
the probabilistic model checking results. Finally, section 7 concludes this paper.

2 Related Works

To improve the reliability of WSNs protocols, proposed approaches include: sim-
ulation, testing and formal verification. Even if simulation and testing can be
used to check large scale networks and discover errors; they can never guaran-
tee the detection of all the bugs in a system. In (Elleuch et al. 2011), several
works which are based on simulation are discussed. Formal modelling and verifi-
cation are used to model the behaviour of a system and to prove its correctness.
There have been several attempts to verify communication protocols for wireless
networks.
For modelling and verification the MAC level protocols, the work presented in
(Ho et al. 1996) is one of the first works that studied the IEEE 802.11 CSMA/CA
protocol (IEEE 802.11,1995). The authors of (Ho et al. 1996) used the basic
scheme of the protocol where the IFS (Inter-frame space) are introduced: ”IFS,
Random backoff, Data, IFS, ACK”. In this work, the authors used Markov chains
to compute the ”throughput” and the ”average delay”. They made also a perfor-
mance analysis of the protocol where hidden terminals are considered. Hidden
terminals problem occurs when some nodes could not sense a neighbour node
even if it is in its scope. They define a specific probability that a station does
not hear another station. The paper showed the improvement in the throughput
and the reduction of the delay when the CA (collision avoidance) is exploited in
the protocol.
In (Kwiatkowska et al. 2002), the authors presented a formal study of a ”two-
way handshake” sub-protocol of the IEEE 802.11 standard. The authors studied
a case where the net is composed of two sending stations and two destination
stations. They made three hypothesis: (i) there is not an EIFS (Extended Inter-
frame Space) parameter, (ii) there is no timing synchronisation function where
a specific station sends periodically short frames to synchronise the clocks of
all the stations, (iii) and finally, the retry limits is supposed to be infinite. In
their paper (Kwiatkowska et al. 2002), UPPAAL is used to make qualitative
verification of some properties, then the PRISM tool is exploited to make a
performance evaluation of the protocol. The PRISM tool can be used to give
answer to several questions as: ”what is the probability that a station sends
correctly a packet within certain deadline”. In another study on performance
analysis of IEEE 802.11 CSMA/CA protocol in Wireless LANs, (Zhai et al.
2004), the authors studied two metrics: the ”throughput” and the ”delay” at
various traffic loads. Basically, each station is seen as a queuing system with a
packets-arrival process and a service time distribution (here, the service time is
the MAC layer service time, which can be computed as the difference between
the time a packet starts to contend for transmission and the time that the
packet either is acknowledged for correct reception by the intended receiver or
is dropped. Hence, dropping of packet is possible here). In order to study this
queuing system, they model the ”exponential backoff process” as a Markov Chain
(more exactly a semi-Markov chain, where the service time is considered as the
sojourn time in each state). Through this modelling, the authors computed a
probability distribution for the time service. As a conclusion, they demonstrated
that the exponential distribution is a good model for the MAC layer service
time. In (Zhang et al. 2013), the authors used stochastic timed automaton in
the study of WSNs protocols. As a case study, they considered the Timing-sync
Protocol for Sensor Networks (TPSNs) (Ganeriwal et al. 2003).
The authors, of (Ganeriwal et al. 2003), used timed automata to describe
the protocol in an ideal context where no messages can be lost and no node
will be in fail. Based on this specification, the authors used UPPAAL to verify
some qualitative properties of the TPSNs protocol. Then, the authors enrich
this specification by introducing stochastic transitions, either to model losing of
messages or to model damaged nodes. In (Ajith et al. 2014), the authors applied
Model Driven Software Engineering (MDSE) to develop protocols dedicated to
Wireless Sensors Actuators Networks. The use of MDSE aims to produce, in
a short time, reliable protocols code. The authors used CPN (Coloured Petri
Nets) and CPN-tool (Jensen et al. 2007) to realise a first model of the protocol
then they exploit an extension of the PetriCode (Simonsen et al. 2013) tool
to generate the code. This last approach can be used to produce the code for
WSN platforms (TinyOS (Levis et al. 2005)) or to produce scripts for simulators
(TOSSIM (Lewis et al. 2003), MiXiM (Köpke et al. 2008)).
In (Ballarini et al. 2006) a comparative analysis of the IEEE 802.11 protocol
for wireless ad-hoc network and the S-MAC protocol is developed. In this work,
DTMC (Discrete Time Markov Chain) models referring to a specific three-hop
topology are developed with PRISM (Prism 2016). The authors have used the
PCTL (Probabilistic Computation Tree Logic) logic to express relevant proper-
ties: probabilistic reachability, time-bounded probabilistic reachability and ex-
pected reachability properties are verified. In (Marta et al. 2002), the authors
studied the DCF (Distributed Coordination Function) protocol, in a fixed net-
work topology consisting of two sending stations and two destination stations,
using probabilistic timed automata. The probabilistic choice, in this work, is
presented in the randomized backoff procedure. The authors in (Marta et al.
2002) used PRISM to automatically verify the probability of a station delivering
a packet before a deadline.
Finally, (Hammal et al. 2014) proposed a new variant of the CSMA/CA with
DCF mode. In this variant, each station has to disconnect whenever its signal-to-
noise ratio is lower than a specific threshold. Such disconnections are intended
to reduce the number of collisions and to improve the transmission rate. The
authors in (Hammal et al. 2014) used the timed automata in UPPAAL and they
analysed some safety and liveness properties, such as the absence of a deadlock
and the successful termination of a transmission. However, the model checking
shows a peculiar case where the protocol could not guarantee the successful
transmission of packets. Furthermore, no upper bound exists for the required
delay to successfully transmit a packet, and no performance evaluation was done.
In our work, we are interested to the qualitative/quantitative verification of
IEEE 802.11 MAC protocol in particular, the variant proposed in (Hammal et
al. 2014). We consider stochastic events that can occur during the execution
of the protocol. These stochastic events concern failures to access the medium,
collisions, messages lose, the choice made by a station to send or to receive,
etc. In order to handle these stochastic aspects, Probabilistic Timed Automata
are used as a modelling formalism and UPPAAL is exploited to check and to
evaluate the protocol.

3 Probabilistic timed automata
Probabilistic timed automata (Kwiatkowska et al. 2001) are a modelling for-
malism for distributed systems that support dense time, non-determinism, and
probabilistic choice. They represent an extension of timed automata, for which
discrete probability distributions range over the edges of the control graph.

3.1 Clocks and Zones
Let X be a finite set of variables called clocks, ranging over the time domain T
∈ { R,N} of either non-negative real or natural numbers. A function v : X → T
is referred to as a clock valuation. For any v and t ∈ T , the clock valuation v ⊕ t
denotes the time increment for v with t. Let Zones(X ) be the set of zones over
X , which are conjunctions of atomic constraints of the form x ∼ c for x ∈ X ,
∼ ∈ { ≤,=,≥ } , and c ∈ N. The clock valuation v satisfies the zone ζ , written
v C ζ, if and only if ζ resolves to true after substituting each clock x ∈ X with
the corresponding clock value from v.

3.2 Syntax of probabilistic timed automata
A probabilistic timed automaton is a tuple (L,¯l,X ,Σ,inv,prob) where:
– L is a finite set of locations;
– ¯l ∈ L is the initial location;
– X is a finite set of clocks;
– Σ is a finite set of events, such that Σu ⊆ Σ are urgent;
– inv: L → Zones(X ) is the invariant function associated for each location;
– prob ⊆ L × Zones(X ) × Σ × Dist(2X × L) is the probabilistic transition
relation.Dist(2X ×L) denotes the couple: (probability intensity over the tran-
sition, the target location).

3.3 Semantics of probabilistic timed automata
A state of a probabilistic timed automaton is a pair (l, v) where l ∈ L and
v ∈ T|X | are such that v C inv(l) (i.e. v satisfies inv(l)). The model starts
in the initial location ¯l with all clocks set to 0, and hence the initial state is
(¯l,0). In each location, there is a nondeterministic choice between two types
of transitions: Delay transitions which correspond to the elapsing of time in a
location. They are permitted as long as the invariant condition is satisfied and no
urgent transitions are enabled. Discrete transition correspond to the execution
of probabilistic transitions (l, g, σ, p) ∈ prob. If the current location l satisfies the
clock constraint g and the current event is σ, then p(X, l0 ) is the probability of
resetting all clocks in X(X ⊆ X )to 0 and moving to the location l0 .

4 SMC in the UPPAAL tool
Statistical Model Checking (SMC) (Koushik et al. 2004) is an innovative ap-
proach proposed as an alternative to avoid the exhaustive exploration of the
state-space of the model. SMC is a simulation-based solution, which is less time
and memory intensive than classical model checking. The idea behind SMC is to
generate enough sample execution paths for the system and then to use the statis-
tical hypothesis testing to decide whether the system satisfies the given property
or not. Using SMC, one can verify qualitative properties (as in classical model-
checking) and make quantitative evaluation too. UPPAAL SMC (David et al.
2015) is an extension of UPPAAL, proposed to represent systems via networks
of priced timed automata (David et al. 2011) whose behaviours may depend on
both stochastic and non-linear dynamical features. Each component of the sys-
tem is described with an automaton whose clocks can evolve with various rates.
Such rates can be specified with, e.g., ordinary differential equations.

4.1 Modelling
The modelling formalism of UPPAAL SMC is based on probabilistic timed au-
tomata. The stochastic interpretation replaces the non-deterministic choices be-
tween multiple enabled transitions by probabilistic choices (that may or may
not be user-defined). The non-deterministic choices of time-delays are refined by
probability distributions, which at the component level are given either uniform
distributions in cases with time-bounded delays or exponential distributions in
cases of unbounded delays.
4.2 Query Language
UPPAAL SMC supports five different analysis methods. Below we use N to
denote natural number, M to denote number of simulations, P to denote a
probability, and exp to denote an expression:
- Statistical evaluation (Hérault et al. 2004): SMC estimates the probability
of the state property being satisfied, using the following query:
P r[<= N ](” <> |[]”exp)
- Hypothesis testing (Younes 2005): SMC checks if the property is satisfied
within a certain probability, using the following query:
P r[<= N ](” <> |[]”exp)” <= | >= ”P
- Statistical comparison: SMC compares the satisfaction possibilities over two
properties, using the following query:
P r[<= N ](” <> |[]”exp)” <= | >= ”P r[<= N ](” <> |[]”exp)
- Expected value: SMC computes the maximal or the minimal value of a cer-
tain variable while checking the system, using the following query:
E[<= N ; M ](”min|max” : exp)
- Simulations: SMC simulates a system multiple times and computes trajec-
tories of specified expressions over time, using the following query:
simulate M [<= N ]{exp, exp}

5 The Contention Resolution Protocol CSMA-CA
After having presented the necessary formalisms, in the above paragraphs, the
current section aims to present informally the protocol IEEE 802.11 which will
be our case study.
The primary MAC scheme of the standard IEEE 802.11 is called Distributed
Coordination Function (DCF)(Ballarini et al. 2006). It describes a decentralised
mechanism which allows network stations to coordinate for the use of a medium
in an attempt to avoid collision. Three time periods are considered: the DCF
InterFrame Space (DIFS), the Short InterFrame Space (SIFS) and the Extended
InterFrame Space (EIFS), where SIF S < DIF S < EIF S. A station can start
a transmission of data packets only after sensing the medium free for a DIFS.
On reception of a data packet, the destination station, after sensing the channel
free for SIFS, sends an acknowledgement packet (ACK) back to the sender. A
collision is recognised by the sending station if either: on termination of the
transmission the channel is sensed occupied by another station, or if an ACK
packet is not received within a given time. In order to avoid collisions, the MAC
protocol obliges the stations to enter in backoff stage before sending if either
(Marta et al. 2002):
- the channel is not sensed idle for a DIFS;
- the channel is sensed busy after the station finishes a data transmission;
- a positive acknowledgement of successful transmission is not received from
the destination station before a timeout;
- the station receives an acknowledgement and wishes to send another packet.

As soon as a backoff condition becomes true, the deferring station selects a
BackoffTime composed of a random number backoffvalue of slot times, where
each slot has size SlotT ime. This value indicates the number of time periods
which must be passed before the station can start transmitting. If the channel
is detected idle for a some SlotT ime, the backoffvalue is decremented by 1. This
decrementing procedure is temporarily suspended if a transmission is detected
(the reduction of backoffvalue is frozen) and is resumed only after the channel
is sensed free for DIFS time units. When the backoffvalue reaches 0, the station
can start its transmission. The value of backoffvalue is a pseudo-random integer
drawn from a uniform distribution over the interval [0, CW ], where CW is
the Contention Window which has initial value CW min and takes values of
ascending powers of 2 minus 1. Thus CW = (CW min + 1) × 2bc − 1 where
bc (the BackoffCounter ) increases with the number of consecutive unsuccessful
transmissions. Note that the likelihood of a longer backoff delay for repeatedly
detected collisions (where bc is large) is increased. The value of CW has an upper
bound of CW max. Once this value has been reached, CW will remain at this
value until it is reset.

6 Modelling using UPPAAL

In this section, we present the formal model of the studied protocol. The model
is composed, basically, of three synchronised PTA (Probabilistic Timed Au-
tomata): Wireless station (WS) model, Backoff model, and Medium Model. In
the following, we present only the WS model and the Medium model.

6.1 Model of wireless station and wireless medium

When analysing the model presented in the previous work (Hammal et al. 2014),
we have found several cases where the transmission operation fails forever. These
fails do not reflect real anomalies in the studied protocol, but they are due to
the modelling process:

1. A station may have f ail as a response of the medium forever. In the model of
the station, there is no mechanism that allows it to get out of this particular
case. The station can only retry continuously sending the PDU, and the
medium continues to meet fail. This is an unrealistic case, but the model
proposed may make it a possible case in the protocol. Indeed, this way of
simulating the fail causes the random simulations made by UPPAAL enter
in infinite loops choosing each time a transition fail.
2. A station can get infinitely in a loop (Disconnected,idle Connected) without
advancing the protocol. Another unrealistic behaviour but a possible path
in the model.
3. From the idle state, there are three possible transitions, one towards the
Disconnected state, the second towards the W aitingU ntilT ransmit state,
and the third towards the af ter begin receiveP DU state, but this last one
is not possible unless there is a synchronization (with the medium). Fol-
lowing this modelling, the station can always take the transition towards
W aitingU ntilT ransmit and never take the third one; this leads to a dead-
lock problem that will be explained in the next fourth point.
4. When the station st wants to send a PDU to the station st0 , along st0
wants to send a PDU. Both stations are leaving their states Idle to the
state W aitingU ntilT ransmit. The two stations can not return to their Idle
states before the end of their transmissions. However, terminating the trans-
mission of the st PDU requires receiving an ACK from st0 . The latter can
never send this ACK, because it can never return to its Idle state, for several
reasons (including those described in 1 and 2 as examples).

The resolution of these deficiencies can be made in several ways. Indeed,
solving the problems mentioned in 1, 2 and 3 can be achieved by making the
model more realistic by introducing stochastic factors to reduce unrealistic non-
determinism in the model. Disconnections, failures and collisions must happen
with probabilities (rare events under normal conditions). We can also assign
two different probabilities for a station, one for transmitting and one for re-
ceiving. This allows for a more realistic model. However, the problem cited
in the fourth point requires the updating of the model structure in order to
avoid this deadlock. Hence, the station st can return to its Idle state from the
W aitingU ntilT ransmit state after passing a time limit without having access
to the medium. Indeed, if st returns to its Idle state it will unlock other stations
waiting its ACK.
The following figures (Figures 1 and 2) show the probabilistic models af-
ter consideration of probabilities on some transitions (fail in the model of the
medium and disconnected, transmitted and received in the model of the station).
In these models, we have associated a probability of 1/10 for a fail event and a
probability of 2/10 for a disconnect event. For the transmission and reception
we will discuss the different values.

6.2 Model verification

The statistical model-checker associated with UPPAAL 4.1.19 required to make
all channels ”broadcast channels” and to define the probability laws governing
elapsing time for all locations with output transitions. In our model, we have
associated a rate = 1 for all locations without invariants on clocks. In this work,
we are interested to verify qualitative and quantitative properties using the UP-
PAAL SMC.
Fig. 1: Probabilistic model of wireless station

Fig. 2: Probabilistic model of wireless medium
Verification of qualitative properties. Qualitative properties can be classi-
fied into reachability, safety, liveness, and fairness.
- Reachability Properties: they are the simplest form of properties. They ask
whether a given state formula, φ, possibly can be satisfied by any reachable
state. We express that ”a state satisfying φ” is reachable by the use of the
path formula, E <> φ. For example, the formula E <> ws.W aitingF orAck
determines whether the protocol makes it possible for the sender ws to send
a message, and therefore it will pass to the ”waiting acknowledgement” state.
The figure 3.a below shows that this formula is satisfied.
- Safety Properties: they are of the form: ” something bad will never hap-
pen”. For example, the formula A[]notdeadlock determines that the model
is deadlock-free. The figure 3.b shows that this formula is not satisfied (it
was discussed in Section 6.1 ).
- Liveness Properties: These properties are of the form:”Something will even-
tually happen”. In the model of the communication protocol, any message
that has been sent should eventually be received. In its simplest form, the
liveness is expressed using the path formula A <> φ, meaning that φ is
always eventually satisfied. For example, the station ws0 always reaches the
state where it will expect an ACK. The figure 3.c shows that the formula
A <> ws0.BRAck is not satisfied. This means that the station can pass into
collision paths and never reach this state.

(a) Reachability Properties (b) Safety Properties

Fig. 3: Verification of qualitative properties

Verification of quantitative properties. In this case, the question is to
estimate the probability that a certain property will be satisfied by the system
prior to the violation of some constraint. In other words, we are not interested
here in whether a station reaches a state or not, but to know with what rate
this station will reach this state. To check the model, we added to the model of
the station, a probability to be the sender and another to be the receiver. Here
after, we will show the results in two different cases:
- Both probabilities are equal: we assigned a probability of 4/10 for both
transitions, and we will make a set of queries as following:
• The query: P r[<= 1000](<> ws.W aitingF orAck), which allows to
know the probability that the station reaches a state where it has finished
its transmission and waits for an ACK before 1000 units of time during
the run of the protocol. Figure 4.a shows the response of UPPAAL to
this request.
• The query: P r[<= 1200](<> ws.BR Ack), which allows to know the
probability that the station reaches a state where it started receiving an
ACK before 1200 units of time during the run of the protocol. Figure
4.b shows the response of UPPAAL to this request.
• The query: P r[<= 1000](<> ws.Collision), which allows to know the
probability that the station reaches a collision state before 1000 units
of time during the run of the protocol. Figure 4.c shows the probability
interval.

(a) sending PDU

(b) receiving ACK

Fig. 4: The probability confidence interval of case1

- The two probabilities are different: in the case of two stations, we assigned
to each one two different probabilities. For example, for station ws0, we as-
signed a probability of 4/14 to be the receiver and a probability of 8/14 to
be the sender. Rather, for the station ws1, we assigned a probability of 4/8
to be the receiver and a probability of 2/8 to be the sender. We will presente
some queries to compare the results with the first case. Figures 5.a, 5.b and
5.c show the response of UPPAAL to the following requests, respectively:
P r[<= 1000](<> ws.W aitingF orAck), P r[<= 1200](<> ws.BRA ck)
and P r[<= 1000](<> ws.Collision).

(a) sending PDU

(b) receiving ACK

Fig. 5: The probability confidence interval of case2

If we make a comparison, we will notice that the rates have changed con-
siderably. The rate of sending a pdu will be 66% instead of 51%, the rate of
receiving of an ACK will be 50% instead of 36% and finally the collision rate
will be 39% instead of 40%. Finally, 75% of sent packets are received correctly,
unfortunately, the collision rate remains high.
It is also possible to plot the characteristic function of probability using the
tool UPPAAL, as shown in figure 6. Based on these charts, we see that the
probability of sending for ws0 is the largest, and the collision probability is the
smallest (of course, using the current parameters). In addition, the ws1 station
is less likely to perform the transmission first.

7 Conclusion

In this paper, we have described the use of statistical model checking to analyse
and evaluate the WSN MAC protocol. We have modelled stochastic uncertainties
which are quite common in WSN systems behaviour, like disconnections and
Fig. 6: The characteristic function of probability

failures using probabilistic timed automata. Besides of checking the correctness
of the protocol, we have used statistical model checking, in the UPPAAL tool,
to evaluate the performance of the protocol numerically as well. In a first step
of performance evaluation, we have detected that there is some anomalies in the
proposed model, inspired from the work (Hammal et al 2014). In a next work,
we plan to make more evaluation of the protocol model, to detect all anomalies
in the proposed model, to correct and update the model and then to make a
complete verification process.

References

Prism. Available (seen in 2016) at: http://www.prismmodelchecker.org/
Uppaal. Available (seen in 2016) at: http://www.uppaal.org/
Ballarini, P., Miller, A.: Model checking medium access control for sensor networks.
In: Leveraging Applications of Formal Methods, Verification and Validation, 2006.
ISoLA 2006. Second International Symposium on. pp. 255–262. IEEE (2006)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal smc tutorial.
International Journal on Software Tools for Technology Transfer 17(4), 397–415
(August 2015)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Van Vliet, J., Wang,
Z.: Statistical model checking for networks of priced timed automata. In: Formal
Modeling and Analysis of Timed Systems. p. 8096. Springer Berlin Heidelberg
(2011)
Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal analysis of mac protocols for wsns:
a review. Tech. rep. (May 2011)
Ganeriwal, S., Kumar, R., Srivastava, M.B.: Timing-sync protocol for sensor networks.
In: Proceedings of the 1st international conference on Embedded networked sensor
systems. pp. 138–149 (2003)
Hai, N.V.: Formal verification of a distributed routing protocol for wireless sensor
networks wire on a large scale (2015)
Hammal, Y., Ben-Othman, J., Mokdad, L., Abdelli, A.: Formal modeling and verifica-
tion of an enhanced variant of the ieee 802.11 csma/ca protocol. Communications
and networks 16(4), 385–396 (August 2014)
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic
model checking. In: International Workshop on Verification, Model Checking, and
Abstract Interpretation. pp. 73–84. Springer (2004)
Ho, T.S., Chen, K.C.: Performance analysis of ieee 802.11 csma/ca medium access
control protocol. In: Proceedings of PIMRC 96 - 7th International Symposium on
Personal, Indoor, and Mobile Communications. vol. 2, pp. 407–411 (1996)
IEEE organisation: Wireless LAN Medium Access Control (MAC) and Physical Layer
(PHY) Specifications. (July 1995)
Intana, A., Poppleton, M.R., Merrett, G.V.: A formal co-simulation approach for wire-
less sensor network development. In: Proceedings of the 14th International Work-
shop on Automated Verification of Critical Systems (AVoCS 2014). vol. 70. Elec-
tronic Communications of the EASST (2014)
Jensen, K., Kristensen, L., Wells, L.: Coloured petri nets and cpn tools for modelling
and validation of concurrent systems. International Journal on Software Tools for
Technology Transfer 9, 213–254 (2007)
Köpke, A., Swigulski, M., Wessel, K., Willkomm, D., Haneveld, P.T.K., Parker, T.E.V.,
Visser, O.W., Lichte, H.S., Valentin, S.: Simulating wireless and mobile networks
in omnet++ the mixim vision. In: Proceedings of the 1st international conference
on Simulation tools and techniques for communications, networks and systems &
workshops (Simutools). vol. 71, p. 18 (2008)
Koushik, S., Mahesh, V., Gul, A.: Statistical model checking of black-box probabilistic
systems. In: Computer Aided Verification. pp. 202–215. Springer (2004)
Kumar, S., Simonsen, K.I.: Towards a model-based development approach for wire-
less sensor-actuator network protocols. In: Proceedings of the 4th ACM SIGBED
International Workshop on Design, Modeling, and Evaluation of Cyber-Physical
Systems. pp. 35–39 (2014)
Kwiatkowska, M., Norman, G., Sproston, J.: Process Algebra and Probabilistic Meth-
ods: Performance Modeling and Verification, vol. 2399. Berlin, Heidelberg: Springer
Berlin Heidelberg (2002)
Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic computation of maximal prob-
abilisti reachability. In: International Conference on Concurrency Theory. pp. 169–
183. Springer (2001)
Levis, P., Madden, S., Polastre, J., Szewczyk, R., Whitehouse, K., Woo, A., Gay, D.,
Hill, J., Welsh, M., Brewer, E., Tinyos, D.C.: An operating system for sensor net-
works. In: Ambient Intelligence. p. 115148. Springer Berlin Heidelberg (2005)
Lewis, P., Lee, N.: TOSSIM: A Simulator for TinyOS Networks. TinyOS documentation
(2007)
Marta, K., Gethin, N., Jeremy, S.: Probabilistic Model Checking of the IEEE 802.11
Wireless Local Area Network Protocol, vol. 2399, chap. Lecture Notes in Computer
Science, pp. 169–187. Springer-Verlag Berlin Heidelberg (July 2002)
Patil, U.A., Modi, S.V., Suma, B.: A survey: Mac layer protocol for wireless sensor
networks. International Journal of Emerging Technology and Advanced Engineering
3(9), 203–211 (September 2013)
Simonsen, K.I.F., Kristensen, L., Kindler, E.: Generating protocol software from cpn
models annotated with pragmatics. In: In Formal Methods: Foundations and Ap-
plications. vol. 8195, pp. 227–242. Springer Berlin Heidelberg (2013)
Yick, J., Mukherjee, B., Ghosal, D.: Wireless sensor network survey. Computer Net-
works 52(12), 2292–2330 (August 2008)
Younes, H.L.: Verification and planning for stochastic processes with asynchronous
events. Tech. rep., DTIC Document (2005)
Zhai, H., Kwon, Y., Fang, Y.: Performance analysis of ieee 802.11 mac protocols in
wireless lans. In: Wirel. Commun. Mob. Comput. vol. 4 (December 2004)
Zhang, F., Bu, L., Wang, L., Zhao, J., Chen, X., Zhang, T., Li, X.: Modeling and
evaluation of wireless sensor network protocols by stochastic timed automata. In:
Electron. Notes Theor. Computer Science. vol. 296, pp. 261–277 (August 2013)