The FeaVer Feature Verification System
The telephone call processing code for one of Lucent's switches,
the PathStar®
access server, was checked against a database of formally
specified logical correctness requirements using standard
model checking techniques. Non-standard was the architecture of the
checking system that we built to support this process.
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 have devised a system for extracting
verification models mechanically from implementation level
production code, written in C.
The user of the system is not required to manually
construct an accurate model before verification can begin.
Instead, a generic user-defined map is used to guide
the model extraction process. This type of map is generally
simpler to develop and maintain than a complete user-level
formal model.
The FeaVer system can run virtually autonomously,
generating sample execution scenarios that violate the
required system properties within minutes after a property
is added, or modified, or after the call processing
software itself is revised.
The tester's responsibility is confined to maintaining
a comprehensive database of properties that the software
is required to satisfy, and to interpreting the error
scenarios that the system produces.
(More detail.)
The FeaVer project has meanwhile given rise to a standalone tool,
named FEAVER, for verification of general
software written in ANSI-C.
See: Modex.
Related projects: