Automating software feature verification

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 feature 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. Requirement 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 notoriously difficult to detect with traditional testing techniques. Error reports are typically generated by the system within minutes after a check is initiated, quickly enough to allow near interactive probing of r...

• Type: Journal
• Year: 2000
• Where: BELL
• Authors: Gerard J. Holzmann, Margaret H. Smith
• Keywords: BELL 2000, Formal Verification Techniques, Logic Model Checker, PathStar Access Server