TY - JOUR

T1 - A pre-injection analysis for identifying fault-injection tests for protocol validation

AU - Suri, Neeraj

AU - Sinha, P.

PY - 2010

Y1 - 2010

N2 - 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. © 2010 ACADEMY PUBLISHER.

AB - 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. © 2010 ACADEMY PUBLISHER.

KW - Dependable distributed protocols

KW - Fault injection

KW - Formal techniques

KW - Verification and validation

KW - Distributed protocols

KW - Experimental validations

KW - Formal verifications

KW - Graphical representations

KW - Injection test

KW - Interactive analysis

KW - On-line diagnosis

KW - Operational costs

KW - Overall effectiveness

KW - Protocol level

KW - Protocol operation

KW - Protocol validation

KW - State-space

KW - Statistical approach

KW - Test case

KW - Graphical user interfaces

KW - Theorem proving

U2 - 10.4304/jsw.5.10.1144-1161

DO - 10.4304/jsw.5.10.1144-1161

M3 - Journal article

VL - 5

SP - 1144

EP - 1161

JO - Journal of Software

JF - Journal of Software

SN - 1796-217X

IS - 10

ER -