=Paper= {{Paper |id=None |storemode=property |title=Modeling and Analyzing Wireless Sensor Networks with VeriSensor |pdfUrl=https://ceur-ws.org/Vol-851/paper5.pdf |volume=Vol-851 |dblpUrl=https://dblp.org/rec/conf/apn/MaissaKMT12 }} ==Modeling and Analyzing Wireless Sensor Networks with VeriSensor== https://ceur-ws.org/Vol-851/paper5.pdf

Modeling and Analyzing
Wireless Sensor Networks with VeriSensor

Yann Ben Maissa1,2 , Fabrice Kordon2 , Salma Mouline1 , and Yann
Thierry-Mieg2
1
LRIT – CNRST URAC29, Université Mohammed V-Agdal
4, Avenue Ibn Battouta, B.P. 1014 RP, Rabat Maroc,
mouline@fsr.ac.ma,
2
LIP6 – CNRS UMR7606, Université P. & M. Curie 4, place Jussieu, 75005 Paris,
France
Yann.Ben-Maissa@lip6.fr, Fabrice.Kordon@lip6.fr, Yann.Thierry-Mieg@lip6.fr

Abstract. A Wireless Sensor Network (WSN), made of distributed au-
tonomous nodes, is designed to monitor physical or environmental con-
ditions. WSNs have many application domains such as environment or
health monitoring. Their design must consider energy constraints, con-
currency issues, node heterogeneity, while still meeting the quality re-
quirements of life-critical applications. Formal verification helps to ob-
tain WSN reliability, but usually requires a high expertise, which limits
its adoption in industry.
This paper presents VeriSensor, a domain specific modeling language
(DSML) for WSNs offering support for formal verification. VeriSensor is
designed to be used by WSN experts. It can be automatically translated
into a formal specification for model checking. We present the language,
its translation, show how they work on a simple case study, and illus-
trate how several metrics and properties relevant to the domain can be
evaluated.

Keywords: wireless sensor networks, domain specific modeling languages,
model driven engineering, formal verification

1 Introduction
Context Wireless sensor networks (WSNs) are composed of distributed au-
tonomous nodes, containing programs and sensors to monitor physical or envi-
ronmental conditions. Each node is a small physical device embedding sensors, a
small CPU, a battery, a wireless transceiver and an antenna for communication.
WSNs are useful in many contexts, such as environment or health monitoring,
thus being a hot topic [14, 8].
The design of WSNs is complex and error-prone due to their numerous con-
straints:
– lifetime is a crucial preoccupation (even more important than quality of
service [3]). Overall lifetime of the WSN usually depends on sensor nodes
lifetime because nodes have limited battery power.
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 61

– concurrency and asynchrony lead to important issues such as interleaving of
actions and race conditions.
– heterogeneity, because WSNs may contain various types of nodes, each hav-
ing different characteristics (embedded sensors, wireless range, battery ca-
pacity, etc.).
– limited resources, because nodes have limited CPU and memory capacities.
Problem When WSNs are intended to handle critical functions, verification
and validation must be performed to reach a significant confidence in such sys-
tems [12, 7]. Several propositions in that direction have emerged in recent years.
Case studies using Formal Verification. Formal methods have been applied
on case studies to verify some relevant properties for WSNs. For instance, [12]
uses Real-Time Maude, [11] uses the language IF and the model-checker Kronos,
[19] uses UPPAAL.
While these studies show the practical and industrial relevance of performing
formal analysis on WSNs, they use ad-hoc modeling of the system by an expert
in both WSNs and formal verification. This increases the design and verification
costs of WSNs. Moreover, complex verification “tricks” must be elaborated to
achieve the verification goals, creating a gap between the formal specifications
and the real system.
Language-based approaches. Current trends in software engineering show
the emergence of model-driven engineering (MDE): a model of the system is
expressed using a domain specific modeling language (DSML) providing concepts
of the domain. Then, using model transformation technologies, executable code
or simulation models can be automatically produced.
Such DSMLs dedicated to WSNs ease their modeling by domain experts.
However, they currently do not support formal analysis. VisualSense [4] for in-
stance only allows simulation which is useful during the early design stages, but
may not catch rare unexpected events. Baobab [2], Matilda [21], and Medwsa
[20] provide code generators that produce executable artifacts to be deployed on
the physical system.
Unfortunately, these DSMLs often have a very detailed level of specification
(such as wireless signal propagation characteristics), including non-linear parts
that can only be simulated in practice. So, if they are adapted for code generation
or simulation, they generate a high combinatorial explosion and are thus not
suitable for verification.
Contribution This paper presents VeriSensor, a DSML for WSNs and its map-
ping to a formal language for verification and analysis. VeriSensor has the fea-
tures of an architectural description language (ADL [10]) adapted to a modular
description of WSNs.
VeriSensor offers “natural” modeling of a WSN to domain experts by pro-
viding high-level concepts that capture the main use cases of such systems –
periodic data collection, query-based processing, etc. [22, 9]. VeriSensor can be
transformed into a discrete formal model supporting analysis: Instantiable Tran-
sition Systems (ITS) [18]. At this stage, VeriSensor is not intended for code gen-
eration.
62 PNSE’12 – Petri Nets and Software Engineering

Deployment: node class instantiations + topology
Environment: environmental scenario
Node
Node class
class
Node class
Sensor: type + operating mode

consumption
Energy

model
Application: sending orders to sensors +
processing + sending data to network
Network: communication of messages

Fig. 1: Structure of a VeriSensor specification

To illustrate its capabilities, we use VeriSensor on a small example. Analysis
is performed using our own tools, based on the ITS library.
Contents Section 2 gives an overview of VeriSensor. Section 3 presents the lan-
guage concepts together with the biomedical area network (BAN) case study [13]
used as a running example. Section 4 explains the mapping of VeriSensor into
ITS. Then, section 5 presents the analysis results we compute on the case study.

2 Overview of VeriSensor

A VeriSensor specification is composed of the definition of the nodes themselves,
a description of the physical environment in which the nodes evolve, and the
deployment of the system (see Fig. 1).
Description of the nodes There can be several classes of nodes in a WSN
(e.g. in a heterogeneous network), each one having its own characteristics such
as:
– its sensors (which physical quantities to be measured and how they are cap-
tured),
– its application operating mode (periodic data collection, query-based pro-
cessing, etc.) and the way it manipulates data,
– its interface with the network (wireless range, routing, etc.),
– the energy consumption model.
These characteristics are described through four orthogonal dimensions: sen-
sor, application, network and energy. Dimensions describe independent aspects
of the system.
Several node classes can share common dimensions and a node class can be
instantiated several times when several nodes have the same characteristics.
Environment Model It defines physical quantities as a function of space
(x, y, z) and time (t). Thus, the designer may describe a particular scenario in
which the WSN evolves. These scenarios are used to test qualitative properties of
models on given problem instances. A given environment represents a particular
situation in which a given behavior of the WSN is expected.
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 63

Activity 1 & 2 PDA 1
(activity sensor)

ECGTilt 1
(ECG & Tilt sensors) x

Fig. 2: The Body Area Network (BAN)

Deployment Model It defines how instances of node classes are spread in the
physical environment and may change position over time3 . Engineers use this
model to define the topology of the system (number of instances per class and
their coordinates) as well as the logical routing of messages among the nodes.
Structuration in VeriSensor The various dimensions are defined separately
in VeriSensor to support modularity and reusability of WSNs components. The
deployment model of a system is the entry point of a VeriSensor model. It defines
the Environment model and instantiates all nodes from the definition of their
classes.

3 Modeling with VeriSensor
This section presents VeriSensor through the specification of a case study.

3.1 The Body Area Network (BAN)
Our case study takes place in the context of home medical monitoring of patients
who need constant care but can stay out of hospitals. Home medical monitoring
allows to avoid hospitalization, which is as good for medical staff as for their
patients.
The Body Area Network [13] is part of a wireless health monitoring system.
It is composed of (see Fig. 2): i) a set of sensor nodes capable of sensing, process-
ing and communicating vital signs to a personal server ; ii) a Portable Digital
Assistant (PDA) that forwards patient data to a medical center through internet
(3G or WIFI).
The BAN monitors the vital signs of patients recovering from a heart at-
tack. It checks whether a patient is exercising regularly as recommended by
the doctors. WSNs, due to their small size and wireless nature, reduce system
intrusiveness in patient’s lives.
As shown in Fig. 2, two redundant activity nodes detect periods of physical
exercise (when the body activity level is above 8 W atts.kg −1 ) while a third one
periodically collects both heartbeat with an electrocardiogram (ECG) sensor and
the tilt (i.e. upper body orientation) in terms of the absolute angle relative to a
vertical position.
The system designer (i.e. the end-user of VeriSensor) wants to assess some
critical aspects of his system. To do so, he needs to evaluate properties such as:
3
We do not yet support mobility in our approach but this is a natural extension that
is semantically possible in VeriSensor.
64 PNSE’12 – Petri Nets and Software Engineering

