Automating software feature verification

A significant part of the call processing software for Lucent's new PathStar ™ AccessServer 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 newverification 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 detailedexecution traces of the system source. A main strength of the system is its capability to detect potentialfeature interaction problems at an early stage of systems design. This type of problem is difficult to detectwith traditional testing techniques. Error reports are typically generated by the system within minutes after acomprehensive check is initiated, allowing near‐interactive probing of feature requirements and quickconfirmation (or rejection) of the validity of tentative software fixes.