The FeaVer Feature Verification System

(Bell Labs 1998-1999)

The telephone call processing C code for Lucent's PathStar® access server switch was checked against a database of formally specified logical correctness requirements using standard model checking techniques, in a fully automated process. The architecture of the checking system that we built to support this process was in many ways the first of its kind.

The system had two aims: (1) to automate the verification process to the greatest possible degree, and (2) to shield those performing the verifications as much as possible from the mechanics of the checking process itself. To achieve this we devised a system for extracting verification models mechanically from implementation level production code, written in C, using the modex tool. The user of the system was not required to manually construct an accurate model before verification could begin. Instead, a generic user-defined map was used to guide the model extraction process. This type of map is generally simpler to develop and maintain than a user-level formal model.

The FeaVer system couldn run virtually autonomously, generating sample execution scenarios that violated the required system properties within minutes after a property was added, or modified, or after the call processing software itself was revised. The tester's responsibility was confined to maintaining a comprehensive database of properties that the software was required to satisfy, and to interpreting the error scenarios that the system produces. (More detail.)

The FeaVer project also led to a standalone GUI-based tool, named FEAVER, for verification of general software written in ANSI-C.

Related projects (links updated 2017):

Papers (PDF):
ICSE99, FORTE99, BLTJ2000.