System BAN {environment => HumanBody ;
ECGTilt => e c g t i l t 1 ( x = 0 . 1 , y = 0 . 4 , nextHop = pda1 ) ;
Activity => a c t i v i t y 1 ( x= −0.3 , y = 0 . 1 , nextHop = pda1 ) ,
a c t i v i t y 2 ( x=−0.3 , y= −0.1 , nextHop = pda1 ) ;
PDA => pda1 ( x= −0.1 , y = 0 . 3 , nextHop = n u l l ) ; }

Fig. 3: Deployment of the BAN system

p1 evaluate which node limits the system lifetime according to a given scenario,
p2 identify scenarios leading to undesirable situations that should be avoided,
p3 check that the system behaves as expected by “replaying” existing situations
identified by doctors,
p4 compare alternative hardware solutions according to their characteristics
(energy consumption of sensors, processing duration, etc.),

3.2 Modeling the BAN in VeriSensor

This section illustrates the VeriSensor syntax and structure through the modeling
of the BAN case study. Here, we follow a “path” going from the more general
aspects of the system (its elements) up to implementation of some nodes and
the description of its environment.
The Deployment Model Fig. 3 shows the deployment parameters of the BAN
system. Each node instance is parameterized by its position (shown on fig. 3)
and next hop. For instance, the only node of class ECGTilt is located at position
h0.1, 0.4, 0i (when a position parameter is unspecified, its value is 0) and routes
messages to the pda1 instance. Distances are expressed in meters.
The Node Class Model A node class specifies the physical characteristics of
a node to be instantiated. It relates the data dispatched in the four dimensions:
sensing, application, network, and energy (Fig. 4, left).
In the case study, we only consider static routing based on the nextHop
parameter defined in the deployment model. The XNetwork dimension reflects
this choice and is used by all nodes of the BAN as specified in Fig. 3.
Fig. 4 (right) describes the sensors of ECGTilt. In our study, this node class
samples the upper body orientation (Tilt) and the heartbeat (Heartbeat). Sen-
sors are described through their main technical characteristics: the measured

