1 Introduction

Wireless sensor networks (WSN) have a big number of application fields. They are used mainly for environmental sensing, industrial monitoring, target tracking, assisted living and recently internet of things [1]. As a networked system, WSN application needs sensor node as hardware part, operating systems, some networking protocols and the application itself often uses other technologies and techniques such as Ad hoc networks [2], multi-agent systems [3] and data processing [4]. So, its performance depends on all of these factors. Before deploying and installing a WSN, it is imperative to evaluate performances of the new system. There are several methods which can be used for WSN protocols evaluation and validation. The testbed method consists to produce a prototype with a real experimentation, it is the most realistic and complete method but the most costly. For this reason, several works on WSN especially in the academic field use simulation method where protocols are implemented and tested in various simulators like NS2/3 [5], Omnetpp/Castalia [6, 7], Glomosim [8] and J-Sim [9]. However, it is not easy to obtain solid conclusions from a simulation study. This is due to the suitability of a special tool of simulation and correctness of the used models. In addition, using simulators requires an important effort and makes an important time processing. The third way to evaluate performance is emulation which is a compromise between simulation and real testbed. Emulation combines between elements of real tests and some assumptions obtained by simulation. It generally has realistic parameters which are directly incorporated by software into the architecture being used [10]. So, real and virtual nodes can be used in the same time. As WSN emulator, there is SPSim, EmPro, EmStar, SunSpot Manager and FreeMote emulator. To sum up, protocol verification and validation using simulations or development of prototypes is sometimes difficult, requiring experience in software development, hardware configuration and a considerable working time. Finally, it is possible to use formal methods for protocol validation. These methods are based on mathematic formulation and analyze concluding to obtain exact and proved results. Formal validation needs two fundamental steps, beginning with modeling part which is the most delicate task in this approach. The second step is to study and analyze the system characteristics and performances through the selected model. The most used tools in this field are Markov models [11,12,13], probabilistic and logical modeling and analysis [42], Event B-method [14,15,16,17,18] and Petri nets [19, 20]. This paper proposes to validate WSN energetic model using some formal methods where the system will be described using an Event B-method formulation and the system operation will be modeled by a coloured Petri net. The work consists in defining and modeling each layer in the protocol stack using Petri nets passing by formal specifications and verifications in order to study and validate the quality of protocols managing message routing and energy consumption in a WSN. The main objective is to analyze how the system will perform. So, it is possible to correct, enhance and validate the system operation before deploying it in service. The paper is organized as follows: in Sect. 2, some preliminary notions are introduced such as Event B-method and Petri nets. Section 3 presents related works which are based on these formal tools to validate WSN protocols. Section 4 discusses the proposed model for WSN formal validation. Results and analysis of this proposition are discussed in Sect. 5 and finally, Sect. 6 presents conclusions and future work.

2 Preliminaries

Before giving details on formal validation of WSN energetic model, it is important to recall some fundamental notions related to the formal tools used for the proposed modeling. These tools are mainly the Event- B method, Petri nets and coloured Petri nets.

2.1 Event B Method and Program Proving

The event-B [14, 16] is a software development language based on B method, a tool-supported formal method based on an abstract machine notation; it can be used to model all sorts of discrete event systems, among them sequential programs [15].

System developing with B-method proposes a cycle shown in Fig. 1 and passing by the following steps:

  1. 1.

    Translation of informal system requires a specification into the abstract model or the abstract machine notation.

  2. 2.

    Refinements through a sequence of detailed versions that must be proved to be consistent with the previous one.

  3. 3.

    Possibility of translation into some classical programming language such as C++ and Java.

Fig. 1
figure 1

B-method methodology

Full size image

An event-B project has the following components:

  1. 1.

    Context: representing the static structure of a discrete system, it is a sort of first-order theory that contains declaration of constants and axioms about these constants using an abstract language based on predicates of first order logic, simple sets theory and arithmetic on Z; set of integers. For example, the context for searching a value in an array of strictly positive integers can be described as:

    figure e
  2. 2.

    Abstract machine: it describes the dynamic structure or the system evolution using constants and axioms which are imported from context by the SEES clause. The abstract machine must describe:

    • The system’s state through a set of variables;

    • The consistency of the state by a set of invariants (some formulas to satisfy);

    • Some events to define the possible evolutions of the machine’s state.

    The abstract machine associated to the previous example can be written as:

    figure f

