Automating software feature verification

Abstract

A significant part of the call processing software for Lucent's new PathStar  access server (FSW98) was checked with automated formal verification techniques. The verification system we built for this purpose, named FeaVer, maintains a database of fea- ture requirements which is accessible via a web browser. Via the browser the user can invoke verification runs. The verifications are performed by the system with the help of a standard logic model checker that runs in the background, invisibly to the user. Require- ment violations are reported as C execution traces and stored in the database for user perusal and correction. The main strength of the system is in the detection of undesired feature interactions at an early stage of systems design, the type of problem that is notori- ously difficult to detect with traditional testing techniques. Error reports are typically generated by the system within minutes after a check is initi- ated, quickly enough to allow near interactive probing of requirements or experimenting with software fixes.