NodeClass ECGTilt { include t y p e s . d e f ;
sensing => ECGTsensing ; sensing ECGTsensing {
a p p l i c a t i o n => ECGTApplication ; sensor ECGSensor (
network => XNetwork ; physical_quantity = H e a r t b e a t ,
energy => ECGTEnergy ; } startup_time = 1 ,
capture_time = 1 ) ; }
sensor T i l t S e n s o r (
physical_quantity = T i l t ,
startup_time = 0 ,
capture_time = 1 ) ;

Fig. 4: ECGTilt, the node class (left) and its sensing dimension (right)
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 65

a p p l i c a t i o n ( collectNode ) ECGTApplication { energy ECGTEnergy {
physical_quantity H e a r t B e a t ( sensing_period = 1 3 , i n i t i a l = 1000;
processing_period = 1 3 , sending_period = 1 3 ) ; reception = 4 ;
physical_quantity T i l t ( sensing_period = 4 , emission = 5 ;
processing = 3 ;
processing_period = 8 , sending_period = 1 6 ) ; }
sensing = 2 ; }

Fig. 5: ECGTilt, its application (left) and energy dimensions (right)

physical quantity startup time (i.e. the time for the sensor to be operational
after being turned on), and its capture time (i.e. the time for the sensor to sense
the value). For instance, ECGSensor measures the heartbeat and starts-up in 1
time unit. Physical quantities are defined in a dedicated model (see Fig. 6, left)
contained in the file types.def.
Each physical quantity q is connected to the environment which must provide
a function returning the values of q at the coordinates of the node instance and
for the current time (at any time). So, in Fig. 4 (right), when ECGSensor samples
a value, it invokes the corresponding function returning the Heartbeat from the
Environment dimension. There is one such function per physical quantity of the
system.
Fig. 5 (left) shows the application dimension of ECGTilt. In VeriSensor, nodes
have several typical behaviors provided as a parameter of the definition. Here,
ECGTilt behaves in “collect” mode (keyword collectNode in the figure): this pe-
riodic data collection is parameterized by a sensing period (i.e. the time between
two samples), a processing period (i.e. the time between two processing of the
sampled data), and a sending period (i.e. time between two emissions of the pro-
cessed data). For instance, Tilt is sampled every 4 time units, processed every
8 time units, and sent every 16 time units.
Fig. 5 (right) shows the energy dimension that describes the initial power
stored in the battery (initial) and defines the consumption of dedicated actions:
reception (message reception), emission (message sending), processing (process-
ing of sampled data), and sensing (sample acquisition).
The Physical quantities Model This model describes physical quantities as
discrete ranges of values (see Fig. 6 left). The underlying semantics is the one
of discrete event systems, so, continuous values must be mapped to an integer

