Keywords

1 Introduction

Wireless Sensor Networks (WSN) have emerged as a key enabler technology for the development of the Internet of Things (IoT) paradigm [20, 24]. Deployed over a field of interest, smart sensor nodes collaborate together without any human interaction, in order to mainly achieve a monitoring or a tracking task. Such networks are covering limitless applications [28], including home automation, external environmental monitoring and object tracking, and hence integrating WSN technologies into the IoT context [12, 20].

Due to their restricted size, sensors are basically battery-powered and thus have very critical energy resources. Consider the example of a WSN deployed for forest fire detection, in which the sensor nodes are randomly distributed with a high density. The network should be able to ensure the monitoring of the whole forest area while being functional for a sufficiently long period. Since a wild fire occurs only occasionally, some sensor nodes can be intuitively deactivated to save the network energy. In this context, the k-set randomized scheduling [18] is a kind of scheduling approach, suitable for a wide range of WSN applications, which mainly consists in organizing a given set of nodes by randomly partitioning them into “k” subsets, which work alternatively.

Scheduling sensor nodes for lifetime management purposes is surely a simple and intuitive approach, however it is also crucial to not compromise on the monitoring of the area. For the same forest fire application, the deployed WSN should be also able to cover, i.e., monitor, the outbreak of fires occurring at any point of the area with a high probability. Nevertheless, the coverage performance is completely probabilistic. For instance, some fire outbreaks may not be effectively covered if no nodes are deployed around the fire because of the random node deployment, or the surrounding nodes are inactive, due to random scheduling. Missing fire intrusion, can have devastating consequences.

The performance of the randomized scheduling has been generally analyzed using paper-and-pencil based probabilistic technique [18, 25]. The reliability of the obtained analytical models is consolidated through simulation using the Monte Carlo method [19]. However, both paper-and-pencil proof and simulation methods cannot be regarded as completely accurate mainly due to the error proneness of the former and the in-exhaustive nature of the later.

Formal methods overcome the drawbacks of simulation by rigorously using mathematical techniques to validate the analytical model of the given system. Recently, formal methods have gained a growing interest in the context of analyzing wireless sensor networks to analyze their functional or quantitative correctness [3, 22, 29], but most of the existing work is focused on the validation of their functional aspects only. Nevertheless, rigorous performance evaluation of WSNs constitutes also an extremely challenging aspect.

In this paper, we are interested in providing an accurate performance analysis of WSN randomized scheduling based on the paper-and-pencil models proposed in [18, 26]. In earlier work [6, 7], we have presented a formalization of the k-set randomized scheduling algorithm and its coverage properties based on a probabilistic framework developed by Hasan [13] in the HOL theorem prover. While sufficient for analyzing the coverage aspects of the original WSN models [18, 26], this formalization falls short to reason about other performance aspects of the same algorithm [8], like the detection metrics. In fact, the foremost requirement for reasoning about these WSN aspects in a theorem prover is the availability of the higher-order-logic formalization of probability theory and continuous random variables. In this regard, Hurd’s [16] formalization of measure and probability theories is a pioneering work. Building upon this formalization, most of the commonly-used continuous random variables [14] have been formalized using the HOL theorem prover. However, this foundational formalization of probability theory only supports the whole universe as the probability space, which limits its scope in many aspects. In particular the inability to reason about multiple continuous random variables [14] is a major obstacle for modeling and analyzing detection and lifetime properties of WSNs [9]. More recent probability theory formalizations [15, 21], however, allow the use of any arbitrary probability space that is a subset of the universe and thus are more flexible than Hurd’s and Hasan’s formalizations of probability theory. Particularly, Mhamdi’s [21] probability theory formalization which is based on extended-real numbers (real numbers including \(\pm \infty \)), has been included in the HOL theorem prover and thus has been chosen for our work. Therefore, in this paper we propose to use the most recent probability theory developed by Mhamdi [21] in HOL to formally reason about the coverage properties of randomly-scheduled WSN, while emphasizing on the main lessons learned through this experience. The practical interest of the new developments is illustrated through the formal analysis of the asymptotic coverage behavior of a WSN based environmental surveillance framework.

The rest of this paper is organized as follows. We review some related work on the validation of WSNs in Sect. 2. In Sect. 3, we summarize the main requirements of this work. Section 4 provides the foundational probabilistic analysis of the coverage properties. We utilize these developments to formally verify a WSN-based monitoring framework for IoT applications in Sect. 5. Section 6 is devoted to discuss the main results of our work. We finally conclude the paper in Sect. 7.

