Search

Partial Differential Equations (PDEs) are widely used for modeling the physical phenomena and analyzing the dynamical behavior of many engineering and physical systems. The heat equation is one of the most well-known PDEs that captures the temperature distribution and diffusion of heat within a body. Due to the wider utility of these equations in various safety-critical applications, such as thermal protection systems, a formal analysis of the heat transfer is of utmost importance. In this paper, we propose to use higher-order-logic (HOL) theorem proving for formally analyzing the heat conduction problem in rectangular coordinates. In particular, we formally model the heat transfer as a one-dimensional heat equation for a rectangular slab using the multivariable calculus theories of the HOL Light theorem prover. This requires the formalization of the heat operator and formal verification of its various properties, such as linearity and scaling. Moreover, we use the separation of variables method for formally verifying the solution of the PDEs, which allows modeling the heat transfer in the slab under various initial and boundary conditions using HOL Light., Comment: 15th Conference on Intelligent Computer Mathematics

The Hadoop scheduler is a centerpiece of Hadoop, the leading processing framework for data-intensive applications in the cloud. Given the impact of failures on the performance of applications running on Hadoop, testing and verifying the performance of the Hadoop scheduler is critical. Existing approaches such as performance simulation and analytical modeling are inadequate because they are not able to ascertain a complete verification of a Hadoop scheduler. This is due to the wide range of constraints and aspects involved in Hadoop. In this paper, we propose a novel methodology that integrates and combines simulation and model checking techniques to perform a formal verification of Hadoop schedulers, focusing on the following properties: schedulability, fairness and resources-deadlock freeness. We use the CSP language to formally describe a Hadoop scheduler, and the PAT model checker to verify its properties. Next, we use the proposed formal model to analyze the scheduler of OpenCloud, a Hadoop-based cluster that simulates the Hadoop load, in order to illustrate the usability and benefits of our work. Results show that our proposed methodology can help identify several tasks failures (up to 78%) early on, i.e., before the tasks are executed on the cluster., Comment: In Proceedings SCSS 2021, arXiv:2109.02501

Stochastic computing allows a drastic reduction in hardware complexity using serial processing of bit streams. While the induced high computing latency can be overcome using integrated optics technology, the design of realistic optical stochastic computing architectures calls for energy efficient switching devices. Photonics Crystal (PhC) nanocavities are $\mu m^2$ scale devices offering 100fJ switching operation under picoseconds-scale switching speed. Fabrication process allows controlling the Quality factor of each nanocavity resonance, leading to opportunities to implement architectures involving cascaded gates and multi-wavelength signaling. In this report, we investigate the design of cascaded gates architecture using nanocavities in the context of stochastic computing. We propose a transmission model considering key nanocavity device parameters, such as Quality factors, resonance wavelength and switching efficiency. The model is calibrated with experimental measurements. We propose the design of XOR gate and multiplexer. We illustrate the use of the gates to design an edge detection filter. System-level exploration of laser power, bit-stream length and bit-error rate is carried out for the processing of gray-scale images. The results show that the proposed architecture leads to 8.5nJ/pixel energy consumption and 512ns/pixel processing time.

Cause-consequence Diagram (CCD) is widely used as a deductive safety analysis technique for decision-making at the critical-system design stage. This approach models the causes of subsystem failures in a highly-critical system and their potential consequences using Fault Tree (FT) and Event Tree (ET) methods, which are well-known dependability modeling techniques. Paper-and-pencil-based approaches and simulation tools, such as the Monte-Carlo approach, are commonly used to carry out CCD analysis, but lack the ability to rigorously verify essential system reliability properties. In this work, we propose to use formal techniques based on theorem proving for the formal modeling and step-analysis of CCDs to overcome the inaccuracies of the simulation-based analysis and the error-proneness of informal reasoning by mathematical proofs. In particular, we use the HOL4 theorem prover, which is a computer-based mathematical reasoning tool. To this end, we developed a formalization of CCDs in Higher-Order Logic (HOL), based on the algebraic approach, using HOL4. We demonstrate the practical effectiveness of the proposed CCD formalization by performing the formal reliability analysis of the IEEE 39-bus electrical power network. Also, we formally determine the Forced Outage Rate (FOR) of the power generation units and the network reliability index, i.e., System Average Interruption Duration Index (SAIDI). To assess the accuracy of our proposed approach, we compare our results with those obtained with MATLAB Monte-Carlo Simulation (MCS) as well as other state-of-the-art approaches for subsystem-level reliability analysis., Comment: 41 pages, 17 figures, 8 tables