type H e a r t B e a t i s 0 . . 2 0 0 ; include t y p e s . d e f ;
type T i l t i s 0 . . 1 8 0 ; environment c y c l i c HumanBody { context {}
type A c t i v i t y i s 0 . . 1 5 ; body {
c y c l e 6 0 ; // c y c l i c b e h a v i o r ( i n time u n i t s )
H e a r t B e a t function HeartBeatFunc ( x , y , z , t ) {
i f ( 0 <= t and t < 1 0 ) then return ( 9 5 ) ;
e l s i f ( 1 0 <= t and t < 1 4 ) then return ( 4 0 ) ;
e l s e return ( 7 5 ) ; }
T i l t function T i l t F u n c ( x , y , z , t ) { . . . }
A c t i v i t y function A c t i v i t y F u n c ( x , y , z , t ) { . . . } }

Fig. 6: Physical quantities definition (left) and an example of Environment Model
(right)
66 PNSE’12 – Petri Nets and Software Engineering

range. This mapping is user-defined; the designer must evaluate the trade-off
between precision of quantities units and the analysis complexity.
The Environment Model It defines the evolution of each physical quantity
in the model (see Fig. 6, right ) in a given scenario. Thus, it provides a function
that is bound to each sensor sampling the corresponding physical quantity (e.g
HeartBeatFunc is bound to the ECGSensor defined in Fig. 4).
In our example of environment model, values of HeartBeat depend on time
only. Since there are two Activity sensors, ActivityFunc can use the node co-
ordinates to provide different values to each sensor in nodes activity1 and
activity2. Here, values in HeartBeatFunc are deduced from the thresholds of
the application: for instance, any value above 95 is considered a situation where
the patient exercises; then, these values are abstracted to the threshold constant.
Our simplified example illustrates a common situation where WSNs designers
generate such a function from observed traces of the system activity. No pars-
ing of traces is provided since these are too “system dependent”. To extend an
existing trace, a cyclic behavior may be specified.
For some properties of interest such as worst case scenarios, instead of using
the user supplied environment we can use a “free” unconstrained environment,
which might return any value at any time. The clear separation between the
input conditions (environment) and the system specification is important in the
analysis phase described below.

4 Formal Analysis of VeriSensor specifications

Formal analysis by model checking of a system is a powerful technique that al-
lows to capture subtle defects as well as to reason about worst case scenarios
and occurrence of rare events by exhaustively analyzing all possible behaviors.
However it is limited in the scale of the systems it can analyze due to the combi-
natorial state space explosion characteristic of concurrent asynchronous systems.
To partly overcome this problem, techniques and tools have emerged such as SAT
solvers [6] or shared decision diagrams [5].
However formal models are usually limited to a low level specification of the
system transition relation, that describes the state space generator.
Since WSNs are highly time driven and complex, we need a tool support-
ing a large amount of concurrency, some notion of time constraints and able to
tackle combinatorial explosion. To achieve this, we rely on our own preexisting
tool: Instantiable Transition Systems (ITS) [18] and their recent extension that
supports discrete time [15]. The ITS model checker is general and efficient: it
relies on a powerful decision diagram library to cope with the complexity of large
systems. ITS also provide a way to define a structured and hierarchical specifi-
cation of a system and a notion of behavior instantiation. They were previously
experimented to analyze UML activity diagrams through a model transformation
approach [17] similar to the one outlined here.
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 67

4.1 The Underlying Formal Model

This section first gives an informal overview of the underlying formal notations
for VeriSensor. There are two formalisms involved: labeled time Petri nets to
describe elementary behavior and ITS to structure the specification. We only
provide here an intuitive definition (see [18, 15] for a formal presentation).
Instantiable Transition Systems ITS allow hierarchical and compositional
modeling, through a notion of type and instance and an application of the com-
posite design pattern at a behavioral level. A type has an interface, defined as
a set of action labels, and some definition of its internal behavior. Similarly to
component oriented models, an ITS composite is a type that contains instances
of ITS types.
Figure 7 shows a simple example of a composite ITS type. The system offers
one interface, begin, that is synchronized with the start interfaces of the nested
components (Client and Server). This system contains a local transition () that
only has a local effect and is built on the synchronization of send and get inter-
faces. Client and Server are elementary components that contain an automaton
where local transitions are labeled by too. In practice, we use labeled time
Petri nets to define elementary ITS types.
Labeled Time Petri Nets In a Petri net, places (circles) contain tokens
representing resources that are consumed by transitions (rectangles) when they
fire, producing new tokens. A state of a Petri net assigns to each place of the
net an integer representing the number of tokens it contains. In a given state,
a transition is enabled if all its input places (connected by an arc from place to
transition) contain enough tokens. Each arc may be labeled by an integer that
indicates how many tokens are consumed or produced (the value 1 is assumed if
there is no annotation). When firing, a transition produces tokens in the places
connected by outgoing arcs.
Time Petri nets (TPNs) add a notion of clock to each transition, constrained
by an earliest and latest firing time noted [α, β]. As soon as a transition is
enabled, the associated clock starts. This transition cannot fire before α time
units have elapsed and must occur if the transition’s clock reaches β. Hence a
transition with [0, ∞] can occur at any date if it is enabled, like normal Petri
nets. This is assumed to be the default values and is not explicitly shown in the
figures.
The time model is discrete: a special transition elapse represents the evolution
of time by one unit. All clocks evolve simultaneously when elapse is fired.
Client-Server

Client Server begin
start start
start � send start � get
� send � get
�

Fig. 7: Small example of composite-ITS
68 PNSE’12 – Petri Nets and Software Engineering

Labels add a notion of interface to Petri nets, where some transitions (rep-
resented with thick borders) are called public and allow communication with
the outside world. These transitions define the ITS interface. Private transitions
can occur locally, independently from any situation outside the net, and typically
represent an autonomous control flow.

4.2 Mapping VeriSensor to a Formal Specification
The mapping of VeriSensor into formal specifications relies on patterns associ-
ated to its syntactic elements. It is also based on a set of automatically com-
puted abstractions that help containing the combinatorial explosion due to large
datatypes.
The Transformation process To automatically transform the specification
into a formal model we define a set of “generic ITS”, modeling behavioral patterns
that correspond to the VeriSensor execution semantics.
Thus, the transformation process takes parameters in a VeriSensor specifi-
cation to customize such patterns. Each dimension has its own generic pattern
that is hierarchically defined, thus taking benefits from the ITS mechanisms. The
final model is obtained by assembling and instantiating these patterns according
to the deployment model.
Figure 8 shows two examples of generic ITS. The first one (Fig. 8a) rep-
resents the environment as seen by a given node. To obtain this behavior, the
environment function q(x, y, z, t) is projected over the coordinates of the node,
yielding a function q(t) of time only that is specific to the considered node sen-
sor. This function is finally discretized, and encoded as a series of plateau values
that have a certain duration di . Each public transition is labeled by a possible
value of the �physical
1 quantity. The time bound on local transitions () represents
the evolution of q(t) as �time
1
progresses. The last transition n can be added to
�2
represent a cyclic environment. This ITS is parameterized by n, the number of
values sent in the cycle,�2 and by di for i ∈ [1..n], the duration for sending these
�n �1
values. Its ITS interface is the set of possible values sendVi ToSens of the physical
quantity. � �n
�2
n−1
�1
�1
sendV1ToSens
[d1 , d1 ] [d1 , d1 ] sendV1ToApp recvV1FromEnv
�n [a, a]
�2
S
[d2 , d2 ] 1 �2 start S1 [d, d]
[d2 , d2 ]
[d1 , d1 ] �1
•••

�n rdy
[dn , dn ] �n off sendVnToApp recvVnFromEnv
[dn , dn ] idle
•••

[d2 , d2 ]
�2
[dn−1 , dn−1 ] �n−1 Sn [d, d]
Senddd12
sendVnToSens
[dn , dn ] [d1 , d1 ] recvOrderFromApp
d
Senddn−1 �n
n Sn [d1 , d1 ] stop

(a) n-ary cyclic environment [d2 , d2 ] (b) Sensor sampling n values
[d[d1 ,,dd1 ]]
2 2
Fig. 8: Two generic ITS, [dninterfaces
, dn ] transitions are outlined in bold
[d , d
[dn , dn ]
2 2 ]

[d[d n ,,ddnn−1
n−1 ] ]
Senddd12
d
Senddn−1
n
1

1
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 69

 
0 · · · 0 1 


Deployment:  . 


activity1  .
. . . . 0



 

 . . 

 0 . . .
. 


node
 

 1 0 · · · 0 

 


2 Activity, 1 ECGTilt ecgtilt1 pda1
 1 0 · · · 0 

 

 1 0 · · · 0



instances
 1 0 · · · 0 

 


activity2  1 0 · · · 0 



and 1 PDA
 1 0 · · · 0 

 

 1 0 · · · 0 

 

 1 0 · · · 0 

 

 1 0 · · · 0 



 1 0 · · · 0 
0 · · · 0 1 


Network Activity 



ECGTilt
.
.
.
.
PDA
. .
.
0
.









 0 . . .
. 



send,receive


 Sensors
1 0
Sensors
· · · 0 





Energy

Energy
 1 0 · · · 0
node


Energy

 
 1 0 · · · 0
 1 0 · · · 0 

Application




Application
1 0 Application
· · · 0 classes







 1 0 · · · 0 

 

 1 0 · · · 0 

 


start/stop/sendVi

 Network
1
1
0
0 Network
· · ·
· · ·
0
0








1 0 · · · 0 
0 · · · 0 1 

 . . 

 . . . 

 . 0 



Sensor
 

environment
. . .
. 

recvVi
 0 . . 

 

 1 0 · · · 0 

 


ʻʻfreeʼʼ unconstrained Environment
 1 0 · · · 0 

 

 1 0 · · · 0

 1 0 · · · 0 
 

 1 0 · · · 0 

 

 1 0 · · · 0 

 

 1 0 · · · 0 

 

 1 0 · · · 0 

 

 1 0 · · · 0 



1 0 · · · 0

Fig. 9: Structure of the BAN specification according to the deployment of Fig. 3

Fig. 8b represents the behavior of a sensor (as for the BAN system in Fig. 4
right) and is parameterized by n, the number of potential values in the physi-
cal quantity, a, the startup time, and d, the capture time. Its ITS interface is
composed of the control commands (start, stop, recvVi FromEnv , sendVi ToApp).
Although the model size grows with the number of potential values, we con-
trol this combinatorial explosion by reducing the domains of physical quantities
to the minimum set of representative values that impact the system control flow
(see paragraph Abstraction below). Moreover, our ITS tool only encapsulates on
P/T nets.
The transmission of a value Vk from the environment to the sensor is rep-
resented by a synchronization between sendVk ToSens and recvVk FromEnv. The
transition sendVi ToApp transmits sampled values back to the application di-
mension. Because these definitions of the sensor and the environment are clearly
separated we can easily associate the specification to any arbitrary environment
instead of a fixed scenario. This is done in the deployment model.
Similarly, each dimension has its own parameterized pattern. Some dimen-
sion, such as the application dimension of a node class has one pattern per
operating mode (data collection, query processing, etc.).
The Energy dimension is modeled by a one-place Petri net. This place’s initial
marking depends on the initial energy of the node. Transitions (capture, process,
send, receive, etc.) consume the number of tokens corresponding to the energy
cost of the associated operation. Since operations in a node are synchronized
to the energy dimension, the lack of tokens in the energy dimension stops the
corresponding node. When all nodes are out of energy, the system cannot execute
anymore and reaches a deadlock.
The full node is then defined as a composite ITS that assembles the projec-
tion of the environment with the various ITS corresponding to each dimension
(sensors, application, network, energy). This composite ITS has an interface al-
lowing transmission of network messages to other nodes. The nodes are then
finally instantiated and connected according to the logical network topology.
Figure 9 illustrates the overall elaboration of the final formal specification for
the BAN case study based on the VeriSensor architecture. The assembling of a
node class is illustrated for the activity node class. We show how the dimensions
70 PNSE’12 – Petri Nets and Software Engineering

interfaces are synchronized one to another. For example, the public transition
start is a synchronization between the application, energy and sensor dimensions.
This is similar with recvVi between the sensor and environment dimensions. Let
us remind that transitions like recvVi are instantiated as many times as there
are relevant values in the parameters to be exchanged.
Then, each node class is instantiated according to the deployment model.
In Fig. 9, there are two activity nodes, one ECGTilt and one PDA. Context
variables of each node, describing the node characteristics and its coordinates
are initialized according to the deployment model.
Abstractions The final assembling, as described, generates complex models
since each potential value of a physical quantity q makes the overall model larger.
To avoid this, a structural analysis of the VeriSensor specification allows to au-
tomatically abstract the domains of physical quantities to the minimum set of
representative values that impact the system control flow. Such techniques are
derived from automatic symmetry detection [16] or symbolic trajectory evalua-
tion [1]. The complexity of these techniques is low, since it relies on the size of
the specification instead of the size of the state space.
Deriving such abstractions automatically is important because: i) they are
then correct by construction ii) using abstractions does not imply any end-user
knowledge of the underlying techniques. For instance, activity nodes only detect
whether the patient is exercising (i.e. activity>8, see subsection 3.1) or not,
so the domain of the physical quantity activity (i.e. 0 to 15, see Fig. 6 left)
is automatically reduced to 2 values: 0 for no physical exercise, 1 for physical
exercise.
About the Final Model The resulting model for the BAN case study is
composed of 17 ITS-types of which 13 are elementary. The enclosed Petri nets
contain 100 places and 81 transitions of which 43 are time constrained. Thus,
each state is a vector of 143 variables (places marking + transition clocks).
Explicit storage with no optimization of such a state would need 143 integer
values, and thus 1.12 Kbyte with a 64 bit representation.