2 Related Work

Theoretical analysis, also known as paper-and-pencil based probabilistic technique, has been widely used to validate randomized scheduling algorithms for WSN [18, 25, 26]. Such analysis consists in constructing a theoretical model where the required random variables are determined together with the associated performance metrics. Afterwards, a probabilistic based study is achieved. For validation purposes, simulation, using the Monte Carlo method [19], is finally done.

Traditional model checking technique [2] has been successfully used to validate various aspects in the WSN context. In [22], the formal analysis of the Optimal Geographical Density Control (OGDC) algorithm, which is a kind of randomized scheduling algorithm, is done. Several other prominent works reported on the use of model checking for the analysis of WSN protocols include [10, 30]. The main strength of all these methods is their formal models and automatic verification. However, they suffer from the common model checking related problem of state space explosion [2]. Hence, the analysis of the OGDC algorithm [22] has been restricted for WSN with up to 6 nodes in a region of 15 m \(\times \) 15 m. Furthermore, the work of [30] has pointed out over 1 million generated states for the analysis of a simple property. Furthermore, none of the previous works has provided reliable probabilistic modelling. For example, in [22], a random function, assumed to be ‘good’, has been used to model the probabilistic behavior.

To cope with these major problems, probabilistic model checking [23] has also been used for the probabilistic functional analysis of wireless systems. Probabilistic model checking allows to capture the probability modelling for both the system and the property of interest. The probabilistic model checker PRISM has been applied quite frequently for the validation of Medium Access Control (MAC) protocols for WSNs [11, 29]. Nevertheless, the reasoning support for statistical quantities in most of model checkers suffers from many shortcomings. Indeed, expected performance values are usually obtained through several runs on the built model [29]. The obtained results can hardly be termed as exhaustive and thus formally verified.

On the other hand, very few works based on theorem proving exist in the open literature. The work [4] reports on the use of the PVS system to build a theorem proving based framework for WSN algorithms, with some theories expressing dynamic scenarios like nodes mobility and link quality changes [4]. While the PVS framework is supposed to be extended with some “dynamic” scenarios in [4], the randomness aspect has been characterized by a pseudo-random generator. The nodes mobility, specified by the random walk pattern, has been also specified through a recursive function.

Unlike the PVS framework which is limited by the probability support of the PVS system, the work, described in this paper, provides very accurate formalizations of the randomized scheduling algorithm based on the sound probability support of the HOL theorem prover. In addition, the presented formalizations are generic and completely valid for all the parameter values.

3 Preliminaries

3.1 Probabilistic Analysis in HOL

A probability measure P is basically a measure function on the sample space \(\varOmega \) and an event is a measurable set within the set F of events which are subsets of \(\varOmega \). By definition, a random variable is a measurable function, satisfying the condition that the inverse image of a measurable set is also measurable [21].

Definition 1

figure a

where X designates the random variable, p is a given probability space, NegInf and PosInf are the higher-order-logic formalizations of negative infinity or positive infinity, and Borel is the HOL definition of the Borel sigma algebra.

The probability distribution of a random variable is specified as the function that accepts a random variable X and a set s and returns the probability of the event {X \(\in \) s}.

Definition 2

figure b

In the discrete case, the expectation of the random variable X has been formalized in HOL as follows.

Theorem 1

figure c

where (IMAGE X (p_space p)) designates the list of values taken by the random variable X over the sample space (p_space p).

3.2 The k-set Randomized Scheduling Algorithm

During the initialization stage, the k-set randomized scheduling is run in parallel on every node as follows [18]. Each node starts by randomly picking a number, denoted by i, ranging from 0 to \((k-1)\), where k is the number of subsets or partitions. A node \(s_j\) is thus assigned to the \(i^{th}\) sub-network, designated by \(S_i\), and will activate itself only during the scheduling round of that subset. At the end of the algorithm, k disjoint sub-networks are created. These subsets will be working independently and alternatively. Figure 1 shows a small WSN of eight sensor nodes, which is randomly portioned into two sub-networks; \(S_0\) and \(S_1\). Each node randomly chooses a number 0 or 1 in order to be assigned to one of these two sub-networks. Suppose that nodes 0; 2; 5, randomly choose the number 0 and thus join the subset \(S_0\), whereas nodes 1; 3; 4; 6; 7, select the number 1 and will be in the subset \(S_1\). These two sub-networks will work by rounds, i.e., once the nodes 1; 3; 4; 6; 7, illustrated by the dashed circles, will be active, the remaining nodes 0; 2; 5, will be at the sleep state, and vice-versa.

