Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks

In the context of Wireless Sensor Networks (WSNs), the ability to detect an intrusion event is the most desired characteristic. Due to the randomness in nodes scheduling algorithm and sensor deployment, probabilistic techniques are used to analyze the detection properties of WSNs. However, traditional probabilistic analysis techniques, such as simulation and model checking, do not ensure accurate results, which is a severe limitation considering the mission-critical nature of most of the WSNs. In this chapter, the authors overcome these limitations by using higher-order-logic theorem proving to formally analyze the detection properties of randomly deployed WSNs using the randomized scheduling of nodes. Based on the probability theory, described in Chapters 5, they first formally reason about the intrusion period of any occurring event. This characteristic is then built upon to develop the fundamental formalizations of the key detection metrics: the detection probability and the detection delay. For illustration purposes, the authors formally analyze the detection performance of a WSN deployed for border security monitoring.

Applications of Formalized Information Theory

In previous chapters, the authors provided a comprehensive framework that can be used in the formal probabilistic and information-theoretic analysis of a wide range of systems and protocols. In this chapter, they illustrate the usefulness of conducting this analysis using theorem proving by tackling a number of applications including a data compression application, the formal analysis of an anonymity-based MIX channel, and the properties of the onetime pad encryption system.

Classified Discrete-Time Markov Chains

The main focus of this chapter is on the formalization of classified DTMCs. The chapter begins by presenting the formalization of some foundational notions of classified states, which are categorized based on reachability, periodicity, or absorbing features. Then, these results along with the formal definition of a DTMC, presented in the previous chapter, are used to formalize classified Markov chains, such as aperiodic and irreducible DTMCs. Based on these concepts, some long-term properties are verified for the purpose of formally checking the correctness of the functions of Markovian systems or analyzing the performance of Markov chain models.

Probabilistic Analysis Using Theorem Proving

In this chapter, the authors first provide the overall methodology for the theorem proving formal probabilistic analysis followed by a brief introduction to the HOL4 theorem prover. The main focus of this book is to provide a comprehensive framework for formal probabilistic analysis as an alternative to less accurate techniques like simulation and paper-and-pencil methods and to other less scalable techniques like probabilistic model checking. For this purpose, the HOL4 theorem prover, which is a widely used higher-order-logic theorem prover, is used. The main reasons for this choice include the availability of foundational probabilistic analysis formalizations in HOL4 along with a very comprehensive support for real and set theoretic reasoning.

Probabilistic Analysis

This chapter provides the motivations behind the usage of probabilistic analysis in the domains of science and engineering. This is followed by a brief introduction of some of the foremost concepts of probabilistic analysis and the widely used probabilistic analysis techniques. The chapter concludes by highlighting some of the limitations of the traditional probabilistic analysis techniques.

Discrete-Time Markov Chains in HOL

In this chapter, the authors describe the formalization of discrete-time Markov chains and the formal verification of some of its most important properties using the probability theory presented in the last chapter. In order to illustrate the usefulness of this work, a binary communication channel model and a collection process model involved in the Automatic Mail Quality Measurement (AMQM) protocol are formally analyzed in HOL.

Scheduling Algorithm for Wireless Sensor Networks

In Wireless Sensor Networks (WSNs), scheduling of the sensors is considered to be the most effective energy conservation mechanism. The random and unpredictable deployment of sensors in many WSNs in open fields makes the sensor-scheduling problem very challenging and thus randomized scheduling algorithms are used. The performance of these algorithms is usually analyzed using simulation techniques, which do not offer 100% accurate results. Moreover, probabilistic model checking, when used, does not include a strong support to reason accurately about statistical quantities like expectation and variance. In this chapter, the authors overcome these limitations by using higher-order-logic theorem proving to formally analyze the coverage-based random scheduling algorithm for WSNs. Using the probability theory formalization, described in Chapter 5, the authors formally reason about the probability of some events that are interesting in the context of WSN coverage.

Probability Theory

In this chapter, the authors make use of the formalizations of measure theory and Lebesgue integration in HOL4 to provide a higher-order-logic formalization of probability theory (Mhamdi, 2013). For illustration purposes, they also present the probabilistic analysis of the Heavy Hitter problem using HOL.

Measure Theory and Lebesgue Integration Theories

As discussed in the previous chapter, the fundamental theories of measure and Lebesgue integration are the prerequisites for the formalization of probability theory in higher-order logic. The scope of this chapter is primarily the formalization of these foundations. Both formalizations of measure theory and Lebesgue integral (Mhamdi, Hasan, & Tahar, 2011), presented in this chapter, are based on the extended-real numbers. This allows us to define sigma-finite and even infinite measures and handle extended-real-valued measurable functions. It also allows us to verify the properties of the Lebesgue integral and its convergence theorems for arbitrary functions. Therefore, the chapter begins with a description of the formalization of extended real numbers.

Information Measures

This chapter presents a higher-order-logic formalization of the main concepts of information theory (Cover & Thomas, 1991), such as the Shannon entropy and mutual information, using the formalization of the foundational theories of measure, Lebesgue integration, and probability. The main results of the chapter include the formalizations of the Radon-Nikodym derivative and the Kullback-Leibler (KL) divergence (Coble, 2010). The latter provides a unified framework based on which most of the commonly used measures of information can be defined. The chapter then provides the general definitions that are valid for both discrete and continuous cases and then proves the corresponding reduced expressions where the measures considered are absolutely continuous over finite spaces.