5 Analyzing the Case study

This section discusses the analysis we performed on our case study. The ITS rep-
resentation was generated according to the rules defined in the previous section
(a tool is being implemented). From the ITS model this procedure produces,
we evaluated the properties identified in section 3.1. All experimentations were
done with our own tool based on our ITS library [15].
Prior to this, we discuss the efficiency of this translation with regards to the
analysis scalability (based on the parameters values). All experiments were run
on a Xeon 64 bits at 2.6 GHz processor.
Analysis Scalability The model of the BAN case study is associated with
a “free” unconstrained environment providing all possibles situations from the
environment point of view. Thus leading to the analysis of possible situations in
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 71

1E+16 6E+06
State Space Size 1E+15 5E+06

Memory (KB)
1E+14 4E+06
1E+13
3E+06
1E+12
2E+06
1E+11
1E+06
1E+10
50
10

50
10

10
0

00
Initial energy (energy units) Initial energy (energy units)

(a) Number of states (logarithmic scale) (b) Memory used (linear scale)

1.4E+04 1E+06

Number of state per byte
1.2E+04
1E+05
1.0E+04
Time (s)

8.0E+03 1E+04
6.0E+03 1E+03
4.0E+03
1E+02
2.0E+03
0.0E+00 1E+01
50
10

50
10

