SVEX: switching program verification expert system

The switching program verification expert system (SVEX) automatically detects logical bugs of call handling programs and outputs information for debugging. SVEX can also reverse-engineer the service specifications from the programs. This function is used for detecting service bugs. The functions are implemented by using verification rules and by simulating the actions of programs on an object-oriented switching-system model. SVEX was applied to the development of PBX and detected logical errors automatically, in which the errors overlooked at the functional test using the target switching system were included