Fig. 1.
figure 1

The k-set randomized scheduling for (\(n=8\)) nodes and (\(k=2\)) subsets.

Full size image

4 Formalization of the Network Coverage Intensity

Within a wireless sensor network, a given point is said to be covered, if any occurring event at this point, is detected by at least one active node with a given probability. According to [18], the coverage intensity of a specific point; \(C_p\), inside the monitored area is defined as the average time during which the point is covered in a whole scheduling cycle of length \(k \times T\). A given point is covered if the current active subset contains at least one node, i.e., is not empty.

Let X be the random variable describing the total number of non-empty subsets, the coverage intensity of a given point in the monitored area, \(C_p\), as originally specified in [18], is

$$\begin{aligned} C_p = \frac{{E[X] \times T}}{{k \times T}}. \end{aligned}$$
(1)

where E[X] denotes the expectation of X, which is described as:

$$\begin{aligned} X = \sum \limits _{j = 0}^{k - 1} {X_j}. \end{aligned}$$
(2)

where \(X_j\) is the Bernoulli random variable whose value is 1 in case of non-empty subset. A non-empty sub-network is described by a Bernoulli random variable with the complement probability of \(\mathtt {\left( 1-\frac{1}{k}\right) ^c}\) [6], where c is the number of covering sensors for a given point.

Definition 3

figure d

In higher-order logic, we model the coverage behavior of a specific point (Eq. (1)) by the following predicate cvrge_intsty_pt.

Definition 4

figure e

where X: a random variable that returns an extended real number, p: the probability space, k: the number of sub-networks, s: the summation set whose cardinality is k, and c: the number of covering sensors for a given point. The operator & allows the conversion of the natural number m into its extended number counterpart.

The following mathematical expression for the coverage intensity of a point has been formally verified in Theorem 2.

Theorem 2

figure f

  • The assumption ( \(\forall \) i. i \(\in \) s \(\Rightarrow \) sbst_non_empty_rv (X i) p k c) indicates that every element of the set s is a random variable sbst_non_empty_rv (Definition 3).

  • The HOL function Normal is used to convert a real value to its corresponding value in an extended real.

The proof of the above theorem is mainly based on lemmas about the linearity of the expectation property, which in turn required some reasoning on the integrability of some functions as well as operations from the Lebesgue theory. For most of these lemmas, it was a prerequisite to verify the measurability of the used events, along with some analysis on extended reals.

The whole network can be now statistically described by a single performance metric; \(C_n\), which is the average or the expectation value of the coverage intensity over all points of the monitored area.

$$\begin{aligned} C_n = E[C_p]. \end{aligned}$$
(3)

According to the expression of \(C_p\), shown in Theorem 2, we can write

$$\begin{aligned} C_n = E[1- \left( 1-\frac{1}{k}\right) ^c]. \end{aligned}$$
(4)

Based on the above equation, we notice how the value of \(C_n\) depends mainly on c which is the number of nodes covering a given point of the field. Intuitively, we can assimilate the fact of covering a point or not to a Bernoulli trial with the probability \(q=\frac{r}{a}\) [18]. Considering the variable c among the n nodes of the network, it becomes a Binomial random variable (C) with the probability given in Eq. (5). Thereby, the network coverage intensity \(C_n\), shown in Eq. (4), is not a simple expectation, but rather an expectation of a function of a random variable.

$$\begin{aligned} Pr (C = j) = C_{n}^{j}\times {\left( \frac{r}{a} \right) ^j}\times {\left( 1 - \left( \frac{r}{a} \right) \right) ^{n - j}}. \end{aligned}$$
(5)

where \(C_{n}^{j}\) is the binomial coefficient, r is the size of the sensing area of each sensor, a is the size of the monitored area, and \(\left( \frac{r}{a} \right) \) is the probability that each sensor covers a given point. The Binomial random variable with n trials and success probability \(q = \left( \frac{r}{a} \right) \) has been formalized in HOL as follows.

Definition 5

figure g

where X is a real random variable on the probability space p, and IMAGE( \(\lambda \) x.& x) (count (SUC n)) gives the support of the Binomial. The function binomial, used in the above definition, is the higher-order-logic formalization of the binomial coefficient for reals.

The coverage intensity of the whole WSN with n nodes has been formally specified by the function cvrge_intsty_network, shown in Definition 6. The latter takes as parameters: X: a random variable that returns an extended real number, p: the probability space, s: the summation set used in Definition 4, k: the number of sub-networks, C: the random variable describing the number of covering nodes, n: the total number of nodes, and q: the probability that each sensor covers a given point.

