CONCURRENCY AND COMPUTATION: PRACTICE AND EXPERIENCE
Concurrency Computat.: Pract. Exper. (2015)
Published online in Wiley Online Library (wileyonlinelibrary.com). DOI: 10.1002/cpe.3452
Petri nets-based model for the analysis of NORIA protocol
H. Macia1, M. C. Ruiz1,*,† , J. A. Mateo1 and J. L. Calleja2 1Escuela Superior de Ingeniería Informática, Universidad de Castilla La-Mancha, Campus Univ., s/n, 02071,
Albacete, Spain 2Instituto de Investigación en Informática de Albacete, Avenida de España s/n, 02071, Albacete, Spain
Network rOle-based Routing Intelligent Algorithm is a novel routing algorithm for wireless sensor networks, which combine various effective techniques in order to reduce energy consumption and improve data routes.
This algorithm uses role assignment for distributing tasks over the network nodes and fuzzy logic for making decisions. There is a clear need for the use of formal methods to validate the correctness of the protocols as well as performance and functionality prior to the deployment of such algorithms in a real environment.
This paper presents a formal and rigorous study of Network rOle-based Routing Intelligent Algorithm.
Prioritised-timed coloured petri nets (PTCPNs) have been chosen as an appropriate modelling language. In this way, PTCPNs have been used to describe complete and unambiguous specifications of system behaviour, whereas CPNTools is used to evaluate the correctness of the protocol using state space exploration and for performance evaluation using simulation. Copyright © 2015 John Wiley & Sons, Ltd.
Received 21 March 2013; Revised 10 November 2014; Accepted 15 November 2014
KEY WORDS: wireless sensor networks; performance evaluation; coloured Petri nets; formal methods; routing algorithms; verification 1. MOTIVATION
Recently, a novel generation of network protocols that are able to fulfil the new requirements of wireless sensor networks (WSNs) is emerging. Tests and simulations are the usual validation techniques used for these protocols. Although these techniques give us an excellent overview of the protocol behaviour, some undesirable aspects of the protocol could still be undiscovered, such as deadlocks, livelocks and so on. Therefore, formal verification is needed [1, 2]. The characteristics of wireless ad hoc networks make them especially challenging to model and analyse using existing formal specification languages. One of the main reasons is the fact that they use wireless links for local communication: a wireless ad hoc node can transmit a message simultaneously to all nodes within its transmission range, but the message cannot be received by any node outside that range.
Nevertheless, these challenges are compounded in the case of WSN protocols due to the significant limitations of sensors, such as processing ability, memory capacity and battery lifetime.
The importance of protocol verification before its implementation and the need to be able to carry out performance evaluation prior to the deployment of such a protocol in a real environment has stimulated this work. Moreover, once the model has been developed, it is highly useful for future improvements. In this paper, we have faced the following challenges: modelling spatial entities such as coverage areas and distances, modelling broadcast communication with limited transmission range, modelling time-dependent behaviour, such as the use of timers or transmission delays and modelling energy consumption, all of which in systems using hundreds of nodes. A novel role-based *Correspondence to: M. C. Ruiz, Escuela Superior de Ingeniería Informática, Universidad de Castilla La-Mancha,
Campus Univ., s/n, 02071, Albacete, Spain. †E-mail: firstname.lastname@example.org
Copyright © 2015 John Wiley & Sons, Ltd.
H. MACIA ET AL. routing intelligent algorithm called Network rOle-based Routing Intelligent Algorithm (NORIA)  will be analysed in this paper. NORIA improves data routing in networks oriented mainly to monitoring applications, that is, those in which the information is gathered individually in each node and it is forwarded bottom-up to a special sink called here base station, which is located at the centre. Thus, the network is organised forming a tree. Furthermore, NORIA uses fuzzy logic to make routing decisions, and each node has assigned a role that will determine its functionality.
Moreover, we advocate for the use of prioritised-timed coloured Petri nets (PTCPNs)  for several reasons. First, PTCPNs are based on rigorous mathematical definitions so that one may be capable to obtain complete and unambiguous specifications of the system behaviour. Besides,
PTCPNs have a graphical notation, allowing users to track easily how the system evolves, and provide several analysis methods, including simulation, state space analysis and invariant analysis. In the literature, there are some tools for constructing and evaluating PTCPN models, but we have opted for CPNTools  because it is considered the de facto tool for editing, simulating and analysing
PTCPNs and supports hierarchical nets, priorities and time. In addition, the toolbox provides also the necessary primitives to make your own queries (written as ML functions) to study interesting properties of the system state space. Finally, the tool monitor facilities permit us to extract relevant information from the simulations in order to evaluate system performance.
The authors of this paper have worked closely in the early stages of the design of NORIA algorithm, whereas, in this paper, the evaluation of the fist version of the algorithm is presented.
Currently, of course, we continue working on its improvements and future versions in collaboration with its designers. In detail, our specific contributions in this work are as follows: We formally model NORIA using PTCPNs. We are able to consider node communication and computational behaviour. We have implemented a programme which, from the PTCPN model, automatically generates the model for the system with the desired number of nodes. We analyse this model using state space techniques and validate the correctness of the protocol as well as the absence of deadlocks and proper termination. We validate our results with those obtained in Castalia . We have conducted performance analysis concerning with the following parameters: – Number of packets sent during route discovery phase. Obviously, the fewer packets are sent, the more efficient the protocol in terms of energy consumption. – Energy consumption. Because sensors are highly energy constrained, the energy consumed individually by the nodes will directly impact in system lifetime. – Network setup time. The time needed to discover routes from every node to the base station.