10
0

00
Initial energy (energy units) Initial energy (energy units)

Fig. 10: Evolution of the state space complexity when the initial energy allocated
for each node increases (activity sensor period=18 time units for node activity1
and 9 time units for activity2, ECG sensor period=10 time units, Tilt sensor
period=29 time units, message emission for every node=5 energy units, message
reception for every node=4 energy units, sensing cost for every sensor = 2 energy
units, processing sampled data = 3 energy units for every nodes)

the system. Figure 10 shows the evolution of the corresponding state space, its
computation time and the memory required to build it, according to the initial
energy allowed to the system. In these scenarios, a time unit lasts 1 minute and
an energy unit is 50 microjoules. Such interpretation is decided by the designer
of the WSN.
As seen in Fig. 10a, the state space grows exponentially, the end of the curve
tending to a line in a logarithmic scale. Its representation in memory, as well
as the computation time, evolves in a much more favorable way, thus validating
the choice of ITS, based on decision diagrams, that already proved its efficiency
for such systems [18].
Figures 10b and 10c show the evolution of memory and time required for
state space construction according to the initial energy allocated to each node. As
shown, we can scale this energy up to 1000 units and still have a reasonable CPU
and memory consumption (5.4 GBytes and 3.7 hours). From an industrial point
of view, it becomes feasible to process larger values on current high-performance
servers.
72 PNSE’12 – Petri Nets and Software Engineering

Considering the memory required to store a state and the size of the state
space, our translation into ITS, even if it is yet at a prototype stage, shows en-
couraging results (up to 5.3×105 states per byte as shown in Fig. 10d). Moreover,
no particular optimization has been done besides the abstraction automatically
computed during the translation, thus avoiding the need for expertise in the
underlying formal tools.
This experiment on the BAN shows a good scalability potential for the overall
approach. In particular, it shows the verification complexity of reachability prop-
erties (e.g. p2 in section 3.1) that are a reliable way to detect “rare events”, dif-
ficult to track using classical simulation-based techniques. However, if a Yes/No
answer for a reachability property is provided within a reasonable time, we mea-
sured that computation of a counterexample takes significantly more time and
memory.
Information about the System Lifetime (p1 ) Exhibiting the energy con-
sumption of the WSN in the worst case scenario allows the end-user to evaluate
a lower bound of the system lifetime. Figure 11a shows the worst case lifetime
evolution of the BAN nodes.
To do so, we associate the BAN model with an unconstrained environment
allowing any action. We thus compute a superset of all the possible behaviors
from which we can obtain a worst case scenario. In this model, we search for
Send , the set of states where at least one node cannot communicate anymore (its
energy is below a constant M in, the minimum energy to send a message). Then,
our tool computes the shortest path (i.e. shortest transition sequence) leading
from the initial state to a state in Send . To get the corresponding lifetime, we
count the occurrences of the elapse transition (that let time elapse for 1 time
unit). This is the minimal time from the initial state to a state where an observed
node cannot communicate anymore.
The objective is not to provide quantitative information since the initial
number of energy units allocated to nodes is not sufficient (Fig. 11a shows a
system duration in hours, while, at least, weeks would be needed). However, a
designer can get an idea of the most critical component (i.e. the one that fails
Worst case lifetime (time units)
Worst case lifetime (time units)

1400 1400
BAN node Configuration
1200 EGCTilt 1200 variant 1
1000 Activity1 1000 variant 2
Activity2
800 800
600 600
400 400
200 200

0 0
0

10
50
10

00
0

Initial energy (energy units) Initial energy (energy units)

(a) BAN nodes worst case lifetime (b) Compared lifetime of activity1

Fig. 11: Lifetime analysis on the BAN case study
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 73

first) according to various scenarios. This result is complementary of simulation
that can tackle longer duration but not in an exhaustive way.
Let us note that, in Fig. 11a, ECGTilt and Activity1 are the ones to lack energy
first. Typically the difference between the lifetime of Activity1 and Activity2 can
be analyzed and several parameters can be studied to overcome this situation.
Later in this section, we show how two alternative designs for Activity1 can be
explored.
Reachability Properties (p2 ) A typical and interesting reachability property
deals with unexpected deadlocks in the system (expected ones being those where
nodes have no more energy). This can reveal real deadlocks in the system, or
allow the identification of crucial nodes whose activity is required to keep the
system working. Such a situation can be detected using the following reachability
formula, computed with no additional cost with respect to state space generation:
^
dead ∧ (energy(i) > M ini ) (1)
i∈N odes

