SYSTEMATIC SOFTWARE TESTING USING VERISOFT - AN ANALYSIS OF THE 4ESS(TM) HEART-BEAT MONITOR

VeriSoft is a tool for systematically exploring the state spaces of sy stems composed of several concurrent processes executing arbitrary cod e written in full-fledged programming languages, such as C or C++. Usi ng VeriSoft, we analyzed the 4ESS(TM) switch Heart-Beat Monitor (HBM) a telephone switching application developed at Lucent Technologies. Th e 4ESS HEM plays an important role in routing data in the switch and c an significantly affect switch performance. Since VeriSoft automatical ly generates, executes, and evaluates thousands of tests per minute an d has complete control over nondeterminism, our analysis revealed HEM behavior that is virtually impossible to detect or test in a tradition al lab testing environment. Specifically, we discovered flaws in the e xisting documentation for this application and unexpected behaviors in the software itself. These results are being used as the basis for an improved design of the HEM software in the 4ESS switch.