Definition 6

figure h

where the function expectation designates the higher-order-logic formalization of the expectation of a random variable that returns an extended real, and the values (num(C x)), in the above definition, are the output values of the random variable C. The function num, used here, converts an extended real; (&m), to its corresponding natural value m, using the real function floor.

Based on the higher-order-logic formalizations developed so far, we have been able to formally verify the final network coverage intensity as in Theorem 3.

Theorem 3

figure i

  • The assumption (events p = POW (p_space p)) describes the set of events to be the power set of the sample space \(\varOmega \).

  • The assumptions (1 \(\le \) n) ensures that the WSN include at least one node, while (0 < q < 1) checks that the probability q lies in [0..1].

  • sn_covers_p is the Binomial random variable (Definition 5) with a finite expectation, i.e., (expectation p C \(\ne \) PosInf) \(\wedge \) (expectation p C \(\ne \) NegInf). The variables (PosInf) and (NegInf) are the higher-order-logic formalizations of positive infinity and negative infinity, respectively.

  • The function (sbst_non_empty_rv (X i) p k (num(C x))) is the function specified in Definition 3.

The proof of Theorem 3 is primarily based on Theorem 4 which verifies the expectation of a function of a random variable. Additionally, the current proof also required the application of the linearity of the expectation property. Finally, a considerable amount of real analysis associated to the Binomial theorem for reals, and to the summation function has been needed.

Theorem 4

figure j

where the function f_fct is defined as follows

$$\begin{aligned} \mathtt {f\_fct\,x\,k = Normal\left( 1 - \frac{1}{k}\right) ^x}. \end{aligned}$$
(6)

The proof of Theorem 4 has been possible using intermediate results on the injectivity of some functions, as well as, some properties related to the random variables functions. A lot of reasoning associated with the use of extended real and the floor function, has also been required.

In this section, we presented our new higher-order-logic formalizations of the k-set randomized scheduling for wireless sensor networks, using the recently developed probability theory available in the HOL theorem prover [21]. These formalizations have been then utilized to formally reason about the coverage performance properties. The corresponding HOL code of the current formalizations is available at [5]. Due to fundamental differences in the foundations of the two probability theories in [13, 21], the current resulting formalizations is completely different from the previous one [6]. Indeed, the new probability theory allows to cater for arbitrary probability spaces and is thus more generic and complete compared to the previous formalization in which the probability space has to be the universe of a set. Moreover, the specification of the randomized algorithm has been found to be much more intuitive with [21]. Unlike the work in [6], the developed proofs required much less reasoning about sets and lists producing thus less lengthy proofs. However, these proofs have been more laboured involving usually results from the three HOL theories: Lebesgue, measure and extended reals. A deep learning of all theoretical foundations of [21] was thus required to successfully achieve the target formalizations in the HOL theorem prover. In the next section, we will illustrate how the developed generic theorems extremely facilitate the formal analysis of real-world WSN applications.

5 Application: Formal Analysis of a WSN-based Monitoring Framework for IoT Applications

Numerous frameworks for environmental monitoring based on WSN have been hence proposed in the literature [1, 27]. These systems can be seamlessly integrated to build an extended IoT framework for low-cost, persistent and efficient services [12, 17]. Due to the new constraints of the IoT environment, deployed WSN should have a smart behavior regarding the power availability while performing a good coverage of any intrusion. The randomized node scheduling has been proposed for use to save energy in the context of an heterogeneous surveillance framework for environmental monitoring [27]. Such framework considers collaboration between sensor nodes, mobile robots and RFID tags, to ensure efficient surveillance. Using specific sensors designed for IoT [17], this framework can realize a whole IoT structure.

In this section, we focus on formally analyzing the coverage performances of the hybrid surveillance framework proposed in [27] adopted for IoT applications. The nodes can hence have any sensing area r, and are deployed into a circular region of a radius R with a total size of a, whereas the success probability q of a sensor covering a point is \(q = \frac{r}{a}\). Such framework has been primarily analyzed using a paper-and-pencil model, which has been then validated through some simulation scenarios evaluating the expected coverage and the maximum number of subsets [27]. It would be interesting to provide a more rigorous technique to validate the proposed paper-and-pencil model. Based on the formal development achieved so far, we show in this section how we are able to carry out an accurate asymptotic analysis of the probabilistic coverage according to the key design parameters: n; the total number of sensor and k; the number of subsets.