Where M ini corresponds to the minimum energy required by node i to send
a message and dead is the boolean meaning that the current state of the state
space has no successor. On the BAN case study, this property is verified. It
was computed with the unconstrained environment and with a configuration
providing up to 500 energy units (it took 1 hour 38 minutes and 2.8 Gbytes).
Checking Behavior for Existing Situations (p3 ) Such properties usually
require causal formulas expressed by means of temporal logic.
For the BAN system, a typical property is to ensure that the system generates
neither a false negative (i.e. a heart attack is not detected) nor a false positive
(i.e. a heart attack is detected by mistake in the system). To get this equivalence
relation, we use the CTL formula 2 to detect the presence of a false negative and
the CTL formula 3 to detect the presence of a false positive.

AG(occursheart attack =⇒ AF (detectedheart attack )) (2)

AG(¬occursheart attack =⇒ AF (¬detectedheart attack )) (3)
In this formula the AG and AF operators respectively mean “in all cases”
and “in all futures”. occurse is either true or false for a given environment e.
In the BAN case study, a given environment corresponds to a patient behavior
which is annotated by the doctors as being sick or healthy. detectede is a state
property. In our case (e = heart attack) it involves the PDA and corresponds to
the detection of low activity (gathered from the activity sensors) and bradycardia
detected by ECGTilt.
On the BAN case study, this property is verified (this was computed up to
the system with 500 energy units). This was tested for several environments
representing different patients. Such a computation is less complex in time and
memory than the worst case lifetime analysis since the system is more con-
strained. Formulas were computed for 500 initial energy units. Formula 2 was
74 PNSE’12 – Petri Nets and Software Engineering

Parameter value in config1 value in config2
sensing frequency 11 TU 20 TU
acquisition time 3 TU 1 TU
acquisition energy 3 EU 4 EU
processing time 1 TU 2 TU
processing energy 4 EU 6 EU
emission time 2 TU 3 TU
emission energy 6 EU 8 EU
reception time 2 TU 3 TU
reception energy 5 EU 7 EU

Fig. 12: Data for the two studied variants in time units (TU) or energy units
(EU)

computed in 1 hour 45 minutes and 2.8 Gbyte memory. Formula 3 was computed
in 1 hour 28 minutes and 2.7 Gbyte memory.
Comparing Alternative Solutions (p4 ) The choice of a given component
may have an impact on a WSN lifetime or on some important characteristics of
the system. VeriSensor can be useful to compare two possible solutions. To do so,
the designer may either change the characteristics of the nodes to be replaced
(if only those change) or replace the node by an instance of another node class.
For the BAN case study, we want to evaluate the impact of two configura-
tions on the system lifetime (e.g. when at least one node cannot communicate
anymore). These configurations differ with the characteristics of the activity
nodes. The first configuration (config1 ) embeds a node that samples often but
performs light computation. The second one (config2 ) uses a node that performs
less samples but more computations.
To evaluate these configurations, we provide two variations of the activity
node specification, following the information displayed in Fig. 12. Then, the
obtained specification is linked to the “free” unconstrained environment used to
evaluate the worst case lifetime of the system. This work leads to the results
displayed in Fig. 11b.

6 Conclusion

This paper presented VeriSensor, a domain specific modeling language for wire-
less sensor networks (WSNs), designed to be used by WSNs experts and offering
support for modeling and formal verification. The objective is to evaluate both
quantitative results (e.g. estimation of the system’s lifetime or average consump-
tion per time unit) as well as qualitative results (e.g. detection of unexpected
situations to be avoided).
VeriSensor enables the modeling of a WSN by providing high-level concepts
that support the main use cases of WSNs. Thus, specifying WSNs consists in
defining the node characteristics, how nodes are deployed and the physical en-
vironment in which the system evolves. The physical environment may model
all possible situations (the “free” unconstrained environment), thus leading to
Y. Ben Maissa et al.: Wireless Sensor Networks with VeriSensor 75

the evaluation of the WSN in the worst possible condition. It may also model a
dedicated scenario for which the WSN behavior has to be verified.
Instantiable Transition Systems (ITS) and time Petri nets are the underly-
ing formal techniques used for verification. They show encouraging scalability
capabilities, thus enabling the analysis of reasonable systems with significant
parameters.
The main advantage of the overall approach is to make formal specification
and verification more accessible to the end-users (i.e. the designers of WSNs).
Even if we focus on the verification aspects, our approach does not exclude
simulation. In fact, since VeriSensor has a formal semantic, it is executable and
thus, can be simulated. Then, the environment dimension still allows to select
one situation where the system has to be plugged in.