Event Tree (ET) analysis is a widely used forward deductive safety analysis technique for decision-making at a system design stage. Existing ET tools usually provide Graphical Users Interfaces (GUI) for users to manually draw system-level ET diagrams, which consist of nodes and branches, describing all possible success and failure scenarios. However, these tools do not include some important ET analysis steps, e.g., the automatic generation and reduction of a complete system ET diagram. In this paper, we present a new Event Trees Modeling and Analysis (ETMA) tool to facilitate users to conduct a complete ET analysis of a given system. Some key features of ETMA include: (i) automatic construction of a complete ET model of real-world systems; (ii) deletion/reduction of unnecessary ET nodes and branches; (iii) partitioning of ET paths; and (iv) probabilistic analysis of the occurrence of a certain event. For illustration purposes, we utilize our ETMA tool to conduct the ET analysis of a protective fault trip circuit in power grid transmission lines. We also compared the ETMA results with Isograph, which is a well-known commercial tool for ET analysis., Comment: 21 pages, 10 figures, 4 tables, The 14th Annual IEEE International Systems Conference (SYSCON 2020)

Event Tree (ET) analysis is widely used as a forward deductive safety analysis technique for decision-making at the critical-system design stage. ET is a schematic diagram representing all possible operating states and external events in a system so that one of these possible scenarios can occur. In this report, we propose to use the HOL4 theorem prover for the formal modeling and step-analysis of ET diagrams. To this end, we developed a formalization of ETs in higher-order logic, which is based on a generic list datatype that can: (i) construct an arbitrary level of ET diagrams; (ii) reduce the irrelevant ET branches; (iii) partition ET paths; and (iv) perform the probabilistic analysis based on the occurrence of certain events. For illustration purposes, we conduct the formal ET stepwise analysis of an electrical power grid and also determine its System Average Interruption Frequency Index (SAIFI), which is an important indicator for system reliability., Comment: 17 pages, 3 figures

Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several electronic, communication and controller modules and some actuators and sensors. The mix of heterogeneous underlying smart technologies poses a number of technical challenges to the design and more severely to the verification of such complex infrastructure. In fact, a CPS shall adhere to strict safety, reliability, performance and security requirements, where one needs to capture both physical and random aspects of the various CPS modules and then analyze their interrelationship across interlinked continuous and discrete dynamics. Often times however, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety-critical applications. In this paper, we introduce some of the challenges surrounding the design and verification of contemporary CPS with the advent of smart technologies. In particular, we survey recent developments in the use of theorem proving, a formal method, for the modeling, analysis and verification of CPS, and overview some real world CPS case studies from the automotive, avionics and healthtech domains from system level to physical components., Comment: 15 Pages, Seventh International Workshop on Formal Techniques for Safety-Critical Systems, Shenzhen, China

Dedicated hardware accelerators are suitable for parallel computational tasks. Moreover, they have the tendency to accept inexact results. These hardware accelerators are extensively used in image processing and computer vision applications, e.g., to process the dense 3-D maps required for self-driving cars. Such error-tolerant hardware accelerators can be designed approximately for reduced power consumption and/or processing time. However, since for some inputs the output errors may reach unacceptable levels, the main challenge is to \textit{enhance the accuracy} of the results of approximate accelerators and keep the error magnitude within an allowed range. Towards this goal, in this paper, we propose a novel machine learning-based self-compensating approximate accelerators for energy efficient systems. The proposed error \textit{compensation module}, which is integrated within the architecture of approximate hardware accelerators, efficiently reduces the accumulated error at its output. It utilizes \textit{lightweight supervised machine learning techniques, i.e., decision tree}, to capture input dependency of the error. We consider image blending application in multiplication mode to demonstrate a practical application of self-compensating approximate computing. Simulation results show that the proposed design of self-compensating approximate accelerator can achieve about 9\% accuracy enhancement, with negligible overhead in other performance measures, i.e., power, area, delay and energy., Comment: This work has been accepted at the 14th Annual IEEE International Systems Conference which will be held April 20-23 at Montreal, Quebec, CANADA

