The FeaVer System

The four main components of the Feature Verification System were:

  • A library of properties that capture the verifiable properties of the code being checked;
  • A model extraction capability that can derive abstracted verification models mechanically from implementation level C code;
  • The Spin model checker running in the background to generate all verification jobs that can check the source against the properties.
  • A 16-CPU multiprocessing system, called FeaVer, to parallelize the verification runs.
Library of properties The FeaVer library of logic properties is comparable to the library of test-objectives from a traditional methodology based on software testing, but there are some significant differences as well that speed up the verification process. Each property in the feature database formalizes a large class of potential system executions that may violate a given property. It takes just one run of the verifier to establish if such a class is empty or non-empty in the system as implemented, and, in the latter case, to produce an instance of that class as an example. Properties can be specified in logic, as test automata, or visually with the help of timing diagrams. (More detail.)

Model extraction The conversion of C code into a verification model takes a fraction of a second and is a virtually invisible part of the complete verification process on FeaVer. To setup the extraction capability, the user defines (once) a simple lookup table that identifies the source code statements that are relevant to the properties being checked. The rest of the process is automated. (More detail.)

Model checking FeaVer generates code that can be analyzed efficiently by the Bell Labs model checker Spin. The application within FeaVer has lead to extensions of the Spin system that makes it possible to support the required level of interactive feedback. Searches can either be initiated by the user, or can be autonomously triggered by FeaVer itself when it detects a change in either the software, or in one or more of its required properties. (More detail.)

Hardware support Multiprocessing hardware made it possible to execute a series of increasingly precise searches on 16 computers in parallel, so that property violations could be reported with unprecedented speed. (More detail.)

Back to Main Page