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):