Automating software feature verification

A significant part of the call processing software for Lucent's new PathStar(TM) Access Server was checked with formal verification techniques. The verification system we built for this purpose, named FeaVer, is accessed via a standard Web browser. The system maintains a database of feature requirements, together with the results of the most recently performed verifications. Via the browser the user can invoke new verification runs, which are performed in the background with the help of a logic model checking tool. Requirement violations are reported either as high-level message sequence charts or as detailed execution traces of the system source. A main strength of the system is its capability to detect potential feature interaction problems at an early stage of systems design. This type of problem is difficult to detect with traditional testing techniques. Error reports are typically generated by the system within minutes after a comprehensive check is initiated, allowing near-interactive probing of feature requirements and quick confirmation (or rejection) of the validity of tentative software fixes.