We designate the generic network coverage intensity (cvrge_intsty_network p X s k C n q), shown in Definition 6, by (Cn_wsn p X s k C n q), that has been checked in HOL as

$$\begin{aligned} \mathtt {Normal\left( 1 - \left( 1 - \frac{q}{k}\right) ^n\right) }. \end{aligned}$$
(7)

5.1 Formal Analysis Based on the Number of Nodes

Setting the number of subsets to k and targeting a network coverage intensity \(C{n\_wsn}\) of at least t, we verify, in Lemma 1, the minimum number of sensors; \(n_{min}\), that are necessary to deploy in the context of our monitoring framework.

Lemma 1

figure k

The higher-order-logic proof of the above lemma is based on some properties of transcendental functions and arithmetic reasoning.

We have been able to formally verify, in Lemma 2, that the network coverage intensity \(C{n\_wsn}\) is a growing function of n, i.e., a larger node number n is responding to a better coverage. For the monitoring framework, much more points of the area are expected to be covered, since it is likely that many more covering nodes are deployed in its surrounding area.

Lemma 2

figure l

where the function real is used to convert the network coverage intensity of type extended real to its corresponding real value, and mono_incr is the HOL definition of an increasing sequence.

While \(C{n\_wsn}\) increases with the increase of the number of nodes n, as verified in Lemma 2, the next lemma shows how the network coverage intensity \(C{n\_wsn}\) approaches 100% when n becomes infinite, independently of the monitoring application.

Lemma 3

figure m

5.2 Formal Analysis Based on the Number of Subsets

Targeting a network coverage intensity of at least t, we successfully verify, in Lemma 4, the upper bound on the number of disjoint subsets k for a given n.

Lemma 4

figure n

The above result is interesting for practical WSN applications which necessitate adjustable performance measurement quality for energy preserving purposes.

We have been able to formally check, in Lemma 5, that the network coverage intensity \(Cn\_wsn\) definitely decreases when the WSN is partitioned into a quite large number of sub-networks k.

Lemma 5

figure o

where the HOL function mono_decr defines a decreasing sequence.

We also formally confirm, in Lemma 6, that increasing the number of deployed nodes n gives smaller network coverage and hence a poor performance of the deployed application.

Lemma 6

figure p

The above lemma has been successfully verified in HOL using intermediate results associated to real and sequential limits.

5.3 Formal Analysis Based on Uniform Partitions

We closely investigate the asymptotic coverage behavior of our monitoring framework in the case of a uniform split of the nodes. Here, n can be written as \(k \times m\), where m is the number of nodes per subset.

In particular, as the number of sub-networks k goes infinite, the upper limit of the network coverage \(Cn\_wsn\) has been formally verified in Lemma 7.

Lemma 7

figure q

The proof of the above lemma has been quite tricky requiring the important result \(\mathtt {\lim \limits _{k\rightarrow +\infty }(1 + \frac{x}{k})^k = e^{x}}\), which had to be proved in HOL beforehand.

Based on Lemma 7, we can hence verify that when m becomes very large, the uniform network coverage will surely approach \(100\%\). Such result is considered as a second verification of Lemma 3 in the case where n and k are proportional.

Lemma 8

figure r

The current analysis, presented in this section, distinctly shows how our theoretical developments, described in Sect. 4, match pretty well the original paper-and-pencil models of the randomized scheduling, available in the open literature [18, 26].

6 Discussion

The main motivation of the current work is to provide a rigorous approach for the probabilistic performance evaluation of the k-set randomized scheduling algorithm for wireless sensor networks. The randomness in the scheduling approach and the node deployment makes the accuracy of the performance evaluation of such algorithm very critical, especially given the major limitations of classical techniques and the safety-critical of most WSN applications. In this regard, this paper describes the main formalizations of the k-set randomized scheduling and its coverage properties using the new probability theory available within the HOL4 theorem prover [21]. These higher-order-logic formalizations resulted from the porting process of our previous formalizations [6, 7], developed within a precedent probabilistic framework of the HOL theorem prover [13]. The practical usefulness of our approach is shown in Sect. 5, where we formally analyzed the coverage performance of a general purpose surveillance framework based on WSN for IoT applications.