References
1. S. Adams, M. Björk, T. F. Melham, and C.-J. H. Seger. Automatic abstraction
in symbolic trajectory evaluation. In Formal Methods in Computer-Aided Design,
pages 127–135. IEEE Computer Society, 2007.
2. B. Akbal-Delibas, P. Boonma, and J. Suzuki. Extensible and precise modeling for
wireless sensor networks. In UNISCON, pages 551–562, 2009.
3. I. F. Akyildiz, W. Su, Y. Sankarasubramaniam, and E. Cayirci. A survey on sensor
networks. Communications Magazine, IEEE, 40(8):102–114, Aug. 2002.
4. P. Baldwin, S. Kohli, E. A. Lee, X. Liu, Y. Zhao, C. H. Brooks, N. V. Krishnan,
S. Neuendorffer, C. Zhong, and R. Zhou. Visualsense: Visual modeling for wireless
and sensor network systems. Technical report, U.C. Berkeley, 2005.
5. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. Hwang. Symbolic
model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE
Symposium on Logic in Computer Science, pages 1–33. IEEE Computer Society
Press, 1990.
6. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Se-
bastiani, and A. Tacchella. Nusmv 2: An opensource tool for symbolic model check-
ing. In E. Brinksma and K. Larsen, editors, Computer Aided Verification, volume
2404 of Lecture Notes in Computer Science, pages 241–268. Springer Berlin / Hei-
delberg, 2002.
7. S. C. Ergen, M. Ergen, and T. J. Koo. Lifetime analysis of a sensor network with
hybrid automata modelling. In WSNA, pages 98–104, 2002.
8. O. Gnawali and M. Welsh. Sensor networks architectures and protocols. In Emerg-
ing Wireless Technologies and the Future Mobile Internet, pages 125–153. Cam-
bridge University Press, 2011.
9. A. Mainwaring, D. Culler, J. Polastre, R. Szewczyk, and J. Anderson. Wireless
sensor networks for habitat monitoring. In 1st ACM Int. workshop on Wireless
sensor networks and applications (WSNA), pages 88–97. ACM, 2002.
10. N. Medvidovic and R. N. Taylor. A classification and comparison framework for
software architecture description languages. IEEE Trans. Softw. Eng., 26:70–93,
January 2000.
11. L. Mounier, L. Samper, and W. Znaidi. Worst-case lifetime computation of a
wireless sensor network by model-checking. In 4th ACM workshop on Performance
evaluation of wireless ad hoc, sensor, and ubiquitous networks (PE-WASUN), pages
1–8. ACM, 2007.
76 PNSE’12 – Petri Nets and Software Engineering

12. P. C. Ölveczky and S. Thorvaldsen. Formal modeling and analysis of the ogdc
wireless sensor network algorithm in real-time maude. In 9th Int. conf. on Formal
Methods for Open Object-based Distributed Systems (FMOODS), pages 122–140.
Springer, 2007.
13. C. Otto, A. Milenković, C. Sanders, and E. Jovanov. System architecture of a wire-
less body area sensor network for ubiquitous health monitoring. J. Mob. Multimed.,
1:307–326, January 2005.
14. K. Sohraby, D. Minoli, and T. Znati. Wireless sensor networks: technology, proto-
cols and applications. Wiley Interscience, 2007.
15. Y. Thierry-Mieg, B. Bérard, F. Kordon, D. Lime, and O. H. Roux. Compositional
Analysis of Discrete Time Petri nets. In 1st workshop on Petri Nets Compositions
(CompoNet 2011), volume 726, pages 17–31, Newcastle, UK, June 2011. CEUR.
16. Y. Thierry-Mieg, C. Dutheillet, and I. Mounier. Automatic symmetry detection
in well-formed nets. In Proc. of ICATPN 2003, volume 2679 of Lecture Notes in
Computer Science, pages 82–101. Springer Verlag, June 2003.
17. Y. Thierry-Mieg and L.-M. Hillah. UML behavioral consistency checking using
Instantiable Petri nets. ISSE, 4(3):293–300, 2008.
18. Y. Thierry-Mieg, D. Poitrenaud, A. Hamez, and F. Kordon. Hierarchical Set Deci-
sion Diagrams and Regular Models. In 15th Int. conf. on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS), volume 5505 of LNCS, pages
1–15. Springer, March 2009.
19. S. Tschirner, L. Xuedong, and W. Yi. Model-based validation of QoS properties
of biomedical sensor networks. In 8th ACM Int. conf. on Embedded software (EM-
SOFT), pages 69–78. ACM, 2008.
20. C. Vicente-Chicote, F. Losilla, B. Álvarez, A. Iborra, and P. Sánchez. Applying
mde to the development of flexible and reusable wireless sensor networks. Int. J.
Cooperative Inf. Syst., 16(3/4):393–412, 2007.
21. H. Wada, P. Boonma, J. Suzuki, and K. Oba. Modeling and executing adaptive sen-
sor network applications with the Matilda UML virtual machine. In 11th IASTED
Int. conf. on Software Engineering and Applications (SEA), pages 216–225. ACTA
Press, 2007.
22. Y. Yao and J. Gehrke. The cougar approach to in-network query processing in
sensor networks. SIGMOD Record, 31, 2002.