Dynamic dependability models, such as dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs), are introduced to overcome the modeling limitations of traditional models. Recently, higher-order logic (HOL) formalizations of both models have been conducted, which allow the analysis of these models formally, within a theorem prover. In this report, we provide the formal dynamic dependability analysis of shuffle-exchange networks, which are multistage interconnection networks that are commonly used in multiprocessor systems. We use DFTs and DRBDs to model the terminal, broadcast and network reliability with dynamic spare gates and constructs in several generic versions. We verify generic expressions of probability of failure and reliability of these systems, which can be instantiated with any number of system components and failure rates to reason about the failure behavior of these networks.

Dynamic Fault Trees (DFT) and Dynamic Reliability Block Diagrams (DRBD) are two modeling approaches that capture the dynamic failure behavior of engineering systems for their reliability analysis. Recently, two independent higher-order logic (HOL) formalizations of DFT and DRBD algebras have been developed in the HOL4 theorem prover. In this work, we propose to integrate these two modeling approaches for the efficient formal reliability analysis of complex systems by leveraging upon the advantages of each method. The soundness of this integration is provided through a formal proof of equivalence between the DFT and DRBD algebras. We show the efficiency of the proposed integrated formal reliability analysis on a drive-by-wire system as a case study.

Dynamic reliability block diagrams (DRBDs) are introduced to overcome the modeling limitations of traditional reliability block diagrams, such as the inability to capture redundant components. However, so far there is no algebraic framework that allows conducting the analysis of a given DRBD based on its structure function and enables verifying its soundness using higher-order logic (HOL) theorem proving. In this work, we propose a new algebra to formally express the structure function and the reliability of a DRBD with spare constructs based on basic system blocks and newly introduced DRBD operators. We present several simplification properties that allow reducing the structure of a given DRBD. We provide the HOL formalization of the proposed algebra, and formally verify its corresponding properties using the HOL4 theorem prover. This includes formally verifying generic reliability expressions of the spare construct, series, parallel and deeper structures in an extensible manner that allows verifying the reliability of complex systems. Finally, we demonstrate the applicability of this algebra by formally analyzing the terminal reliability analysis of a shuffle-exchange network in HOL4.

Approximate computing is a nascent energy-efficient computing paradigm suitable for error-tolerant applications. However, the value of approximation error depends on the applied inputs where individual output error may reach intolerable level while the average output error is acceptable. Thus, it is critical to show the response of approximate design for various applied inputs where understanding the interdependence between the inputs and the approximation error could be utilized to control the output quality. In this report, we exhaustively analyze the accuracy of 20 different designs of 8-bit approximate array multipliers. We designed these multipliers based on various configurations including the type of approximable component and how much of the result to approximate, i.e., approximation degree. Accuracy analysis shows a strong correlation between the applied inputs and the magnitude of the observed error, i.e., error distance, normalized error distance and peak-to-signal-noise ratio. We may utilize this input-dependency of approximation error, in controlling the quality of approximate computing by eliminating large magnitude errors and improving the quality of the final results.