There are some tools which can be used for Event-B development. The most known is Rodin [17, 18], an open source platform based on Eclipse IDE for Event-B that provides effective support for refinement and mathematical proof of system description.

2.2 Coloured Petri Net

In general, a petri net PN [19] is a famous mathematical model for distributed and event discrete systems. This formal tool can be used to describe concurrent and synchronous activities. Graphically, a PN is represented by a directed bipartite graph in which vertexes represent transitions (modeling events that may occur and are represented by bars) and places (modeling conditions that are represented by circles). As all graphs, a PN is represented by an incidence matrix and a marking vector. So, the system evolution can be obtained simply by multiplication of the matrix and the marking vector of each step. This formulation allows studying several qualitative system proprieties like reachability, boundedness and liveness. To improve its power of analysis, there are several extensions of PN such as stochastic PN, timed PN and coloured PN. The last one will be used in this paper. Coloured Petri Nets (or CPNs) is a language mainly used for modeling and validation of concurrent and distributed systems in which concurrency, synchronization, and communication play a major role [20]. CPN models are formal and hence, they can be used to prove properties about the modeled systems. This is done by model checking based on state space exploration. The main characteristic of CPN is the possibility to have different types of marks or tokens specified by different colours values in each place. More interesting, several types of transitions can be expressed, depending on the combinations of coloured tokens. Formally, a CPN is defined by a tuple [21, 22]:

$$\begin{aligned} CPN=(S, P, T, A, N, C, G, E, I) \end{aligned}$$
(1)

