Verifying Fault-Tolerance of Sensor Network Applications Using Auto-generated Fault Injection Mechanisms

By: Youssef Wasfy Hanna and Hridesh Rajan

Abstract

The deployment scenarios for sensor networks are often hostile. These networks also have to operate unattended for long periods. Therefore, fault-tolerance mechanisms are needed to protect these networks from various faults such as node failure due to loss of power, compromise, etc and link failure due to network intrusion, etc. A number of fault-tolerance techniques have been developed specifically for wireless sensor networks. Verifying these fault-tolerant techniques is necessary for reliability and dependability checks. Formal methods such as model checking have been used for verification of such fault-tolerance mechanisms; however, building the models is a tedious job which makes model checking a hard task to accomplish. Techniques that allow model checking source code ease this task. These approaches automate the process of verification model construction. There are two aspects of automated verification model construction. First, a model of the application needs to be built. Second, a model of faults has to be created to expose problems with the application. In a previous work, we developed a framework, which we called Slede, to automatically extract PROMELA models from sensor network applications written in the nesC language. The contribution of this work is the design and implementation of a mechanism for automatically generating fault models from a partial specification of the application. By automatically generating fault models, our approach eases the verification of fault-tolerance for sensor network applications.

ACM Reference

Hanna, Y.W. and Rajan, H. 2007. Verifying Fault-Tolerance of Sensor Network Applications Using Auto-generated Fault Injection Mechanisms. Technical Report #07-11. Iowa State University, Dept. of Computer Science.

BibTeX Reference

@techreport{hanna2007verifying,
  title = {Verifying Fault-Tolerance of Sensor Network Applications Using Auto-generated Fault Injection Mechanisms},
  author = {Hanna, Youssef Wasfy and Rajan, Hridesh},
  year = {2007},
  month = {June},
  institution = {Iowa State University, Dept. of Computer Science},
  number = {07-11},
  abstract = {
    The deployment scenarios for sensor networks are often hostile. These networks
    also have to operate unattended for long periods. Therefore, fault-tolerance
    mechanisms are needed to protect these networks from various faults such as
    node failure due to loss of power, compromise, etc and link failure due to
    network intrusion, etc. A number of fault-tolerance techniques have been
    developed specifically for wireless sensor networks. Verifying these
    fault-tolerant techniques is necessary for reliability and dependability
    checks. Formal methods such as model checking have been used for verification
    of such fault-tolerance mechanisms; however, building the models is a tedious
    job which makes model checking a hard task to accomplish. Techniques that
    allow model checking source code ease this task. These approaches automate the
    process of verification model construction. There are two aspects of automated
    verification model construction. First, a model of the application needs to be
    built. Second, a model of faults has to be created to expose problems with the
    application. In a previous work, we developed a framework, which we called
    Slede, to automatically extract PROMELA models from sensor network
    applications written in the nesC language. The contribution of this work is
    the design and implementation of a mechanism for automatically generating
    fault models from a partial specification of the application. By automatically
    generating fault models, our approach eases the verification of
    fault-tolerance for sensor network applications.
  }
}