Importance measures provide a systematic approach to scrutinize critical system components, which are extremely beneficial in making important decisions, such as prioritizing reliability improvement activities, identifying weak-links and effective usage of given resources. The importance measures are then in turn used to obtain a criticality value for each system component and to rank the components in descending manner. Simulations tools are generally used to perform importance measure based analysis, but they require expensive computations and thus they are not suitable for large systems. A more scalable approach is to utilize the importance measures to obtain all the necessary conditions by proving a generic relationship describing the relative importance between any pair of components in a system. In this paper, we propose to use higher-order-logic (HOL) theorem proving to verify such relationships and thus making sure that all the essential conditions are accompanied by the proven property. In particular, we formalize the commonly used importance measures, such as Birnbaum and Fussell-Vesely, and conduct a formal importance measure analysis of a railway signaling system at a Moroccan level crossing as an application for illustration purpose., Comment: 10 pages, 2 figures, International Conference on Formal Methods in Software Engineering (FormaliSE'19). arXiv admin note: text overlap with arXiv:1608.06392

Stochastic computing (SC) allows reducing hardware complexity and improving energy efficiency of error resilient applications. However, a main limitation of the computing paradigm is the low throughput induced by the intrinsic serial computing of bit-streams. In this paper, we address the implementation of SC in the optical domain, with the aim to improve the computation speed. We implement a generic optical architecture allowing the execution of polynomial functions. We propose design methods to explore the design space in order to optimize key metrics such as circuit robustness and power consumption. We show that a circuit implementing a 2 nd order polynomial degree function and operating at 1Ghz leads to 20.1pJ laser consumption per computed bit.

Dynamic Fault Trees (DFTs) is a widely used failure modeling technique that allows capturing the dynamic failure characteristics of systems in a very effective manner. Simulation and model checking have been traditionally used for the probabilistic analysis of DFTs. Simulation is usually based on sampling and thus its results are not guaranteed to be complete, whereas model checking employs computer arithmetic and numerical algorithms to compute the exact values of probabilities, which contain many round-off errors. Leveraging upon the expressive and sound nature of higher-order-logic (HOL) theorem proving, we propose, in this work, a formalization of DFT gates and their probabilistic behavior as well as some of their simplification properties in HOL. This formalization would allow us to conduct the probabilistic analysis of DFTs by verifying generic mathematical expressions about their behavior in HOL. In particular, we formalize the AND, OR, Priority-AND, Functional DEPendency, Hot SPare, Cold SPare and the Warm SPare gates and also verify their corresponding probabilistic expressions in HOL. Moreover, we formally verify an important property, Pr(X

Approximate multipliers are widely being advocated for energy-efficient computing in applications that exhibit an inherent tolerance to inaccuracy. However, the inclusion of accuracy as a key design parameter, besides the performance, area and power, makes the identification of the most suitable approximate multiplier quite challenging. In this paper, we identify three major decision making factors for the selection of an approximate multipliers circuit: (1) the type of approximate full adder (FA) used to construct the multiplier, (2) the architecture, i.e., array or tree, of the multiplier and (3) the placement of sub-modules of approximate and exact multipliers in the main multiplier module. Based on these factors, we explored the design space for circuit level implementations of approximate multipliers. We used circuit level implementations of some of the most widely used approximate full adders, i.e., approximate mirror adders, XOR/XNOR based approximate full adders and Inexact adder cell. These FA cells are then used to develop circuits for the approximate high order compressors as building blocks for 8x8 array and tree multipliers. We then develop various implementations of higher bit multipliers by using a combination of exact and inaccurate 8x8 multiplier cells. All these implementations have been done using the Cadence's Spectre tool with the TSMC65nm technology. The design space of these multipliers is explored based on their power, area, delay and error and the best approximate multiplier designs are identified. The report also presents the validation of our results using an image blending application. An open source library of implemented cells and multiplier circuits are available online.

Dynamic fault trees (DFTs) have emerged as an important tool for capturing the dynamic behavior of system failure. These DFTs are then analyzed qualitatively and quantitatively using stochastic or algebraic methods to judge the failure characteristics of the given system in terms of the failures of its sub-components. Model checking has been recently proposed to conduct the failure analysis of systems using DFTs with the motivation to provide a rigorous failure analysis of safety-critical systems. However, model checking has not been used for the DFT qualitative analysis and the reduction algorithms used in model checking are usually not formally verified. Moreover, the analysis time grows exponentially with the increase of the number of states. These issues limit the usefulness of model checking for analyzing complex systems used in safety-critical domains, where the accuracy and completeness of analysis matters the most. To overcome these limitations, we propose a comprehensive methodology to perform the qualitative and quantitative analysis of DFTs using an integration of theorem proving and model checking based approaches. For this purpose, we formalized all the basic dynamic fault tree gates using higher-order logic based on the algebraic approach and formally verified some of the simplification properties. This formalization allows us to formally verify the equivalence between the original and reduced DFTs using a theorem prover, and conduct the qualitative analysis. We then use model checking to perform the quantitative analysis of the formally verified reduced DFT. We applied our methodology to five benchmarks and the results show that the formally verified reduced DFT was analyzed using model checking with up to six times less states and up to 133000 times faster.

Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, confidentiality, and integrity. Various dependability modeling techniques have been developed to effectively capture the failure characteristics of systems over time. Traditionally, dependability models are analyzed using paper-and-pencil proof methods and computer based simulation tools but their results cannot be trusted due to their inherent inaccuracy limitations. The recent developments in probabilistic analysis support using formal methods have enabled the possibility of accurate and rigorous dependability analysis. Thus, the usage of formal methods for dependability analysis is widely advocated for safety-critical domains, such as transportation, aerospace and health. Given the complementary strengths of mainstream formal methods, like theorem proving and model checking, and the variety of dependability models judging the most suitable formal technique for a given dependability model is not a straightforward task. In this paper, we present a comprehensive review of existing formal dependability analysis techniques along with their pros and cons for handling a particular dependability model.

Hadoop has become the de facto standard for processing large data in today's cloud environment. The performance of Hadoop in the cloud has a direct impact on many important applications ranging from web analytic, web indexing, image and document processing to high-performance scientific computing. However, because of the scale, complexity and dynamic nature of the cloud, failures are common and these failures often impact the performance of jobs running in Hadoop. Although Hadoop possesses built-in failure detection and recovery mechanisms, several scheduled jobs still fail because of unforeseen events in the cloud environment. A single task failure can cause the failure of the whole job and unpredictable job running times. In this report, we propose ATLAS (AdapTive faiLure-Aware Scheduler), a new scheduler for Hadoop that can adapt its scheduling decisions to events occurring in the cloud environment. Using statistical models, ATLAS predicts task failures and adjusts its scheduling decisions on the fly to reduce task failure occurrences. We implement ATLAS in the Hadoop framework of Amazon Elastic MapReduce (EMR) and perform a case study to compare its performance with those of the FIFO, Fair and Capacity schedulers. Results show that ATLAS can reduce the percentage of failed jobs by up to 28% and the percentage of failed tasks by up to 39%, and the total execution time of jobs by 10 minutes on average. ATLAS also reduces CPU and memory usages., Comment: 24 pages

Cloud Computing has emerged as a key technology to deliver and manage computing, platform, and software services over the Internet. Task scheduling algorithms play an important role in the efficiency of cloud computing services as they aim to reduce the turnaround time of tasks and improve resource utilization. Several task scheduling algorithms have been proposed in the literature for cloud computing systems, the majority relying on the computational complexity of tasks and the distribution of resources. However, several tasks scheduled following these algorithms still fail because of unforeseen changes in the cloud environments. In this paper, using tasks execution and resource utilization data extracted from the execution traces of real world applications at Google, we explore the possibility of predicting the scheduling outcome of a task using statistical models. If we can successfully predict tasks failures, we may be able to reduce the execution time of jobs by rescheduling failed tasks earlier (i.e., before their actual failing time). Our results show that statistical models can predict task failures with a precision up to 97.4%, and a recall up to 96.2%. We simulate the potential benefits of such predictions using the tool kit GloudSim and found that they can improve the number of finished tasks by up to 40%. We also perform a case study using the Hadoop framework of Amazon Elastic MapReduce (EMR) and the jobs of a gene expression correlations analysis study from breast cancer research. We find that when extending the scheduler of Hadoop with our predictive models, the percentage of failed jobs can be reduced by up to 45%, with an overhead of less than 5 minutes.

Fractional calculus is a generalization of classical theories of integration and differentiation to arbitrary order (i.e., real or complex numbers). In the last two decades, this new mathematical modeling approach has been widely used to analyze a wide class of physical systems in various fields of science and engineering. In this paper, we describe an ongoing project which aims at formalizing the basic theories of fractional calculus in the HOL Light theorem prover. Mainly, we present the motivation and application of such formalization efforts, a roadmap to achieve our goals, current status of the project and future milestones., Comment: 9 pages

It is customary to assess the reliability of underground oil and gas pipelines in the presence of excessive loading and corrosion effects to ensure a leak-free transport of hazardous materials. The main idea behind this reliability analysis is to model the given pipeline system as a Reliability Block Diagram (RBD) of segments such that the reliability of an individual pipeline segment can be represented by a random variable. Traditionally, computer simulation is used to perform this reliability analysis but it provides approximate results and requires an enormous amount of CPU time for attaining reasonable estimates. Due to its approximate nature, simulation is not very suitable for analyzing safety-critical systems like oil and gas pipelines, where even minor analysis flaws may result in catastrophic consequences. As an accurate alternative, we propose to use a higher-order-logic theorem prover (HOL) for the reliability analysis of pipelines. As a first step towards this idea, this paper provides a higher-order-logic formalization of reliability and the series RBD using the HOL theorem prover. For illustration, we present the formal analysis of a simple pipeline that can be modeled as a series RBD of segments with exponentially distributed failure times., Comment: 15 pages

Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it to formalize electromagnetic fields and to prove the law of reflection for the planar waves., Comment: 15 pages, 1 figure

Optical systems are becoming increasingly important by resolving many bottlenecks in today's communication, electronics, and biomedical systems. However, given the continuous nature of optics, the inability to efficiently analyze optical system models using traditional paper-and-pencil and computer simulation approaches sets limits especially in safety-critical applications. In order to overcome these limitations, we propose to employ higher-order-logic theorem proving as a complement to computational and numerical approaches to improve optical model analysis in a comprehensive framework. The proposed framework allows formal analysis of optical systems at four abstraction levels, i.e., ray, wave, electromagnetic, and quantum.

In top-down multi-level design methodologies, design descriptions at higher levels of abstraction are incrementally refined to the final realizations. Simulation based techniques have traditionally been used to verify that such model refinements do not change the design functionality. Unfortunately, with computer simulations it is not possible to completely check that a design transformation is correct in a reasonable amount of time, as the number of test patterns required to do so increase exponentially with the number of system state variables. In this paper, we propose a methodology for the verification of conformance of models generated at higher levels of abstraction in the design process to the design specifications. We model the system behavior using sequence of recurrence equations. We then use symbolic simulation together with equivalence checking and property checking techniques for design verification. Using our proposed method, we have verified the equivalence of three WiMax system models at different levels of design abstraction, and the correctness of various system properties on those models. Our symbolic modeling and verification experiments show that the proposed verification methodology provides performance advantage over its numerical counterpart., Comment: In Proceedings SCSS 2012, arXiv:1307.8029

Modeling and analysis of soft errors in electronic circuits has traditionally been done using computer simulations. Computer simulations cannot guarantee correctness of analysis because they utilize approximate real number representations and pseudo random numbers in the analysis and thus are not well suited for analyzing safety-critical applications. In this paper, we present a higher-order logic theorem proving based method for modeling and analysis of soft errors in electronic circuits. Our developed infrastructure includes formalized continuous random variable pairs, their Cumulative Distribution Function (CDF) properties and independent standard uniform and Gaussian random variables. We illustrate the usefulness of our approach by modeling and analyzing soft errors in commonly used dynamic random access memory sense amplifier circuits., Comment: In Proceedings SCSS 2012, arXiv:1307.8029, Hardware -> Dynamic memory; Transient errors and upsets; Safety critical systems; Security and privacy -> Logic and verification; Theory of computation -> Automated reasoning; Computer systems organization -> Reliability

Wireless Sensor Networks (WSNs) have been widely explored for forest fire detection, which is considered a fatal threat throughout the world. Energy conservation of sensor nodes is one of the biggest challenges in this context and random scheduling is frequently applied to overcome that. The performance analysis of these random scheduling approaches is traditionally done by paper-and-pencil proof methods or simulation. These traditional techniques cannot ascertain 100% accuracy, and thus are not suitable for analyzing a safety-critical application like forest fire detection using WSNs. In this paper, we propose to overcome this limitation by applying formal probabilistic analysis using theorem proving to verify scheduling performance of a real-world WSN for forest fire detection using a k-set randomized algorithm as an energy saving mechanism. In particular, we formally verify the expected values of coverage intensity, the upper bound on the total number of disjoint subsets, for a given coverage intensity, and the lower bound on the total number of nodes., Comment: In Proceedings SCSS 2012, arXiv:1307.8029