archives

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


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Hanna, Youssef and Rajan, Hridesh (2007) Verifying Fault-Tolerance of Sensor Network Applications Using Auto-generated Fault Injection Mechanisms. Technical Report 07-11, Computer Science, Iowa State University.

Full text available as:Adobe PDF

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.

Keywords:sensor networks, fault tolerance, model checking, slede, fault injection model generation, fault-tolerant systems
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000548
Deposited by:Hridesh Rajan on 05 July 2007



Contact site administrator at: ssg@cs.iastate.edu