Statemate applied to statistical software testing

Abstract

This paper is concerned with the use of statistical testing as a verification technique for complex software. Statistical testing involves exercising a program with random inputs, the test profile and the number of generated inputs being determined according to criteria based on program structure or software functionality. In case of complex programs, the probabilistic generation must be based on a black box analysis, the adopted criteria being defined from behavior models deduced from the specification. The proposed approach refers to a hierarchical specification produced in the STATEMATE(R) environment. Its feasibility is exemplified on a safety-critical module from the nuclear field, and the efficiency in revealing actual faults is investigated through experiments involving two versions of the module.