Academic Journals Database
Disseminating quality controlled scientific knowledge

A Pre-Injection Analysis for Identifying Fault-Injection Tests for Protocol Validation

ADD TO MY LIST
 
Author(s): Neeraj Suri | Purnendu Sinha

Journal: Journal of Software
ISSN 1796-217X

Volume: 5;
Issue: 10;
Start page: 1144;
Date: 2010;
Original page

Keywords: dependable distributed protocols | fault injection | formal techniques | verification and validation

ABSTRACT
Fault-injection (FI) based techniques for dependability assessment of distributed protocols face certain limitations in providing state-space coverage and also incur high operational cost. This is mainly due to lack of complete knowledge of fault-distribution at the protocol level which in turn limits the use of statistical approaches in deriving and estimating the number of test cases to inject. In practice, formal techniques have effectively being used in proving the correctness of dependable distributed protocols, and these techniques  traditionally have not been directly associated with experimental validation techniques such as FI-based testing. There exists a gap between these two well-established approaches, viz. formal verification and FI-based validation  techniques. If there exists an approach which utilizing a rich set of information pertaining to the protocol operation generated through formal verification process can provide guided-support to perform FI-based validation, then the overall effectiveness of such validation techniques can be greatly improved. With this viewpoint, in this paper, we propose a methodology which utilizes the theorem-proving technique as an underlying formal-engine, and is composed of two novel structured and graphical representation schemes (interactive user-interfaces) for (a) capturing/visualizing information generated over the formal verification process, (b) facilitating interactive analysis through the chosen formal-engine (any theorem-proving tool) and database, and (c) user-guided identification of influential parameters, those eventually used for generating test cases for FI-based testing. A case study of an on-line diagnosis protocol is used to illustrate and establish the viability of the proposed methodology.
Save time & money - Smart Internet Solutions     

Tango Rapperswil
Tango Rapperswil