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

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