where:

  • S is a finite set of non empty types, called color sets.

  • P is a set of n places P = {P1, P2,..., Pn}.

  • T is a set of m transitions T = {T1, T2,..., Tm}.

  • A is a finite set of directed arcs relating places to transitions or transitions to places, so:

    $$\begin{aligned} A \subseteq (P) \cup (T) \end{aligned}$$
    (2)

  • N is a node function defined from A into \(\text(P)\!\cup\!(T)\).

  • C is a color function defined from P into S.

  • G is a guard function defined from T into expressions such as:

    $$\begin{aligned} \forall t \in T:[Type (G(t)) = Boolean \wedge Type(Var(G(t))] \subseteq S \end{aligned}$$
    (3)

  • E is an arc expression function defined from A into expressions such that:

    $$\begin{aligned} \forall t\in T: [Type (E(a)) = C(p(a)_{MS}) \wedge Type(Var(E(a))] \subseteq S \end{aligned}$$
    (4)

    where p(a) is the place of N(a).

  • I is the initialization function from L into closed expressions such that:

    $$\begin{aligned} \forall p\in P: [Type(I(p)) = C(p)_{MS}] \end{aligned}$$
    (5)

In (4) and (5) the MS notation signifies a multi sets type. In practice, there are some tools used to study and evaluate CPN models such as CPN-tools [23] and TransCPN [24].

3 Related Works

3.1 Works Using Event-B

A detailed explanation of Event-B modeling and semantics of each part is found in [43]. Authors give a case study in this context and propose a stepwise correct-by-construction model to build asynchronous distributed systems which a priori realize their choreographies by relying on a necessary realizability condition and then applying several refinement steps to generate the distributed peers of the network.

In [44], a fairness based method is proposed by integrating temporal and first order logic with event-B/Rodin proof for modeling and verification of safety and liveness properties in distributed systems. More exactly, they use the temporal logic for actions applied on three examples of protocols as a theoretical framework for computability reasoning about WSN in order to extract certain repeating patterns in the proofs which can be easily identified and reused for similar modeling.

An Event-B formal verification model is used in [25] for checking WSN-ZigBee protocol stack in a layered manner, where protocol semantics are well defined to be embedded in the Event-B language. In that model, each layer with its attributes is modeled in Event-B machine then, different events like initialization events are used to model interfaces between layers, where Event-B guards are used to define preconditions for those events. Finally, for modeling correctness properties of the protocol, author uses Event-B invariants and proof obligations.

In [26], authors propose a formal co-simulation framework for WSN. The goal of that work is to provide a high level abstraction for software engineering practice in WSN by combining existing simulation and proof-based formal verification approaches. So, they use the refinement method of the Event-B and its Rodin toolkit to model and verify the sensor operation from application to MAC layer in a layered and formal manner. In the other hand, MiXiM simulations are used to provide full confidence about reliability and performance analysis of physical environment.

The work in [27] is focused on wireless sensor–actor networks, where both ordinary sensor nodes and more sophisticated and powerful nodes, called actors, are present. In that paper, authors introduce several formal models for that type of wireless networks. Those models formulas are recently introduced with an algorithm for recovering actor–actor coordination links via the existing sensor infrastructure. They prove via refinement that that recovery is correct and that it terminates in a finite number of steps. In addition, they propose a generalization of the formal development strategy, which can be reused in the context of a wider class of networks. They elaborate their models within the Event-B formalism, while their proofs are carried out using the RODIN platform. They formally model a distributed recovery algorithm for wireless sensor–actor networks. They develop the model in four increasing levels of abstraction that refine each other. They prove the correctness and successful termination of the algorithm, tool-assisted. They put forward three types of coordination links in wireless sensor–actor networks. They finally generalize the formal model to a wider class of networks via refinement patterns.

Modeling distributed algorithms for mobile Ad-hoc networks and looking at their assumptions is the subject of [28]. Proving the correctness of these algorithms for dynamic networks is a topic of intensive research. In fact, the solutions which have been proposed previously to express and prove the correctness of distributed algorithms are usually done manually. In addition, all these solutions lack a consensus about their development and their proof. The main contribution of that paper is to propose a general and formal model for dynamic networks based on evolving graphs and Event-B formal method. In fact, evolving graphs is a powerful tool to express fine-grained properties. That model allows to handle topological events and to characterize the concept of time with some particularities. It is implemented with Event-B, based on refinement technique. The proposed model is illustrated by an example of a distributed algorithm encoded by local computations models.

An other work on ZigBee protocol is found in [29] but it focused on secure network authentification. Like the previous work, the Zigbee protocol behavior is described by an Event-B abstract machine adding key management mechanism and other security parameters for context and axioms part to obtain the complete model which is analyzed in Rodin platform.

In [30], the proactive routing protocol OLSR is modeled and analyzed based on event-B and the Rodin theorem proving platform. The protocol complexity is defined by five distinct abstraction layers which are linked to each other by refinement. This approach can be used as a proof-of-concept to be adapted to model and verifying other routing protocols used in large-scale WSN.

In [31], authors formally analyze the zone routing protocol (ZRP), a hybrid routing framework, using Event-B. Since Ad hoc routing protocols are responsible for searching a route from the source to the destination under the dynamic network topology. Hybrid routing protocols combine the features of proactive and reactive approaches. So, the formal specification of a hybrid routing protocol in the dynamic network environment is a challenge. The authors develop the formal specification by the refinement mechanism. It allows them to gradually model the network environment, the construction of routing zones, route discovery based on border casting service and routing update. They prove the stabilization property in the inactive environment. In addition, they demonstrate that discovered routes hold the loop freedom and validity in each reachable system state. To show that the formalization is consistent with the informally expressed requirements, they adopt an animator, ProB, to validate that model. That work provides reference to analyze extensions of the ZRP and other hybrid routing protocols.

3.2 Works Using CPN

Petri nets are widely used to model and verify concurrent and distributed systems functionalities especially in WSN. Several works on formal methods for WSN modeling and validation are interested by the MAC layer like [32] that uses the hierarchical modeling capability of CPN for modeling and evaluating the performance of the S-MAC protocol where it defines a CPN level for wireless channel, node scheduling, neighbors scheduling and message control parts.

The work in [33] presents a CPN based model which allows verifying and validating the design properties and structural behavior of wireless sensor and actuator networks. It is a computation model based on predefined components and CPN specifications giving possibility to generate the equivalent code in C language. The system components can perform two types of activities, periodic ones running with constant time intervals and aperiodic ones which are initiated by the occurrence of external events. For interaction between activities, authors use specific scheduler and timing components.

Authors of [34] are interested in a kind of intelligent wireless sensor networks (IWSN) which is set up from the point of view of multi-agent systems. IWSN is composed of some sensor node agents, some cluster head agents, a base agent and a command agent. According to the characteristics of these agents, intelligent wireless sensor networks model (IWSNM) based on Petri nets is proposed, which can accurately and unambiguously model the overall and individual characteristics of the networks. Moreover, IWSNM can be analyzed, verified and validated by the supporting tools of Petri nets. Consequently, the defects in early design stage can be detected, and the security and reliability can be improved. Finally, IWSNM are employed to develop the target tracking systems.

For role based routing protocol in WSN, [35] presents a formal study for the Network rOle-based Routing Algorithm (NORA) protocol using CPN as a modeling language to obtain unambiguous and complete specifications of system behavior. It begins by writing a pseudo-code describing the protocol then they construct the corresponding CPN that shows all possible states of node, its role and activities with necessary parameters. CPNTools have been used to evaluate and study correctness using state space exploration.

Because nesC is the most used programming language for implementing WSN applications, authors of [36] present a tool that generates power consumption models as CPN from the nesC code of the WSN application. That approach uses three levels to define CPN models, basic models representing operators and statements in the application code. Next, these basic models are composed into function models to express the power consumption of commands and events and finally the entire WSN application is obtained by the composition of all function models. So, it is possible to evaluate the power consumption by determining consumption of each level in that hierarchical CPN.

In [37], authors use a components oriented model and the expressiveness of Coloured Petri Nets to model and estimate network’s energy consumption. Each particular component of a sensor is modeled alone then it is interfaced to other components to obtain the global behavior. The most interesting part in that work is radio and MAC behavior.

In [38], the WSN-PN tool is proposed, it allows the congestion detection on a WSN setting. A recent work in [39] concerns modeling of MAC protocols using CPN for platform independent modeling, initial verification and simulation. Platform-specific implementations for multiple platforms are generated by the Petri Code tool, including MiXiM for simulation and TinyOS for deployment.

An other technique is proposed in [40] for verifying congestion probability on WSN which is modeled by CPN. That work consists to attach reliable probability on each node allowing knowing the probability of reaching the sink according to the network topology. These probabilities combined to routing probabilities are used to transform that topology into a discrete time stochastic CPN. The paper gives some analyzes by tracing the state space of the CPN model. Finally, it estimates that approach is more observable, scalable, and portable than Markov model.

In [41], authors propose a modeling and performance analysis for IEEE 802.15.4 which is the standard protocol for low-rate, low-power wireless personal area networks, including the physical layer and media access control layer specifications. Particularly, some mechanisms for certain purposes, such as transmission efficiency and power saving, are introduced. It is worthwhile to evaluate how the protocol can fulfill the quality of service requirements. Coloured Petri nets are chosen for the modeling and analyzing purposes because of the enhanced modeling power and abundant analysis techniques. The modeling method for wireless network protocols using CPN is summarized, which is general enough and can be directly used to model various wireless network protocols like IEEE 802.15.4. During the modeling process, some modeling techniques are utilized, e.g., building the model in the hierarchical and modular way, reducing the model by the folding technique, and normalizing the modeling process by the modeling patterns. Simulation is conducted on the CPN model to compute some performance metrics such as throughput, delivery ratio, delay, and energy cost. All the above show that coloured Petri nets can play an important role in modeling and analyzing wireless network protocols.

It is to note that related works cited here are based on Event-B modeling for the first part and sometimes CPN modeling combined to some language notations such as C or Nesc code. However, there is not works that try to represent the CPN model corresponding to an Event-B model. So, a solution in this context is given in details in this paper.

4 Proposed Model for WSN Formal Validation

In order to model the proposed solution on formal validation in WSN, an event-B definition is created for each layer in the network according to the OSI model, especially the application, transport, network and MAC layers. In this work, correctness of each layer has been studied in two steps like it is summarized in Fig. 2.

  1. 1.

    In the first step, general mechanism of concerned layer has been modeled by a CPN using the CPNTools environment [23] with verification.

  2. 2.

    In the second step, the Rodin platform has been used to model and proof correctness of network by detailing the corresponding event-B model for each layer.

Fig. 2
figure 2

Flow diagram of modeling and proof

Full size image

The diagram of Fig. 3 shows a general idea on aspects to be treated and modeled for each layer in this work.

Fig. 3
figure 3

General aspects concerned by the modeling

Full size image

This layered and encapsulated principle is similar in formal methods such as event-B, which is based on refinement as illustrated in Figs. 2 and 3. The refinement allows to build a model gradually by making it more and more precise, so that it is closer to the reality. So, it is not about building a single model representing once and for all the reality; this is clearly impossible due to the size of the state space and the number of its transitions. It would also make the resulting model very difficult to master. In theory there are no precise limit while making refinements of a model that is very safe and rigorous, that is why CPN are used here to get a readable number of states and visible for readers. If there is a large number of states in a single module refined several times, there is a need for module decomposition, then a threshold is fixed in this case.

4.1 Application Layer

Application layer is the highest level of a network operation where details of transmission are not treated. At this level, sending and receiving messages between nodes through a network are modeled without mentioning other parameters to specify how and when do something. So, the CPN of Fig. 4 explains what do the application layer.

Fig. 4
figure 4

CPN model for application layer

Full size image

In a second time, an event-B model is created for checking correctness of network operation at this level. Such model contains two parts, context and machine. The static part of application layer is defined by the following context named context_app written in event-B as:

figure g

This context describes the WSN application by a set of nodes, application type and a set of modes of each node in the SETS closure. So, a node can be in one of sending or receiving modes which is shown by the AXIOMS closure in the previous context. The dynamic part of a WSN application is defined by an event-B machine named application for which sets of variables, invariants and events must be given like in Fig. 5.

Fig. 5
figure 5

Application layer machine description

Full size image

The first part shown at left in the previous model defines node parameters which are its identifier ID, application type installed on the node app, different modes or status of a node noted, receiving and sending. Finally the variable time represents the time counter initialized to zero. The rest parts INVARIANT and INITIALISATION closures describe respectively possible and initial values of variables.

The effective operation or dynamic comportment of nodes is managed by a set of events. For each event, it is necessary to verify some conditions in the form of guards noted grdi then the list of possible actions to perform by the node noted actj according to each situation. For example, in the event SEND, there is grd1 and grd2 used for verifying ID and time of the concerned node. If conditions of guards are verified, node must permit its mode to SEND and increment its time counter.

figure h

4.2 Transport Layer

The main role of transport layer is to establish and terminate connection trough source and destination ports of corresponding nodes. Ports are used to distinguish between applications on the same node. In addition to that, the transport layer is responsible to guaranty deliverance of segments that is noted DATA basing on sequence numbers n_Seq and their acknowledgment noted Ack. In order to well understand what happen in the transport layer between a pair of sensor nodes, it is written as two algorithms, one for each side like it is shown in Fig. 6.

Fig. 6
figure 6

Sender and receiver algorithms in transport layer

Full size image

The CPN of Fig. 7 models this principle by detailing states and actions to do according to some conditions by the sender and the receiver nodes as well as intermediate nodes of network.

Fig. 7
figure 7

CPN model for transport layer

Full size image

To establish the corresponding event-B model, the transport layer mechanism is split into two operations:

  1. 1.

    Signalization: to transmit data in the transport layer, the sender must verify that destination node and port exist really in the network, and then it must follow deliverance of messages by acknowledgment.

  2. 2.

    Data: it is the proper action of data transmission when conditions verified in the signalization step are favorable.

For the signalization part, the following context is proposed as static part coded in Rodin by:

figure i

It is clear from the previous context named context_transport that the transport layer has need to information sent by the application layer. It is the EXTENDS closure which allows to implement this principle in event-B. Indeed, the encapsulation mechanism in a network consists to pass data and parameters from a layer to the inferior one. In addition to the application context, the transport layer uses other parameters integrated by the SETS closure essentially the PORT and TYPE_MSG variables representing respectively the number of port and the message type used to send or receive data. The machine part of this model is shown in Fig. 8.

Fig. 8
figure 8

Event-B machine for signalization in transport layer

Full size image

As explained previously, the operation of signalization in the transport layer is based on some variables and invariants which are mainly syn, fin and ack included in the TYPE_MSG set and representing messages used for opening, closing and acknowledging a message respectively. Other variables are port_source for source port, port_destination for destination port included in the PORT set and Time counter.

As initialization event, all these variables are set to the empty set and the value zero for the time variable. In event-B using Rodin, the signalization machine for the transport layer is coded as following:

figure j

Other events of this phase are generated every sending or receiving operation for the three types of messages. So, there is send_ACK and receive_ACK, send_SYN and receive_SYN, FIN_syn and FIN_ACK. For each event, there are some guards for verifying conditions such as the source and destination ports are different, the sequence number of acknowledgment and control like it is shown in the code of receiving an ACK message:

figure k

For the data transmission phase, the following event-B model is proposed:

As context for this part, two sets are needed, where the first one is TYPE_DATA used to specify the type of sent or received data for example scalar, image or video data. The second set is named DATA representing information to transmit. So, the appropriate context is shown below:

figure l

Then, the corresponding machine is represented in Fig. 9.

Fig. 9
figure 9

Event-B machine for data transmission in transport layer

Full size image

When reading variables and invariants parts of this model, the following elements can be removed:

  • Sent_data: included in the set TYPE_DATA and representing data transmitted by a node.

  • Rcv_data: included in the set TYPE_DATA and representing data received by a node.

  • Type_data: it can be scalar, image, video or all other kind of data which can be transmitted or received by sensor nodes.

  • Data: it is the proper information to be treated and transferred.

  • Segment : the complete segment structure.

  • Data_size : data size to transmit.

  • Source: included in the set PORT and representing the source port of data transport.

  • Destination: included in the set PORT and representing the destination port of data transport.

  • Time: it is the time counter.

  • N_seq: each message must have a sequence number to be differentiated from other messages. This number is important for the signalization phase too.

At the beginning, all these variables are initialized to the empty set, except Time and N_seq which are initialized to zero. In data transport, three events occur in the system: INITIALIZATION, send_DATA and receive_DATA. The first event is used in the beginning of operation as explained in the previous paragraph. The second event noted send_DATA is based on six guards for verifying logical conditions and calculating some parameters to send information by a node, like: source and destination ports are different; the node is in the sending mode and how to calculate N_seq from data and segment size. Actions to perform for this event are sending data and incrementing time counter. The third event noted receive_DATA is based on ports and mode verification as guards and receiving data then incrementing the time counter as actions. After combining all the previous events, the following model implemented in Rodin platform can be obtained:

figure m

4.3 Network Layer

It is known that the network layer is responsible to manage the packets routing operation. The main problem is to define routes or links between each pair of nodes. In this level, two sets named PACKET and LINKS are used as in the following context:

figure n

For the machine part of the network layer model, the used variables and invariants are described in Table 1.

Table 1 Variables for network layer model
Full size table

In the first time, all these variables are initialized to the empty set. That is modeled by the INITIALIZATION event for the corresponding machine. Other events are necessary to complete definition of the network layer operation. For managing links, ADD_LINK and DEL_LINK events are used to add and delete routes for a node. For managing packets, SEND, RECEIVE, FORWARD and LOSING events allow respectively to send, receive and forward a packet, the last one is used to trait situation of losing a packet. This is written in event-B as a machine like it is below:

figure o
figure p

4.4 MAC Layer

The main role of the MAC layer is to manage problems due to medium access. Indeed, in a WSN, nodes communicate through shared frequency radio channels which create many problems and affects energy consumption of nodes. There are many solutions for these problems as MAC protocols generally based on altering the state of each node between active or sleep state in addition to manage the way of planning activities of a node according of its neighbors activities that can being Transmit, Receive, Sleep or Idle. This mechanism allows avoiding signal collision. It is the same mechanism used by the IEEE 802.11 standard witch use a preamble frame to determine collision probability due to hidden terminal problem known in CSMA/CA mechanism.

Before transmitting data frames, this mechanism uses two control frames called RTS (for Request To Send) and CTS (for Clear To Send). The medium access time for each node is managed by an allocation vector called NAV (for Network Allocation Vector). This vector contains time counters calculated as function of other parameters like the Back off value which is the random time to wait before transmitting, the DIFS or Distributed Inter Frame Spacing value and the SIFS or Short Inter Frame Spacing value. This mechanism is explained in Fig. 10.

Fig. 10
figure 10

Time allocation principle in MAC layer (802.11)

Full size image

Then, the node state changing can be modeled by the state diagram shown in Fig. 11.

Fig. 11
figure 11

Node states diagram for MAC layer

Full size image

So, the detailed operation of the MAC layer is modeled by the CPN of Fig. 12.

Fig. 12
figure 12

CPN model for MAC layer

Full size image

To validate this model, an event-B model is used too in the Rodin platform. The corresponding context contains necessary sets to manage frames and time called TYPE_FRAME and PERIODE respectively like it is shown here:

figure q

For the machine part of MAC layer, lot of variables and their invariants are used to manage node states, time counters, energy consumption and frame exchange like it is shown in Table 2.

Table 2 Variables for MAC layer model
Full size table

The MAC layer machine model contains six events in terms of Rodin modeling. These events are INITIALIZATION, TRANSMIT_RTS, TRANSMIT_CTS, TRANSMIT_DATA, TRANSMIT_ACK and FIN. The first event concerns system initialization where it is important to set all numeric variables to zero and those of type set to the empty set. In the second event TRANSMIT_RTS shown after, any node that want to transmit data, it must send an RTS frame to ensure synchronization with other neighbors. In this event, it has to verify some guards where the most important are:

  • grd1 that means the node must be in the TRANSMITTING or IDLE mode;

  • grd2 that guaranties to avoid transmission where the value of NAV is zero, which means a risk of collision.

  • grd5 to ensure that available time is sufficient to transmit the frame according to its size, the band width and the synchronization time.

  • grd6 it is necessary to inform neighbors which will awake up that a transmission operation will happen for a time great than sleeping time.

Actions to perform in this event are preparing the RTS frame, computing SIFS value for ACK synchronization and updating energy value.

figure r

The same structure is used for the third event TRANSMIT_CTS but by replacing RTS frame by CTS one. Some other guards are added too, where the most important is to ensure that node can’t transmit a CTS frame before receiving an RTS one. For TRANSMIT_DATA event, node must verify that a CTS frame has been received. This constraint is added as a guard for this event. With the same manner and to transmit an ACK frame, node has to wait until receiving a DATA frame. This is a guard that is added to the TRANSMIT_ACK event. Finally, the event called FIN is used at the end of a transmission session between a pair of nodes. So, receiving an ACK is a condition for this event being a guard in the event-B model.

5 Discussion and Results

The proposed approach relies on proof-based methodology (Event-B); it follows the same method as the one performed on orchestration [45] where refinement and proof-based methods with Event-B have been used for building correct services compositions. Event system is designed from a proved structure. Following refinement steps ensures that the protocol designed from a Petri network (with CPN tools, V4.0.1) model is synchronizable and well formed. So, the iterative approach to check and verify protocols can be avoided. Based on refinement, it is also possible to guarantee that exchanged messages are in same order as specified by their architecture. That provides a rigorous method for the performance evaluation and protocol development for WSNs through theorem proving. All proprieties and events are introduced in Rodin platform version 3.4.0, after many refinement and correction of all syntax and semantic errors, the obtained model and generated results are illustrated in Figs. 13 and 14.

Fig. 13
figure 13

Rodin implementation for a WSN

Full size image
Fig. 14
figure 14

Illustration of Rodin generated results for MAC layer

Full size image

As indicated in previous sections, verification with CPN tools is also made in this work. At first, the state space is used to check proprieties of the Petri net model. The state space is also called occurrence graphs, reachability graphs or reachability trees [46]. The state space tool integrated with CPN Tools can compute the state space and save it as a report file. In order to enter the state space, it must verify the following conditions:

  • There is no syntax error in the network.

  • All transitions and places should have names.

  • Names are required to be unique and to be alphanumeric.

The generated text file contains a standard report providing information about statistics (size of state space and strongly connected components graph or SCC graph), boundedness properties (inter and multi-set bounds for place instances), liveness properties (dead marking, dead/live transition instance) and fairness properties (impartial/fair/just transition instances). The proposed approach focuses on two important layers to evaluate witch are Mac and transport layers.

5.1 MAC Layer

5.1.1 Behavioral Proprieties

Figure 15 shows the first part of the CPN Tools state space report for the CPN model shown in Fig. 12. This part provides some state space statistics specifying how large the state space is. For the protocol shown in Fig. 12, there are 8753 nodes and 52497 arcs. The construction of the state space took 71 s (on a standard PC (Intel I3 , 1GB RAM)). Statistics for the SCC graph are also specified. It has 8753 nodes and 52497 arcs, and was calculated in 1 second. The fact that there are equal nodes in the SCC graph with the state space implies that there are non-trivial SCCs and hence there is no cycle in the state space of protocol. This means that an infinite occurrence sequence does not exist and that the protocol will terminate properly.

Fig. 15
figure 15

CPN tools statistics for MAC layer

Full size image

5.1.2 Boundedness Properties

The boundedness properties indicates how many and which tokens a place may hold, when all reachable markings are considered. Figure 16 specifies the best upper and lower integer bounds. The best upper integer bound of a place measure the maximal number of tokens that can reside on that place in any reachable marking. The best upper integer bound of the place MAC_Count is 1, which means that there is at most one token on the place and that there exists a reachable marking where there is one token on MAC_RECEIVE. It is what would be expected.

Fig. 16
figure 16

Boundedness properties for MAC CPN model

Full size image

5.1.3 Liveness Properties

Figure 17 shows the state space report that indicates the liveness properties. The liveness properties inform us that there is a four dead marking, which have the nodes numbers 2, 3, 8744, 8754. A dead marking is a marking in which no binding elements are enabled. The fact that only 4 nodes are dead marking tells that the protocol as specified by the CPN model is partially correct, if execution terminates, the correct result will be obtained.

Fig. 17
figure 17

Liveness properties for MAC CPN model

Full size image

5.2 Transport Layer

5.2.1 Behavioral Proprieties

In Fig. 18, the state space of the CPN model shown in Fig. 7 is reported. There are 25303 nodes and 381927 arcs. The construction of the state space took 300 seconds (on a standard PC (Intel I3, 1GB RAM)). Statistics for the SCC graph are also specified. It has 13273 nodes and 31391 arcs, and was calculated in 8 second. It’s clear that there are less nodes in the SCC graph than in the state space, this implies that there are non-trivial SCCs and for this reason there are cycles in the state space of the protocol. This means that infinite occurrence sequences exist and that the protocol will not necessarily terminate.

Fig. 18
figure 18

CPN tools statistics for transport layer

Full size image

5.2.2 Boundedness Properties

Figure 19 illustrates the best upper and lower integer bounds. The best upper integer bound of a place measure the maximal number of tokens that can be on that place in any reachable marking. The best upper integer bound of the place TOP_A is 22, which means that there is at most 22 token on the place TOP_A and that there exists a reachable marking.

Fig. 19
figure 19

Boundedness properties for transport CPN model

Full size image

6 Conclusions

In this study, a formal method has been used and combined with Coloured Petri Network for WSN protocol stack verification. Event-B which is the formal method allows to model protocol layers and their proprieties, and Event-B invariants to check the protocol consistency. In addition, a coloured Petri network was developed for each layer. This last gives more rigorous verification and comprehension of a protocol stack.

It is clear that modeling and verifying liveness property of a protocol layers can add more guarantee regarding the validity of design. For future research in this field, it will be interesting to investigate modeling certain features of the protocol operation environment and their impact on its functionality.