The higher-order-logic formalizations, presented in this paper, consumed approximatively 730 lines of code in the HOL4 theorem prover. On the other hand, the formal analysis of our application took only 200 lines of HOL code for the verification of most of the lemmas. Nevertheless, the proofs of Lemmas 7 and 8 have been quite tedious consuming in total 500 lines of HOL code, since the mathematical theorem \(\mathtt {\lim \limits _{k\rightarrow +\infty } (1 + \frac{x}{k})^k = e^{x}}\), was missing in HOL. The latter result required a lot of real analysis related to the exponential function as a power series and many other properties for the sequence convergence.

The generic nature of the theorem proving technique and the high expressibility of higher-order logic allows us a considerable amount of flexibility in several aspects. Indeed, the formalizations, presented in this paper, primarily constitutes a successful automation of the paper-and-pencil models [18, 26] of the k-set randomized scheduling and its coverage performance within a higher-order-logic proof assistant. Through this work, we therefore clearly assert the complete accordance of the resulting formal developments with the mathematical models, increasing thus the confidence on the developed theory. Given the discussion, presented in Sect. 2, it is certain that other analysis techniques can never have this efficiency. Actually, the existing probabilistic models of the randomized scheduling are not so reliable either regarding the complete set of assumptions or the correctness of the manual mathematical analysis, which may include human errors. In addition, while previous simulation methods usually rely on pseudo-random modelling, we have been able to provide an appropriate modelling of the inherent randomness of the algorithm of interest. Besides, unlike probabilistic model checkers where statistical properties are not so accurately specified, we have been able to achieve formal and precise analysis of the network coverage as a statistical measure of the coverage intensity for a specific point. On the other hand, the formal performance analysis of the coverage behavior of the environmental framework clearly shows the usefulness of our theoretical developments. Such verification enables reliable asymptotic reasoning of the deployed WSN. Compared to the asymptotic analysis already done in [7], we have been able to enrich our analysis with new valuable results. At the end, it is important to note that the presented application is a simple case study illustrating the practical interest of our work, but the claimed generic results can be obviously applied to any other WSN application as well.

To successfully achieve the current work, we have experienced many difficulties. Firstly, although the initial paper-and-pencil models [18, 26] are depending on simple discrete random variables, the major challenge was to correctly translate these models of a real WSN algorithm into higher-order logic. These analytical modelling of real-world systems is effectively very intuitive, and the original mathematical models [18, 26] are usually missing detailed explanations either when describing the probabilistic analysis or when applying the probability rules. In addition, the assumptions of the original model are never presented exhaustively. A deep investigation step was thus required in order to correctly understand all missing steps and achieve then efficiently the target higher-order-logic formalizations. For that purposes, a good background on probability coupled with a sound knowledge of the WSN context, are usually required for an effective understanding of the probabilistic reasoning.

Secondly, the choice of porting our previous higher-order-logic formalizations [6, 7] into a new probability theory [21], was, at once, tough and time consuming. As previously mentioned, such choice has been primarily motivated by the fact that we were targeting more evolutive probabilistic analysis of the k-set randomized scheduling with the formalization of further performance aspects in the near future [8]. These aspects should require some probabilistic features which are not available in [13]. Moreover, while the new HOL specification seems to be more straightforward in the new probability theory, we had to get extensive understanding of all the corresponding mathematical foundations including extended reals, measure and Lebesgue theories in order to correctly conduct the probabilistic analysis. Nevertheless, the existing results from the formalized probability theory helped us to keep the amount of proof efforts reasonable.

7 Conclusions

In this paper, we presented a reliable approach for the formal analysis of the coverage performances of wireless sensor networks using the k-set randomized scheduling to save energy. This formalization enables us to formally verify the coverage related characteristics of most WSNs using the k-set randomized scheduling. To show the practical interest of our foundational results, we apply them to perform the formal probabilistic analysis of an hybrid monitoring framework for environmental Internet of Things (IoT) applications. Such framework can be adapted for any kind of monitoring application using WSN as well.

On the other hand, the produced results are thoroughly generic, i.e., valid for all parameter values. It is clear that such results cannot be achieved in simulation or probabilistic model checking based approach. Moreover, it has been possible to provide precise formal reasoning on the statistical coverage using expectation. Finally, unlike most of the existing work that focuses on the validation of the functional aspects of WSN algorithms, our work is distinguishable by addressing the performance aspects. Finally, the proposed solution allowed us to build upon our coverage formalizations to develop our whole methodology [8] in a single coherent formalism. In particular, the current results have been very helpful for our work on the higher-order-logic formalizations of the detection properties of WSNs [9], based on the paper-and-pencil analysis of [26]. It has been useful to formally check the relationship between coverage and detection showing that coverage reflects detection [18].